Documentation

Mathlib.Order.UpperLower.Prod

Upper and lower set product #

The Cartesian product of sets carries over to upper and lower sets in a natural way. This file defines said product over the types UpperSet and LowerSet and proves some of its properties.

Notation #

source
theorem IsUpperSet.prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {t : Set β} (hs : IsUpperSet s) (ht : IsUpperSet t) :
IsUpperSet (s ×ˢ t)
source
theorem IsLowerSet.prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {t : Set β} (hs : IsLowerSet s) (ht : IsLowerSet t) :
IsLowerSet (s ×ˢ t)
source
def UpperSet.prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : UpperSet α) (t : UpperSet β) :
UpperSet (α × β)

The product of two upper sets as an upper set.

Equations
  • s.prod t = { carrier := ↑s ×ˢ ↑t, upper' := ⋯ }
Instances For
    source
    @[implicit_reducible]
    instance UpperSet.instSProd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
    SProd (UpperSet α) (UpperSet β) (UpperSet (α × β))
    Equations
    source
    @[simp]
    theorem UpperSet.coe_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : UpperSet α) (t : UpperSet β) :
    ↑(s ×ˢ t) = ↑s ×ˢ ↑t
    source
    @[simp]
    theorem UpperSet.mem_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} {s : UpperSet α} {t : UpperSet β} :
    x ∈ s ×ˢ t ↔ x.1 ∈ s ∧ x.2 ∈ t
    source
    theorem UpperSet.Ici_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (x : α × β) :
    Ici x = Ici x.1 ×ˢ Ici x.2
    source
    @[simp]
    theorem UpperSet.Ici_prod_Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α) (b : β) :
    Ici a ×ˢ Ici b = Ici (a, b)
    source
    @[simp]
    theorem UpperSet.prod_top {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : UpperSet α) :
    s ×ˢ ⊤ = ⊤
    source
    @[simp]
    theorem UpperSet.top_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (t : UpperSet β) :
    ⊤ ×ˢ t = ⊤
    source
    @[simp]
    theorem UpperSet.bot_prod_bot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
    ⊥ ×ˢ ⊥ = ⊥
    source
    @[simp]
    theorem UpperSet.sup_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ s₂ : UpperSet α) (t : UpperSet β) :
    (s₁ ⊔ s₂) ×ˢ t = s₁ ×ˢ t ⊔ s₂ ×ˢ t
    source
    @[simp]
    theorem UpperSet.prod_sup {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : UpperSet α) (t₁ t₂ : UpperSet β) :
    s ×ˢ (t₁ ⊔ t₂) = s ×ˢ t₁ ⊔ s ×ˢ t₂
    source
    @[simp]
    theorem UpperSet.inf_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ s₂ : UpperSet α) (t : UpperSet β) :
    (s₁ ⊓ s₂) ×ˢ t = s₁ ×ˢ t ⊓ s₂ ×ˢ t
    source
    @[simp]
    theorem UpperSet.prod_inf {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : UpperSet α) (t₁ t₂ : UpperSet β) :
    s ×ˢ (t₁ ⊓ t₂) = s ×ˢ t₁ ⊓ s ×ˢ t₂
    source
    theorem UpperSet.prod_sup_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ s₂ : UpperSet α) (t₁ t₂ : UpperSet β) :
    s₁ ×ˢ t₁ ⊔ s₂ ×ˢ t₂ = (s₁ ⊔ s₂) ×ˢ (t₁ ⊔ t₂)
    source
    theorem UpperSet.prod_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ s₂ : UpperSet α} {t₁ t₂ : UpperSet β} :
    s₁ ≤ s₂ → t₁ ≤ t₂ → s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂
    source
    theorem UpperSet.prod_mono_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ s₂ : UpperSet α} {t : UpperSet β} :
    s₁ ≤ s₂ → s₁ ×ˢ t ≤ s₂ ×ˢ t
    source
    theorem UpperSet.prod_mono_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : UpperSet α} {t₁ t₂ : UpperSet β} :
    t₁ ≤ t₂ → s ×ˢ t₁ ≤ s ×ˢ t₂
    source
    @[simp]
    theorem UpperSet.prod_self_le_prod_self {α : Type u_1} [Preorder α] {s₁ s₂ : UpperSet α} :
    s₁ ×ˢ s₁ ≤ s₂ ×ˢ s₂ ↔ s₁ ≤ s₂
    source
    @[simp]
    theorem UpperSet.prod_self_lt_prod_self {α : Type u_1} [Preorder α] {s₁ s₂ : UpperSet α} :
    s₁ ×ˢ s₁ < s₂ ×ˢ s₂ ↔ s₁ < s₂
    source
    theorem UpperSet.prod_le_prod_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ s₂ : UpperSet α} {t₁ t₂ : UpperSet β} :
    s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂ ↔ s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₂ = ⊤ ∨ t₂ = ⊤
    source
    @[simp]
    theorem UpperSet.prod_eq_top {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : UpperSet α} {t : UpperSet β} :
    s ×ˢ t = ⊤ ↔ s = ⊤ ∨ t = ⊤
    source
    @[simp]
    theorem UpperSet.codisjoint_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ s₂ : UpperSet α} {t₁ t₂ : UpperSet β} :
    Codisjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Codisjoint s₁ s₂ ∨ Codisjoint t₁ t₂
    source
    def LowerSet.prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : LowerSet α) (t : LowerSet β) :
    LowerSet (α × β)

    The product of two lower sets as a lower set.

    Equations
    • s.prod t = { carrier := ↑s ×ˢ ↑t, lower' := ⋯ }
    Instances For
      source
      @[implicit_reducible]
      instance LowerSet.instSProd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
      SProd (LowerSet α) (LowerSet β) (LowerSet (α × β))
      Equations
      source
      @[simp]
      theorem LowerSet.coe_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : LowerSet α) (t : LowerSet β) :
      ↑(s ×ˢ t) = ↑s ×ˢ ↑t
      source
      @[simp]
      theorem LowerSet.mem_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} {s : LowerSet α} {t : LowerSet β} :
      x ∈ s ×ˢ t ↔ x.1 ∈ s ∧ x.2 ∈ t
      source
      theorem LowerSet.Iic_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (x : α × β) :
      Iic x = Iic x.1 ×ˢ Iic x.2
      source
      @[simp]
      theorem LowerSet.Ici_prod_Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α) (b : β) :
      Iic a ×ˢ Iic b = Iic (a, b)
      source
      @[simp]
      theorem LowerSet.prod_bot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : LowerSet α) :
      s ×ˢ ⊥ = ⊥
      source
      @[simp]
      theorem LowerSet.bot_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (t : LowerSet β) :
      ⊥ ×ˢ t = ⊥
      source
      @[simp]
      theorem LowerSet.top_prod_top {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
      ⊤ ×ˢ ⊤ = ⊤
      source
      @[simp]
      theorem LowerSet.inf_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ s₂ : LowerSet α) (t : LowerSet β) :
      (s₁ ⊓ s₂) ×ˢ t = s₁ ×ˢ t ⊓ s₂ ×ˢ t
      source
      @[simp]
      theorem LowerSet.prod_inf {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : LowerSet α) (t₁ t₂ : LowerSet β) :
      s ×ˢ (t₁ ⊓ t₂) = s ×ˢ t₁ ⊓ s ×ˢ t₂
      source
      @[simp]
      theorem LowerSet.sup_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ s₂ : LowerSet α) (t : LowerSet β) :
      (s₁ ⊔ s₂) ×ˢ t = s₁ ×ˢ t ⊔ s₂ ×ˢ t
      source
      @[simp]
      theorem LowerSet.prod_sup {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : LowerSet α) (t₁ t₂ : LowerSet β) :
      s ×ˢ (t₁ ⊔ t₂) = s ×ˢ t₁ ⊔ s ×ˢ t₂
      source
      theorem LowerSet.prod_inf_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ s₂ : LowerSet α) (t₁ t₂ : LowerSet β) :
      s₁ ×ˢ t₁ ⊓ s₂ ×ˢ t₂ = (s₁ ⊓ s₂) ×ˢ (t₁ ⊓ t₂)
      source
      theorem LowerSet.prod_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ s₂ : LowerSet α} {t₁ t₂ : LowerSet β} :
      s₁ ≤ s₂ → t₁ ≤ t₂ → s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂
      source
      theorem LowerSet.prod_mono_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ s₂ : LowerSet α} {t : LowerSet β} :
      s₁ ≤ s₂ → s₁ ×ˢ t ≤ s₂ ×ˢ t
      source
      theorem LowerSet.prod_mono_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : LowerSet α} {t₁ t₂ : LowerSet β} :
      t₁ ≤ t₂ → s ×ˢ t₁ ≤ s ×ˢ t₂
      source
      @[simp]
      theorem LowerSet.prod_self_le_prod_self {α : Type u_1} [Preorder α] {s₁ s₂ : LowerSet α} :
      s₁ ×ˢ s₁ ≤ s₂ ×ˢ s₂ ↔ s₁ ≤ s₂
      source
      @[simp]
      theorem LowerSet.prod_self_lt_prod_self {α : Type u_1} [Preorder α] {s₁ s₂ : LowerSet α} :
      s₁ ×ˢ s₁ < s₂ ×ˢ s₂ ↔ s₁ < s₂
      source
      theorem LowerSet.prod_le_prod_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ s₂ : LowerSet α} {t₁ t₂ : LowerSet β} :
      s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂ ↔ s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₁ = ⊥ ∨ t₁ = ⊥
      source
      @[simp]
      theorem LowerSet.prod_eq_bot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : LowerSet α} {t : LowerSet β} :
      s ×ˢ t = ⊥ ↔ s = ⊥ ∨ t = ⊥
      source
      @[simp]
      theorem LowerSet.disjoint_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ s₂ : LowerSet α} {t₁ t₂ : LowerSet β} :
      Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂
      source
      @[simp]
      theorem upperClosure_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : Set α) (t : Set β) :
      upperClosure (s ×ˢ t) = upperClosure s ×ˢ upperClosure t
      source
      @[simp]
      theorem lowerClosure_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : Set α) (t : Set β) :
      lowerClosure (s ×ˢ t) = lowerClosure s ×ˢ lowerClosure t