Definition of complete lattices

This file contains the definition of complete lattices with suprema/infima of arbitrary sets.

Main definitions

• sSup and sInf are the supremum and the infimum of a set;
• iSup (f : ι → α) and iInf (f : ι → α) are indexed supremum and infimum of a function, defined as sSup and sInf of the range of this function;
• class CompleteLattice: a bounded lattice such that sSup s is always the least upper boundary of s and sInf s is always the greatest lower boundary of s;
• class CompleteLinearOrder: a linear ordered complete lattice.

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.

@[instance_reducible]

instance OrderDual.supSet (α : Type u_4) [h : InfSet α] : SupSet αᵒᵈ

Equations

• OrderDual.supSet α = { sSup := fun (s : Set αᵒᵈ) => sInf s }

@[instance_reducible]

instance OrderDual.infSet (α : Type u_4) [h : SupSet α] : InfSet αᵒᵈ

Equations

• OrderDual.infSet α = { sInf := fun (s : Set αᵒᵈ) => sSup s }

class CompleteSemilatticeSup (α : Type u_4) extends PartialOrder α, SupSet α : Type u_4

Note that we rarely use CompleteSemilatticeSup (in fact, any such object is always a CompleteLattice, so it's usually best to start there).

Nevertheless it is sometimes a useful intermediate step in constructions.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sSup : Set α → α
• isLUB_sSup (s : Set α) : IsLUB s (sSup s)

  Every set has a least upper bound.

class CompleteSemilatticeInf (α : Type u_4) extends PartialOrder α, InfSet α : Type u_4

Note that we rarely use CompleteSemilatticeInf (in fact, any such object is always a CompleteLattice, so it's usually best to start there).

Nevertheless it is sometimes a useful intermediate step in constructions.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sInf : Set α → α
• isGLB_sInf (s : Set α) : IsGLB s (sInf s)

  Every set has a greatest lower bound.

theorem isLUB_sSup {α : Type u_1} [CompleteSemilatticeSup α] (s : Set α) : IsLUB s (sSup s)

theorem isGLB_sInf {α : Type u_1} [CompleteSemilatticeInf α] (s : Set α) : IsGLB s (sInf s)

theorem le_sSup {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} (h : a ∈ s) : a ≤ sSup s

theorem sInf_le {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} (h : a ∈ s) : sInf s ≤ a

theorem sSup_le {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} (h : ∀ b ∈ s, b ≤ a) : sSup s ≤ a

theorem le_sInf {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} (h : ∀ b ∈ s, a ≤ b) : a ≤ sInf s

theorem isLUB_iff_sSup_eq {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} : IsLUB s a ↔ sSup s = a

theorem isGLB_iff_sInf_eq {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} : IsGLB s a ↔ sInf s = a

theorem IsLUB.sSup_eq {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} : IsLUB s a → sSup s = a

Alias of the forward direction of isLUB_iff_sSup_eq.

theorem IsGLB.sInf_eq {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} : IsGLB s a → sInf s = a

Alias of the forward direction of isGLB_iff_sInf_eq.

theorem sSup_mem_upperBounds {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} : sSup s ∈ upperBounds s

theorem sInf_mem_lowerBounds {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} : sInf s ∈ lowerBounds s

theorem le_sSup_of_le {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a b : α} (hb : b ∈ s) (h : a ≤ b) : a ≤ sSup s

theorem sInf_le_of_le {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a b : α} (hb : b ∈ s) (h : b ≤ a) : sInf s ≤ a

theorem sSup_le_sSup {α : Type u_1} [CompleteSemilatticeSup α] {s t : Set α} (h : s ⊆ t) : sSup s ≤ sSup t

theorem sInf_le_sInf {α : Type u_1} [CompleteSemilatticeInf α] {s t : Set α} (h : s ⊆ t) : sInf t ≤ sInf s

@[simp]

theorem sSup_le_iff {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} : sSup s ≤ a ↔ ∀ b ∈ s, b ≤ a

@[simp]

theorem le_sInf_iff {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} : a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b

theorem le_sSup_iff {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} : a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b

theorem sInf_le_iff {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} : sInf s ≤ a ↔ ∀ b ∈ lowerBounds s, b ≤ a

theorem le_iSup_iff {α : Type u_1} {ι : Sort u_3} [CompleteSemilatticeSup α] {a : α} {s : ι → α} : a ≤ iSup s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b

theorem iInf_le_iff {α : Type u_1} {ι : Sort u_3} [CompleteSemilatticeInf α] {a : α} {s : ι → α} : iInf s ≤ a ↔ ∀ (b : α), (∀ (i : ι), b ≤ s i) → b ≤ a

theorem sSup_lt_iff {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {l : α} : sSup s < l ↔ ∃ b < l, b ∈ upperBounds s

theorem lt_sInf_iff {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {l : α} : l < sInf s ↔ ∃ (b : α), l < b ∧ b ∈ lowerBounds s

theorem iSup_lt_iff {α : Type u_1} {ι : Sort u_3} [CompleteSemilatticeSup α] {l : α} {f : ι → α} : iSup f < l ↔ ∃ b < l, ∀ (i : ι), f i ≤ b

theorem lt_iInf_iff {α : Type u_1} {ι : Sort u_3} [CompleteSemilatticeInf α] {l : α} {f : ι → α} : l < iInf f ↔ ∃ (b : α), l < b ∧ ∀ (i : ι), b ≤ f i

@[instance_reducible]

instance instCompleteSemilatticeSupOrderDualOfCompleteSemilatticeInf {α : Type u_4} [CompleteSemilatticeInf α] : CompleteSemilatticeSup αᵒᵈ

Equations

• instCompleteSemilatticeSupOrderDualOfCompleteSemilatticeInf = { toPartialOrder := OrderDual.instPartialOrder α, toSupSet := OrderDual.supSet α, isLUB_sSup := ⋯ }

@[instance_reducible]

instance instCompleteSemilatticeInfOrderDualOfCompleteSemilatticeSup {α : Type u_4} [CompleteSemilatticeSup α] : CompleteSemilatticeInf αᵒᵈ

Equations

• instCompleteSemilatticeInfOrderDualOfCompleteSemilatticeSup = { toPartialOrder := OrderDual.instPartialOrder α, toInfSet := OrderDual.infSet α, isGLB_sInf := ⋯ }

class CompleteLattice (α : Type u_4) extends Lattice α, CompleteSemilatticeSup α, CompleteSemilatticeInf α, BoundedOrder α : Type u_4

A complete lattice is a bounded lattice which has suprema and infima for every subset.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• sSup : Set α → α
• isLUB_sSup (s : Set α) : IsLUB s (sSup s)
• sInf : Set α → α
• isGLB_sInf (s : Set α) : IsGLB s (sInf s)
• top : α
• le_top (a : α) : a ≤ ⊤
• bot : α
• bot_le (a : α) : ⊥ ≤ a

@[instance_reducible, instance 100]

instance CompleteLattice.toPartialOrder' {α : Type u_1} [CompleteLattice α] : PartialOrder α

Equations

• CompleteLattice.toPartialOrder' = inferInstance

@[instance_reducible]

def completeLatticeOfInf (α : Type u_4) [H1 : PartialOrder α] [H2 : InfSet α] (isGLB_sInf : ∀ (s : Set α), IsGLB s (sInf s)) : CompleteLattice α

Create a CompleteLattice from a PartialOrder and InfSet that returns the greatest lower bound of a set. Usually this constructor provides poor definitional equalities. If other fields are known explicitly, they should be provided; for example, if inf is known explicitly, construct the CompleteLattice instance as

instance : CompleteLattice my_T where
  inf := better_inf
  le_inf := ...
  inf_le_right := ...
  inf_le_left := ...
  -- don't care to fix sup, sSup, bot, top
  __ := completeLatticeOfInf my_T _

Equations

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

@[instance_reducible]

def completeLatticeOfCompleteSemilatticeInf (α : Type u_4) [CompleteSemilatticeInf α] : CompleteLattice α

Any CompleteSemilatticeInf is in fact a CompleteLattice.

Note that this construction has bad definitional properties: see the doc-string on completeLatticeOfInf.

Equations

• completeLatticeOfCompleteSemilatticeInf α = completeLatticeOfInf α ⋯

@[instance_reducible]

def completeLatticeOfSup (α : Type u_4) [H1 : PartialOrder α] [H2 : SupSet α] (isLUB_sSup : ∀ (s : Set α), IsLUB s (sSup s)) : CompleteLattice α

Create a CompleteLattice from a PartialOrder and SupSet that returns the least upper bound of a set. Usually this constructor provides poor definitional equalities. If other fields are known explicitly, they should be provided; for example, if inf is known explicitly, construct the CompleteLattice instance as

instance : CompleteLattice my_T where
  inf := better_inf
  le_inf := ...
  inf_le_right := ...
  inf_le_left := ...
  -- don't care to fix sup, sInf, bot, top
  __ := completeLatticeOfSup my_T _

Equations

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

@[instance_reducible]

def completeLatticeOfCompleteSemilatticeSup (α : Type u_4) [CompleteSemilatticeSup α] : CompleteLattice α

Any CompleteSemilatticeSup is in fact a CompleteLattice.

Note that this construction has bad definitional properties: see the doc-string on completeLatticeOfSup.

Equations

• completeLatticeOfCompleteSemilatticeSup α = completeLatticeOfSup α ⋯

class CompleteLinearOrder (α : Type u_4) extends CompleteLattice α, BiheytingAlgebra α, Ord α : Type u_4

A complete linear order is a linear order whose lattice structure is complete.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• sSup : Set α → α
• isLUB_sSup (s : Set α) : IsLUB s (sSup s)
• sInf : Set α → α
• isGLB_sInf (s : Set α) : IsGLB s (sInf s)
• top : α
• le_top (a : α) : a ≤ ⊤
• bot : α
• bot_le (a : α) : ⊥ ≤ a
• himp : α → α → α
• le_himp_iff (a b c : α) : a ≤ b ⇨ c ↔ min a b ≤ c
• compl : α → α
• himp_bot (a : α) : a ⇨ ⊥ = aᶜ
• sdiff : α → α → α
• sdiff_le_iff (a b c : α) : a \ b ≤ c ↔ a ≤ max b c
• hnot : α → α
• top_sdiff (a : α) : ⊤ \ a = ￢a
• compare : α → α → Ordering
• le_total (a b : α) : a ≤ b ∨ b ≤ a

  A linear order is total.

• toDecidableLE : DecidableLE α

  In a linearly ordered type, we assume the order relations are all decidable.

• toDecidableEq : DecidableEq α

  In a linearly ordered type, we assume the order relations are all decidable.

• toDecidableLT : DecidableLT α

  In a linearly ordered type, we assume the order relations are all decidable.

• compare_eq_compareOfLessAndEq (a b : α) : compare a b = compareOfLessAndEq a b

  Comparison via compare is equal to the canonical comparison given decidable < and =.

@[instance_reducible]

instance CompleteLinearOrder.toLinearOrder {α : Type u_1} [i : CompleteLinearOrder α] : LinearOrder α

Equations

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

@[instance_reducible]

instance OrderDual.instCompleteLattice {α : Type u_1} [CompleteLattice α] : CompleteLattice αᵒᵈ

Equations

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

@[instance_reducible]

instance OrderDual.instCompleteLinearOrder {α : Type u_1} [CompleteLinearOrder α] : CompleteLinearOrder αᵒᵈ

Equations

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

@[simp]

theorem toDual_sSup {α : Type u_1} [SupSet α] (s : Set α) : OrderDual.toDual (sSup s) = sInf (⇑OrderDual.ofDual ⁻¹' s)

@[simp]

theorem toDual_sInf {α : Type u_1} [InfSet α] (s : Set α) : OrderDual.toDual (sInf s) = sSup (⇑OrderDual.ofDual ⁻¹' s)

@[simp]

theorem ofDual_sSup {α : Type u_1} [InfSet α] (s : Set αᵒᵈ) : OrderDual.ofDual (sSup s) = sInf (⇑OrderDual.toDual ⁻¹' s)

@[simp]

theorem ofDual_sInf {α : Type u_1} [SupSet α] (s : Set αᵒᵈ) : OrderDual.ofDual (sInf s) = sSup (⇑OrderDual.toDual ⁻¹' s)

@[simp]

theorem toDual_iSup {α : Type u_1} {ι : Sort u_3} [SupSet α] (f : ι → α) : OrderDual.toDual (⨆ (i : ι), f i) = ⨅ (i : ι), OrderDual.toDual (f i)

@[simp]

theorem toDual_iInf {α : Type u_1} {ι : Sort u_3} [InfSet α] (f : ι → α) : OrderDual.toDual (⨅ (i : ι), f i) = ⨆ (i : ι), OrderDual.toDual (f i)

@[simp]

theorem ofDual_iSup {α : Type u_1} {ι : Sort u_3} [InfSet α] (f : ι → αᵒᵈ) : OrderDual.ofDual (⨆ (i : ι), f i) = ⨅ (i : ι), OrderDual.ofDual (f i)

@[simp]

theorem ofDual_iInf {α : Type u_1} {ι : Sort u_3} [SupSet α] (f : ι → αᵒᵈ) : OrderDual.ofDual (⨅ (i : ι), f i) = ⨆ (i : ι), OrderDual.ofDual (f i)

theorem lt_sSup_iff {α : Type u_1} [CompleteLinearOrder α] {s : Set α} {b : α} : b < sSup s ↔ ∃ a ∈ s, b < a

theorem sInf_lt_iff {α : Type u_1} [CompleteLinearOrder α] {s : Set α} {b : α} : sInf s < b ↔ ∃ a ∈ s, a < b

theorem lt_iSup_iff {α : Type u_1} {ι : Sort u_3} [CompleteLinearOrder α] {a : α} {f : ι → α} : a < iSup f ↔ ∃ (i : ι), a < f i

theorem iInf_lt_iff {α : Type u_1} {ι : Sort u_3} [CompleteLinearOrder α] {a : α} {f : ι → α} : iInf f < a ↔ ∃ (i : ι), f i < a

theorem le_sSup_iff_forall_lt {α : Type u_1} [CompleteLinearOrder α] {s : Set α} {l : α} : l ≤ sSup s ↔ ∀ b < l, ∃ a ∈ s, b < a

theorem sInf_le_iff_forall_lt {α : Type u_1} [CompleteLinearOrder α] {s : Set α} {l : α} : sInf s ≤ l ↔ ∀ (b : α), l < b → ∃ a ∈ s, a < b

theorem le_iSup_iff_forall_lt {α : Type u_1} {ι : Sort u_3} [CompleteLinearOrder α] {l : α} {f : ι → α} : l ≤ iSup f ↔ ∀ b < l, ∃ (i : ι), b < f i

theorem iInf_le_iff_forall_lt {α : Type u_1} {ι : Sort u_3} [CompleteLinearOrder α] {l : α} {f : ι → α} : iInf f ≤ l ↔ ∀ (b : α), l < b → ∃ (i : ι), f i < b

theorem sSup_eq_top {α : Type u_1} [CompleteLinearOrder α] {s : Set α} : sSup s = ⊤ ↔ ∀ b < ⊤, ∃ a ∈ s, b < a

theorem sInf_eq_bot {α : Type u_1} [CompleteLinearOrder α] {s : Set α} : sInf s = ⊥ ↔ ∀ (b : α), ⊥ < b → ∃ a ∈ s, a < b

theorem iSup_eq_top {α : Type u_1} {ι : Sort u_3} [CompleteLinearOrder α] {f : ι → α} : iSup f = ⊤ ↔ ∀ b < ⊤, ∃ (i : ι), b < f i

theorem iInf_eq_bot {α : Type u_1} {ι : Sort u_3} [CompleteLinearOrder α] {f : ι → α} : iInf f = ⊥ ↔ ∀ (b : α), ⊥ < b → ∃ (i : ι), f i < b

theorem lt_biSup_iff {α : Type u_1} {β : Type u_2} [CompleteLinearOrder α] {a : α} {s : Set β} {f : β → α} : a < ⨆ i ∈ s, f i ↔ ∃ i ∈ s, a < f i

theorem lt_biInf_iff {α : Type u_1} {β : Type u_2} [CompleteLinearOrder α] {a : α} {s : Set β} {f : β → α} : ⨅ i ∈ s, f i < a ↔ ∃ i ∈ s, f i < a

@[reducible, inline]

abbrev Equiv.supSet {α : Type u_1} {β : Type u_2} (e : α ≃ β) [SupSet β] : SupSet α

Transfer SupSet across an Equiv.

Equations

• e.supSet = { sSup := fun (s : Set α) => e.symm (⨆ a ∈ s, e a) }

theorem Equiv.supSet_def {α : Type u_1} {β : Type u_2} (e : α ≃ β) [SupSet β] (s : Set α) : sSup s = e.symm (⨆ a ∈ s, e a)

@[reducible, inline]

abbrev Equiv.infSet {α : Type u_1} {β : Type u_2} (e : α ≃ β) [InfSet β] : InfSet α

Transfer InfSet across an Equiv.

Equations

• e.infSet = { sInf := fun (s : Set α) => e.symm (⨅ a ∈ s, e a) }

theorem Equiv.infSet_def {α : Type u_1} {β : Type u_2} (e : α ≃ β) [InfSet β] (s : Set α) : sInf s = e.symm (⨅ a ∈ s, e a)