Definitions of conditionally complete lattices

A conditionally complete lattice is a lattice in which every non-empty bounded subset s has a least upper bound and a greatest lower bound, denoted below by sSup s and sInf s. Typical examples are ℝ, ℕ, and ℤ with their usual orders.

The theory is very comparable to the theory of complete lattices, except that suitable boundedness and nonemptiness assumptions have to be added to most statements. We express these using the BddAbove and BddBelow predicates, which we use to prove most useful properties of sSup and sInf in conditionally complete lattices.

To differentiate the statements between complete lattices and conditionally complete lattices, we prefix sInf and sSup in the statements by c, giving csInf and csSup. For instance, sInf_le is a statement in complete lattices ensuring sInf s ≤ x, while csInf_le is the same statement in conditionally complete lattices with an additional assumption that s is bounded below.

class ConditionallyCompleteLattice (α : Type u_5) extends Lattice α, SupSet α, InfSet α : Type u_5

A conditionally complete lattice is a lattice in which every nonempty subset which is bounded above has a supremum, and every nonempty subset which is bounded below has an infimum. Typical examples are real numbers or natural numbers.

To differentiate the statements from the corresponding statements in (unconditional) complete lattices, we prefix sInf and sSup by a c everywhere. The same statements should hold in both worlds, sometimes with additional assumptions of nonemptiness or boundedness.

• 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 ≤ SemilatticeSup.sup a b
• le_sup_right : ∀ (a b : α), b ≤ SemilatticeSup.sup a b
• sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → SemilatticeSup.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 α → α
• sInf : Set α → α
• le_csSup : ∀ (s : Set α) (a : α), BddAbove s → a ∈ s → a ≤ sSup s

  a ≤ sSup s for all a ∈ s.

• csSup_le : ∀ (s : Set α) (a : α), s.Nonempty → a ∈ upperBounds s → sSup s ≤ a

  sSup s ≤ a for all a ∈ upperBounds s.

• csInf_le : ∀ (s : Set α) (a : α), BddBelow s → a ∈ s → sInf s ≤ a

  sInf s ≤ a for all a ∈ s.

• le_csInf : ∀ (s : Set α) (a : α), s.Nonempty → a ∈ lowerBounds s → a ≤ sInf s

  a ≤ sInf s for all a ∈ lowerBounds s.

class ConditionallyCompleteLinearOrder (α : Type u_5) extends ConditionallyCompleteLattice α : Type u_5

A conditionally complete linear order is a linear order in which every nonempty subset which is bounded above has a supremum, and every nonempty subset which is bounded below has an infimum. Typical examples are real numbers or natural numbers.

To differentiate the statements from the corresponding statements in (unconditional) complete linear orders, we prefix sInf and sSup by a c everywhere. The same statements should hold in both worlds, sometimes with additional assumptions of nonemptiness or boundedness.

• 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 ≤ SemilatticeSup.sup a b
• le_sup_right : ∀ (a b : α), b ≤ SemilatticeSup.sup a b
• sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → SemilatticeSup.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 α → α
• sInf : Set α → α
• le_csSup : ∀ (s : Set α) (a : α), BddAbove s → a ∈ s → a ≤ sSup s
• csSup_le : ∀ (s : Set α) (a : α), s.Nonempty → a ∈ upperBounds s → sSup s ≤ a
• csInf_le : ∀ (s : Set α) (a : α), BddBelow s → a ∈ s → sInf s ≤ a
• le_csInf : ∀ (s : Set α) (a : α), s.Nonempty → a ∈ lowerBounds s → a ≤ sInf s
• le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a

  A ConditionallyCompleteLinearOrder is total.

• decidableLE : DecidableRel fun (x1 x2 : α) => x1 ≤ x2

  In a ConditionallyCompleteLinearOrder, we assume the order relations are all decidable.

• decidableEq : DecidableEq α

  In a ConditionallyCompleteLinearOrder, we assume the order relations are all decidable.

• decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2

  In a ConditionallyCompleteLinearOrder, we assume the order relations are all decidable.

• csSup_of_not_bddAbove : ∀ (s : Set α), ¬BddAbove s → sSup s = sSup ∅

  If a set is not bounded above, its supremum is by convention sSup ∅.

• csInf_of_not_bddBelow : ∀ (s : Set α), ¬BddBelow s → sInf s = sInf ∅

  If a set is not bounded below, its infimum is by convention sInf ∅.

class ConditionallyCompleteLinearOrderBot (α : Type u_5) extends ConditionallyCompleteLinearOrder α, OrderBot α : Type u_5

A conditionally complete linear order with Bot is a linear order with least element, in which every nonempty subset which is bounded above has a supremum, and every nonempty subset (necessarily bounded below) has an infimum. A typical example is the natural numbers.

To differentiate the statements from the corresponding statements in (unconditional) complete linear orders, we prefix sInf and sSup by a c everywhere. The same statements should hold in both worlds, sometimes with additional assumptions of nonemptiness or boundedness.

