Theory of complete lattices

This file contains results on complete lattices that need more theory to develop.

Naming conventions

In lemma names,

• sSup is called sSup
• sInf is called sInf
• ⨆ i, s i is called iSup
• ⨅ i, s i is called iInf
• ⨆ i j, s i j is called iSup₂. This is an iSup inside an iSup.
• ⨅ i j, s i j is called iInf₂. This is an iInf inside an iInf.
• ⨆ i ∈ s, t i is called biSup for "bounded iSup". This is the special case of iSup₂ where j : i ∈ s.
• ⨅ i ∈ s, t i is called biInf for "bounded iInf". This is the special case of iInf₂ where j : i ∈ s.

Notation

• ⨆ i, f i : iSup f, the supremum of the range of f;
• ⨅ i, f i : iInf f, the infimum of the range of f.

iSup and iInf under Type

theorem iSup_bool_eq {α : Type u_1} [CompleteLattice α] {f : Bool → α} : ⨆ (b : Bool), f b = f true ⊔ f false

theorem iInf_bool_eq {α : Type u_1} [CompleteLattice α] {f : Bool → α} : ⨅ (b : Bool), f b = f true ⊓ f false

theorem sup_eq_iSup {α : Type u_1} [CompleteLattice α] (x y : α) : x ⊔ y = ⨆ (b : Bool), bif b then x else y

theorem inf_eq_iInf {α : Type u_1} [CompleteLattice α] (x y : α) : x ⊓ y = ⨅ (b : Bool), bif b then x else y

iSup and iInf under ℕ

theorem iSup_ge_eq_iSup_nat_add {α : Type u_1} [CompleteLattice α] (u : ℕ → α) (n : ℕ) : ⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i = ⨆ (i : ℕ), u (i + n)

theorem iInf_ge_eq_iInf_nat_add {α : Type u_1} [CompleteLattice α] (u : ℕ → α) (n : ℕ) : ⨅ (i : ℕ), ⨅ (_ : i ≥ n), u i = ⨅ (i : ℕ), u (i + n)

theorem Monotone.iSup_nat_add {α : Type u_1} [CompleteLattice α] {f : ℕ → α} (hf : Monotone f) (k : ℕ) : ⨆ (n : ℕ), f (n + k) = ⨆ (n : ℕ), f n

theorem Antitone.iInf_nat_add {α : Type u_1} [CompleteLattice α] {f : ℕ → α} (hf : Antitone f) (k : ℕ) : ⨅ (n : ℕ), f (n + k) = ⨅ (n : ℕ), f n

theorem iSup_iInf_ge_nat_add {α : Type u_1} [CompleteLattice α] (f : ℕ → α) (k : ℕ) : ⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), f (i + k) = ⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), f i

theorem iInf_iSup_ge_nat_add {α : Type u_1} [CompleteLattice α] (f : ℕ → α) (k : ℕ) : ⨅ (n : ℕ), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), f (i + k) = ⨅ (n : ℕ), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), f i

theorem sup_iSup_nat_succ {α : Type u_1} [CompleteLattice α] (u : ℕ → α) : u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = ⨆ (i : ℕ), u i

theorem inf_iInf_nat_succ {α : Type u_1} [CompleteLattice α] (u : ℕ → α) : u 0 ⊓ ⨅ (i : ℕ), u (i + 1) = ⨅ (i : ℕ), u i

theorem iInf_nat_gt_zero_eq {α : Type u_1} [CompleteLattice α] (f : ℕ → α) : ⨅ (i : ℕ), ⨅ (_ : i > 0), f i = ⨅ (i : ℕ), f (i + 1)

theorem iSup_nat_gt_zero_eq {α : Type u_1} [CompleteLattice α] (f : ℕ → α) : ⨆ (i : ℕ), ⨆ (_ : i > 0), f i = ⨆ (i : ℕ), f (i + 1)

Instances

theorem sup_sInf_le_iInf_sup {α : Type u_1} [CompleteLattice α] {a : α} {s : Set α} : a ⊔ sInf s ≤ ⨅ b ∈ s, a ⊔ b

This is a weaker version of sup_sInf_eq

theorem iSup_inf_le_inf_sSup {α : Type u_1} [CompleteLattice α] {a : α} {s : Set α} : ⨆ b ∈ s, a ⊓ b ≤ a ⊓ sSup s

This is a weaker version of inf_sSup_eq

theorem sInf_sup_le_iInf_sup {α : Type u_1} [CompleteLattice α] {a : α} {s : Set α} : sInf s ⊔ a ≤ ⨅ b ∈ s, b ⊔ a

This is a weaker version of sInf_sup_eq

theorem iSup_inf_le_sSup_inf {α : Type u_1} [CompleteLattice α] {a : α} {s : Set α} : ⨆ b ∈ s, b ⊓ a ≤ sSup s ⊓ a

This is a weaker version of sSup_inf_eq

theorem iInf_sup_le_iInf_sup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f : ι → α) (a : α) : (⨅ (i : ι), f i) ⊔ a ≤ ⨅ (i : ι), f i ⊔ a

theorem sup_iInf_le_iInf_sup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f : ι → α) (a : α) : a ⊔ ⨅ (i : ι), f i ≤ ⨅ (i : ι), a ⊔ f i

