Sigma conditional completeness

Mathlib's ConditionallyCompleteLattice records Dedekind completeness of a lattice. This file gives vector-lattice characterisations of conditional completeness, introduces the sequential analogue SigmaConditionallyCompleteLattice, and relates these completeness notions to the Archimedean property.

Shared order-completeness lemmas

theorem exists_isLUB_of_pos_of_shift {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {P : Set X → Prop} (hP_image : ∀ {S : Set X} (f : X → X), P S → P (f '' S)) (Hpos : ∀ {S : Set X}, P S → S ⊆ {x : X | 0 ≤ x} → S.Nonempty → BddAbove S → ∃ (x : X), IsLUB S x) {S : Set X} (hPS : P S) (hne : S.Nonempty) (hbdd : BddAbove S) : ∃ (x : X), IsLUB S x

Shift trick: in a lattice-ordered group, given a predicate P preserved under pointwise transformations and a hypothesis producing a least upper bound for P-sets of positive elements, the same hypothesis extends to any P-set that is non-empty and bounded above.

@[reducible]

noncomputable def conditionallyCompleteLatticeOfHasLUB {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (hLUB : ∀ {S : Set X}, S.Nonempty → BddAbove S → ∃ (x : X), IsLUB S x) : ConditionallyCompleteLattice X

Build a ConditionallyCompleteLattice structure from a blanket hypothesis that every non-empty bounded above set has a least upper bound.

Equations

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

theorem exists_isLUB_pos_set_of_pos_net {X : Type u} [AddCommGroup X] [Lattice X] (H : ∀ {ι : Type u} [inst : Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] {u : ι → X}, Monotone u → (∀ (i : ι), 0 ≤ u i) → BddAbove (Set.range u) → ∃ (x : X), IsLUB (Set.range u) x) {S : Set X} (hpos : S ⊆ {x : X | 0 ≤ x}) (hne : S.Nonempty) (hbdd : BddAbove S) : ∃ (x : X), IsLUB S x

From the existence of a least upper bound for every increasing bounded above net of positive elements, deduce the same conclusion for any non-empty bounded above set of positive elements. The net is obtained by indexing over non-empty finite subsets ordered by inclusion.

Characterisations of ConditionallyCompleteLattice

@[reducible]

noncomputable def conditionallyCompleteLatticeOfPosNet (X : Type u) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (H : ∀ {ι : Type u} [inst : Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] {u : ι → X}, Monotone u → (∀ (i : ι), 0 ≤ u i) → BddAbove (Set.range u) → ∃ (x : X), IsLUB (Set.range u) x) : ConditionallyCompleteLattice X

On a lattice-ordered additive commutative group, a ConditionallyCompleteLattice structure exists provided every increasing net of positive elements that is bounded above has a least upper bound. The net is indexed by a type in the same universe as the carrier.

Equations

• conditionallyCompleteLatticeOfPosNet X H = conditionallyCompleteLatticeOfHasLUB ⋯

@[reducible]

noncomputable def conditionallyCompleteLatticeOfPosSet (X : Type u_1) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (H : ∀ {S : Set X}, S ⊆ {x : X | 0 ≤ x} → S.Nonempty → BddAbove S → ∃ (x : X), IsLUB S x) : ConditionallyCompleteLattice X

On a lattice-ordered additive commutative group, a ConditionallyCompleteLattice structure exists provided every non-empty bounded above set of positive elements has a least upper bound.

Equations

• conditionallyCompleteLatticeOfPosSet X H = conditionallyCompleteLatticeOfHasLUB ⋯

Sigma conditional completeness

class SigmaConditionallyCompleteLattice (X : Type u_1) extends Lattice X, SupSet X, InfSet X : Type u_1

A lattice is sigma conditionally complete when non-empty bounded countable subsets admit suprema and infima: for every countable set s, sSup s is the least upper bound if s is bounded above, and sInf s is the greatest lower bound if s is bounded below.

• le : X → X → Prop
• lt : X → X → Prop
• le_refl (a : X) : a ≤ a
• le_trans (a b c : X) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : X) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : X) : a ≤ b → b ≤ a → a = b
• sup : X → X → X
• le_sup_left (a b : X) : a ≤ sup a b
• le_sup_right (a b : X) : b ≤ sup a b
• sup_le (a b c : X) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : X → X → X
• inf_le_left (a b : X) : Lattice.inf a b ≤ a
• inf_le_right (a b : X) : Lattice.inf a b ≤ b
• le_inf (a b c : X) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• sSup : Set X → X
• sInf : Set X → X
• le_csSup (s : Set X) (a : X) : s.Countable → BddAbove s → a ∈ s → a ≤ sSup s
• csSup_le (s : Set X) (a : X) : s.Countable → s.Nonempty → a ∈ upperBounds s → sSup s ≤ a
• csInf_le (s : Set X) (a : X) : s.Countable → BddBelow s → a ∈ s → sInf s ≤ a
• le_csInf (s : Set X) (a : X) : s.Countable → s.Nonempty → a ∈ lowerBounds s → a ≤ sInf s