• 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 ≤ SemilatticeSup.sup a b
• le_sup_right : ∀ (a b : α), b ≤ SemilatticeSup.sup a b
• sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → SemilatticeSup.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 α → α
• sInf : Set α → α
• le_csSup : ∀ (s : Set α) (a : α), BddAbove s → a ∈ s → a ≤ sSup s
• csSup_le : ∀ (s : Set α) (a : α), s.Nonempty → a ∈ upperBounds s → sSup s ≤ a
• csInf_le : ∀ (s : Set α) (a : α), BddBelow s → a ∈ s → sInf s ≤ a
• le_csInf : ∀ (s : Set α) (a : α), s.Nonempty → a ∈ lowerBounds s → a ≤ sInf s
• le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
• decidableLE : DecidableRel fun (x1 x2 : α) => x1 ≤ x2
• decidableEq : DecidableEq α
• decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
• csSup_of_not_bddAbove : ∀ (s : Set α), ¬BddAbove s → sSup s = sSup ∅
• csInf_of_not_bddBelow : ∀ (s : Set α), ¬BddBelow s → sInf s = sInf ∅
• bot : α
• bot_le : ∀ (a : α), ⊥ ≤ a
• csSup_empty : sSup ∅ = ⊥

  The supremum of the empty set is special-cased to ⊥

@[reducible, inline]

noncomputable abbrev WellFoundedLT.conditionallyCompleteLinearOrderBot (α : Type u_5) [i₁ : LinearOrder α] [i₂ : OrderBot α] [h : WellFoundedLT α] : ConditionallyCompleteLinearOrderBot α

A well founded linear order is conditionally complete, with a bottom element.

Equations

• WellFoundedLT.conditionallyCompleteLinearOrderBot α = ConditionallyCompleteLinearOrderBot.mk ⋯

def conditionallyCompleteLatticeOfsSup (α : Type u_5) [H1 : PartialOrder α] [H2 : SupSet α] (bddAbove_pair : ∀ (a b : α), BddAbove {a, b}) (bddBelow_pair : ∀ (a b : α), BddBelow {a, b}) (isLUB_sSup : ∀ (s : Set α), BddAbove s → s.Nonempty → IsLUB s (sSup s)) : ConditionallyCompleteLattice α

Create a ConditionallyCompleteLattice from a PartialOrder and sup function that returns the least upper bound of a nonempty set which is bounded above. 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 ConditionallyCompleteLattice instance as

instance : ConditionallyCompleteLattice my_T :=
  { inf := better_inf,
    le_inf := ...,
    inf_le_right := ...,
    inf_le_left := ...
    -- don't care to fix sup, sInf
    ..conditionallyCompleteLatticeOfsSup my_T _ }

Equations

• conditionallyCompleteLatticeOfsSup α bddAbove_pair bddBelow_pair isLUB_sSup = ConditionallyCompleteLattice.mk ⋯ ⋯ ⋯ ⋯

def conditionallyCompleteLatticeOfsInf (α : Type u_5) [H1 : PartialOrder α] [H2 : InfSet α] (bddAbove_pair : ∀ (a b : α), BddAbove {a, b}) (bddBelow_pair : ∀ (a b : α), BddBelow {a, b}) (isGLB_sInf : ∀ (s : Set α), BddBelow s → s.Nonempty → IsGLB s (sInf s)) : ConditionallyCompleteLattice α

Create a ConditionallyCompleteLattice from a PartialOrder and inf function that returns the greatest lower bound of a nonempty set which is bounded below. 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 ConditionallyCompleteLattice instance as

instance : ConditionallyCompleteLattice my_T :=
  { inf := better_inf,
    le_inf := ...,
    inf_le_right := ...,
    inf_le_left := ...
    -- don't care to fix sup, sSup
    ..conditionallyCompleteLatticeOfsInf my_T _ }

Equations

• conditionallyCompleteLatticeOfsInf α bddAbove_pair bddBelow_pair isGLB_sInf = ConditionallyCompleteLattice.mk ⋯ ⋯ ⋯ ⋯

def conditionallyCompleteLatticeOfLatticeOfsSup (α : Type u_5) [H1 : Lattice α] [SupSet α] (isLUB_sSup : ∀ (s : Set α), BddAbove s → s.Nonempty → IsLUB s (sSup s)) : ConditionallyCompleteLattice α

A version of conditionallyCompleteLatticeOfsSup when we already know that α is a lattice.

This should only be used when it is both hard and unnecessary to provide inf explicitly.

Equations

• conditionallyCompleteLatticeOfLatticeOfsSup α isLUB_sSup = ConditionallyCompleteLattice.mk ⋯ ⋯ ⋯ ⋯

def conditionallyCompleteLatticeOfLatticeOfsInf (α : Type u_5) [H1 : Lattice α] [InfSet α] (isGLB_sInf : ∀ (s : Set α), BddBelow s → s.Nonempty → IsGLB s (sInf s)) : ConditionallyCompleteLattice α

A version of conditionallyCompleteLatticeOfsInf when we already know that α is a lattice.

This should only be used when it is both hard and unnecessary to provide sup explicitly.

Equations

• conditionallyCompleteLatticeOfLatticeOfsInf α isGLB_sInf = ConditionallyCompleteLattice.mk ⋯ ⋯ ⋯ ⋯