theorem iSup_inf_le_iSup_inf {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f : ι → α) (a : α) : ⨆ (i : ι), f i ⊓ a ≤ (⨆ (i : ι), f i) ⊓ a

theorem iSup_inf_le_inf_iSup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f : ι → α) (a : α) : ⨆ (i : ι), a ⊓ f i ≤ a ⊓ ⨆ (i : ι), f i

theorem biInf_sup_le_biInf_sup {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : β → α) (s : Set β) (a : α) : (⨅ i ∈ s, f i) ⊔ a ≤ ⨅ i ∈ s, f i ⊔ a

theorem sup_biInf_le_biInf_sup {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : β → α) (s : Set β) (a : α) : a ⊔ ⨅ i ∈ s, f i ≤ ⨅ i ∈ s, a ⊔ f i

theorem biSup_inf_le_biSup_inf {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : β → α) (s : Set β) (a : α) : ⨆ i ∈ s, f i ⊓ a ≤ (⨆ i ∈ s, f i) ⊓ a

theorem biSup_inf_le_inf_biSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : β → α) (s : Set β) (a : α) : ⨆ i ∈ s, a ⊓ f i ≤ a ⊓ ⨆ i ∈ s, f i

theorem le_iSup_inf_iSup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f g : ι → α) : ⨆ (i : ι), f i ⊓ g i ≤ (⨆ (i : ι), f i) ⊓ ⨆ (i : ι), g i

theorem iInf_sup_iInf_le {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f g : ι → α) : (⨅ (i : ι), f i) ⊔ ⨅ (i : ι), g i ≤ ⨅ (i : ι), f i ⊔ g i

theorem disjoint_sSup_left {α : Type u_1} [CompleteLattice α] {a : Set α} {b : α} (d : Disjoint (sSup a) b) {i : α} (hi : i ∈ a) : Disjoint i b

theorem disjoint_sSup_right {α : Type u_1} [CompleteLattice α] {a : Set α} {b : α} (d : Disjoint b (sSup a)) {i : α} (hi : i ∈ a) : Disjoint b i

theorem disjoint_of_sSup_disjoint_of_le_of_le {α : Type u_1} [CompleteLattice α] {a b : α} {c d : Set α} (hs : ∀ e ∈ c, e ≤ a) (ht : ∀ e ∈ d, e ≤ b) (hd : Disjoint a b) (he : ⊥ ∉ c ∨ ⊥ ∉ d) : Disjoint c d

theorem disjoint_of_sSup_disjoint {α : Type u_1} [CompleteLattice α] {a b : Set α} (hd : Disjoint (sSup a) (sSup b)) (he : ⊥ ∉ a ∨ ⊥ ∉ b) : Disjoint a b

@[implicit_reducible]

instance ULift.supSet {α : Type u_1} [SupSet α] : SupSet (ULift α)

Equations

• ULift.supSet = { sSup := fun (s : Set (ULift α)) => { down := sSup (ULift.up ⁻¹' s) } }

theorem ULift.down_sSup {α : Type u_1} [SupSet α] (s : Set (ULift α)) : (sSup s).down = sSup (up ⁻¹' s)

theorem ULift.up_sSup {α : Type u_1} [SupSet α] (s : Set α) : { down := sSup s } = sSup (down ⁻¹' s)

@[implicit_reducible]

instance ULift.infSet {α : Type u_1} [InfSet α] : InfSet (ULift α)

Equations

• ULift.infSet = { sInf := fun (s : Set (ULift α)) => { down := sInf (ULift.up ⁻¹' s) } }

theorem ULift.down_sInf {α : Type u_1} [InfSet α] (s : Set (ULift α)) : (sInf s).down = sInf (up ⁻¹' s)

theorem ULift.up_sInf {α : Type u_1} [InfSet α] (s : Set α) : { down := sInf s } = sInf (down ⁻¹' s)

theorem ULift.down_iSup {α : Type u_1} {ι : Sort u_4} [SupSet α] (f : ι → ULift α) : (⨆ (i : ι), f i).down = ⨆ (i : ι), (f i).down

theorem ULift.up_iSup {α : Type u_1} {ι : Sort u_4} [SupSet α] (f : ι → α) : { down := ⨆ (i : ι), f i } = ⨆ (i : ι), { down := f i }

theorem ULift.down_iInf {α : Type u_1} {ι : Sort u_4} [InfSet α] (f : ι → ULift α) : (⨅ (i : ι), f i).down = ⨅ (i : ι), (f i).down

theorem ULift.up_iInf {α : Type u_1} {ι : Sort u_4} [InfSet α] (f : ι → α) : { down := ⨅ (i : ι), f i } = ⨅ (i : ι), { down := f i }

@[implicit_reducible]

instance ULift.instCompleteLattice {α : Type u_1} [CompleteLattice α] : CompleteLattice (ULift α)

Equations

• ULift.instCompleteLattice = Function.Injective.completeLattice ULift.down ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[implicit_reducible]

instance PUnit.instCompleteLinearOrder : CompleteLinearOrder PUnit

Equations

• One or more equations did not get rendered due to their size.