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

• ×ˢ is notation for UpperSet.prod / LowerSet.prod.

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

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

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' := ⋯ }

instance UpperSet.instSProd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : SProd (UpperSet α) (UpperSet β) (UpperSet (α × β))

Equations

• UpperSet.instSProd = { sprod := UpperSet.prod }

@[simp]

theorem UpperSet.coe_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : UpperSet α) (t : UpperSet β) : ↑(s ×ˢ t) = ↑s ×ˢ ↑t

@[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

theorem UpperSet.Ici_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (x : α × β) : Ici x = Ici x.1 ×ˢ Ici x.2

@[simp]

theorem UpperSet.Ici_prod_Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α) (b : β) : Ici a ×ˢ Ici b = Ici (a, b)

@[simp]

theorem UpperSet.prod_top {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : UpperSet α) : s ×ˢ ⊤ = ⊤

@[simp]

theorem UpperSet.top_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (t : UpperSet β) : ⊤ ×ˢ t = ⊤

@[simp]

theorem UpperSet.bot_prod_bot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : ⊥ ×ˢ ⊥ = ⊥

@[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

@[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₂

@[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

@[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₂

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₂)

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₂

theorem UpperSet.prod_mono_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ s₂ : UpperSet α} {t : UpperSet β} : s₁ ≤ s₂ → s₁ ×ˢ t ≤ s₂ ×ˢ t

theorem UpperSet.prod_mono_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : UpperSet α} {t₁ t₂ : UpperSet β} : t₁ ≤ t₂ → s ×ˢ t₁ ≤ s ×ˢ t₂

@[simp]

theorem UpperSet.prod_self_le_prod_self {α : Type u_1} [Preorder α] {s₁ s₂ : UpperSet α} : s₁ ×ˢ s₁ ≤ s₂ ×ˢ s₂ ↔ s₁ ≤ s₂

@[simp]

theorem UpperSet.prod_self_lt_prod_self {α : Type u_1} [Preorder α] {s₁ s₂ : UpperSet α} : s₁ ×ˢ s₁ < s₂ ×ˢ s₂ ↔ s₁ < s₂

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₂ = ⊤

@[simp]

theorem UpperSet.prod_eq_top {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : UpperSet α} {t : UpperSet β} : s ×ˢ t = ⊤ ↔ s = ⊤ ∨ t = ⊤

@[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₂

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' := ⋯ }

instance LowerSet.instSProd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : SProd (LowerSet α) (LowerSet β) (LowerSet (α × β))

Equations

• LowerSet.instSProd = { sprod := LowerSet.prod }

@[simp]

theorem LowerSet.coe_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : LowerSet α) (t : LowerSet β) : ↑(s ×ˢ t) = ↑s ×ˢ ↑t

@[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

theorem LowerSet.Iic_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (x : α × β) : Iic x = Iic x.1 ×ˢ Iic x.2

@[simp]

theorem LowerSet.Ici_prod_Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α) (b : β) : Iic a ×ˢ Iic b = Iic (a, b)

@[simp]

theorem LowerSet.prod_bot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : LowerSet α) : s ×ˢ ⊥ = ⊥

@[simp]

theorem LowerSet.bot_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (t : LowerSet β) : ⊥ ×ˢ t = ⊥

@[simp]

theorem LowerSet.top_prod_top {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : ⊤ ×ˢ ⊤ = ⊤

@[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

@[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₂

@[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

@[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₂

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₂)

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₂

theorem LowerSet.prod_mono_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ s₂ : LowerSet α} {t : LowerSet β} : s₁ ≤ s₂ → s₁ ×ˢ t ≤ s₂ ×ˢ t

theorem LowerSet.prod_mono_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : LowerSet α} {t₁ t₂ : LowerSet β} : t₁ ≤ t₂ → s ×ˢ t₁ ≤ s ×ˢ t₂

@[simp]

theorem LowerSet.prod_self_le_prod_self {α : Type u_1} [Preorder α] {s₁ s₂ : LowerSet α} : s₁ ×ˢ s₁ ≤ s₂ ×ˢ s₂ ↔ s₁ ≤ s₂

@[simp]

theorem LowerSet.prod_self_lt_prod_self {α : Type u_1} [Preorder α] {s₁ s₂ : LowerSet α} : s₁ ×ˢ s₁ < s₂ ×ˢ s₂ ↔ s₁ < s₂

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₁ = ⊥

@[simp]

theorem LowerSet.prod_eq_bot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : LowerSet α} {t : LowerSet β} : s ×ˢ t = ⊥ ↔ s = ⊥ ∨ t = ⊥

@[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₂

@[simp]

theorem upperClosure_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : Set α) (t : Set β) : upperClosure (s ×ˢ t) = upperClosure s ×ˢ upperClosure t

@[simp]

theorem lowerClosure_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : Set α) (t : Set β) : lowerClosure (s ×ˢ t) = lowerClosure s ×ˢ lowerClosure t