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