@[instance_reducible, instance 100]

instance ConditionallyCompleteLattice.toSigmaConditionallyCompleteLattice {X : Type u_1} [ConditionallyCompleteLattice X] : SigmaConditionallyCompleteLattice X

Every conditionally complete lattice is sigma conditionally complete.

Equations

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

Characterisations of sigma conditional completeness

@[reducible]

noncomputable def sigmaConditionallyCompleteLatticeOfHasCountableLUB {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (hLUB : ∀ {S : Set X}, S.Countable → S.Nonempty → BddAbove S → ∃ (x : X), IsLUB S x) : SigmaConditionallyCompleteLattice X

Build a SigmaConditionallyCompleteLattice structure from a hypothesis that every countable non-empty bounded above set has a least upper bound.

Equations

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

theorem exists_isLUB_pos_countable_set_of_pos_seq {X : Type u_1} [AddCommGroup X] [Lattice X] (H : ∀ {u : ℕ → X}, Monotone u → (∀ (n : ℕ), 0 ≤ u n) → BddAbove (Set.range u) → ∃ (x : X), IsLUB (Set.range u) x) {S : Set X} (hpos : S ⊆ {x : X | 0 ≤ x}) (hcount : S.Countable) (hne : S.Nonempty) (hbdd : BddAbove S) : ∃ (x : X), IsLUB S x

From the existence of a least upper bound for every increasing bounded above sequence of positive elements, deduce the same conclusion for every non-empty bounded above countable set of positive elements. The sequence is obtained by enumerating the set and taking finite suprema.

@[reducible]

noncomputable def sigmaConditionallyCompleteLatticeOfPosSeq (X : Type u_1) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (H : ∀ {u : ℕ → X}, Monotone u → (∀ (n : ℕ), 0 ≤ u n) → BddAbove (Set.range u) → ∃ (x : X), IsLUB (Set.range u) x) : SigmaConditionallyCompleteLattice X

On a lattice-ordered additive commutative group, a SigmaConditionallyCompleteLattice structure exists provided every increasing bounded above sequence of positive elements has a least upper bound.

Equations

• sigmaConditionallyCompleteLatticeOfPosSeq X H = sigmaConditionallyCompleteLatticeOfHasCountableLUB ⋯

@[reducible]

noncomputable def sigmaConditionallyCompleteLatticeOfPosCountableSet (X : Type u_1) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (H : ∀ {S : Set X}, S ⊆ {x : X | 0 ≤ x} → S.Countable → S.Nonempty → BddAbove S → ∃ (x : X), IsLUB S x) : SigmaConditionallyCompleteLattice X

On a lattice-ordered additive commutative group, a SigmaConditionallyCompleteLattice structure exists provided every non-empty bounded above countable set of positive elements has a least upper bound.

Equations

• sigmaConditionallyCompleteLatticeOfPosCountableSet X H = sigmaConditionallyCompleteLatticeOfHasCountableLUB ⋯

Archimedean property

theorem IsVLArchimedean_of_sigmaConditionallyCompleteLattice {X : Type u_1} [SigmaConditionallyCompleteLattice X] [AddCommGroup X] [IsOrderedAddMonoid X] : IsVLArchimedean X

Every sigma conditionally complete lattice-ordered group is Archimedean in the vector-lattice sense.