# 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.

source
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_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 α → α
- 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`.

Instances

source
class ConditionallyCompleteLinearOrder (α : Type u_5) extends ConditionallyCompleteLattice α, Ord α :
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_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 α → α
- 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
- compare : α → α → Ordering
- le_total (a b : α) : a ≤ b ∨ b ≤ a

  A `ConditionallyCompleteLinearOrder` is total.

- toDecidableLE : DecidableLE α

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

- toDecidableEq : DecidableEq α

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

- toDecidableLT : DecidableLT α

  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 ∅`.

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

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

Instances

source
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_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 α → α
- 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
- compare : α → α → Ordering
- le_total (a b : α) : a ≤ b ∨ b ≤ a
- toDecidableLE : DecidableLE α
- toDecidableEq : DecidableEq α
- toDecidableLT : DecidableLT α
- csSup_of_not_bddAbove (s : Set α) : ¬BddAbove s → sSup s = sSup ∅
- csInf_of_not_bddBelow (s : Set α) : ¬BddBelow s → sInf s = sInf ∅
- compare_eq_compareOfLessAndEq (a b : α) : compare a b = compareOfLessAndEq a b
- bot : α
- bot_le (a : α) : ⊥ ≤ a
- csSup_empty : sSup ∅ = ⊥

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

Instances

source
@[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

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

Instances For

source
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

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

Instances For

source
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

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

Instances For

source
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

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

Instances For

source
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

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

Instances For