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 OrderDual.supSet (α : Type u_8) [InfSet α] : SupSet αᵒᵈ

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

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

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_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sSup : Set α → α
• le_sSup (s : Set α) (a : α) : a ∈ s → a ≤ sSup s

  Any element of a set is less than the set supremum.

• sSup_le (s : Set α) (a : α) : (∀ b ∈ s, b ≤ a) → sSup s ≤ a

  Any upper bound is more than the set supremum.

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

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

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

theorem isLUB_iff_sSup_eq {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} : IsLUB s a ↔ sSup 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 le_sSup_of_le {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a b : α} (hb : b ∈ s) (h : a ≤ b) : a ≤ sSup s

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

@[simp]

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

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

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

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

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_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sInf : Set α → α
• sInf_le (s : Set α) (a : α) : a ∈ s → sInf s ≤ a

  Any element of a set is more than the set infimum.

• le_sInf (s : Set α) (a : α) : (∀ b ∈ s, a ≤ b) → a ≤ sInf s

  Any lower bound is less than the set infimum.

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

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

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

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

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 sInf_le_of_le {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a b : α} (hb : b ∈ s) (h : b ≤ a) : sInf s ≤ a

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

@[simp]

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

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

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

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

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

class CompleteLattice (α : Type u_8) extends Lattice α, CompleteSemilatticeSup α, CompleteSemilatticeInf α, Top α, Bot α : Type u_8

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_le (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 α → α
• le_sSup (s : Set α) (a : α) : a ∈ s → a ≤ sSup s
• sSup_le (s : Set α) (a : α) : (∀ b ∈ s, b ≤ a) → sSup s ≤ a
• sInf : Set α → α
• sInf_le (s : Set α) (a : α) : a ∈ s → sInf s ≤ a
• le_sInf (s : Set α) (a : α) : (∀ b ∈ s, a ≤ b) → a ≤ sInf s
• top : α
• bot : α
• le_top (x : α) : x ≤ ⊤

  Any element is less than the top one.

• bot_le (x : α) : ⊥ ≤ x

  Any element is more than the bottom one.

@[instance 100]

instance CompleteLattice.toBoundedOrder {α : Type u_1} [CompleteLattice α] : BoundedOrder α

def completeLatticeOfInf (α : Type u_8) [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 _

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

Any CompleteSemilatticeInf is in fact a CompleteLattice.

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

def completeLatticeOfSup (α : Type u_8) [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 _

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

Any CompleteSemilatticeSup is in fact a CompleteLattice.

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

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

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_le (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 α → α
• le_sSup (s : Set α) (a : α) : a ∈ s → a ≤ sSup s
• sSup_le (s : Set α) (a : α) : (∀ b ∈ s, b ≤ a) → sSup s ≤ a
• sInf : Set α → α
• sInf_le (s : Set α) (a : α) : a ∈ s → sInf s ≤ a
• le_sInf (s : Set α) (a : α) : (∀ b ∈ s, a ≤ b) → a ≤ sInf s
• top : α
• bot : α
• le_top (x : α) : x ≤ ⊤
• bot_le (x : α) : ⊥ ≤ x
• himp : α → α → α
• le_himp_iff (a b c : α) : a ≤ b ⇨ c ↔ min a b ≤ c
• compl : α → α
• himp_bot (a : α) : a ⇨ ⊥ = aᶜ
• sdiff : α → α → α
• hnot : α → α
• sdiff_le_iff (a b c : α) : a \ b ≤ c ↔ a ≤ max b c
• 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 CompleteLinearOrder.toLinearOrder {α : Type u_1} [i : CompleteLinearOrder α] : LinearOrder α

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

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

@[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_4} [SupSet α] (f : ι → α) : OrderDual.toDual (⨆ (i : ι), f i) = ⨅ (i : ι), OrderDual.toDual (f i)

@[simp]

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

@[simp]

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

@[simp]

theorem ofDual_iInf {α : Type u_1} {ι : Sort u_4} [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 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 > ⊥, ∃ a ∈ s, a < b

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

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