Documentation

Mathlib.Order.ConditionallyCompleteLattice.Basic

Theory 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 introduce two predicates BddAbove and BddBelow to express this boundedness, prove their basic properties, and then go on 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.

Extension of sSup and sInf from a preorder α to WithTop α and WithBot α

noncomputable instance WithTop.instSupSet {α : Type u_5} [Preorder α] [SupSet α] :
Equations
noncomputable instance WithTop.instInfSet {α : Type u_5} [InfSet α] :
Equations
  • WithTop.instInfSet = { sInf := fun S => if S {} then else ↑(sInf ((fun a => a) ⁻¹' S)) }
noncomputable instance WithBot.instSupSet {α : Type u_5} [SupSet α] :
Equations
  • WithBot.instSupSet = { sSup := sInf }
noncomputable instance WithBot.instInfSet {α : Type u_5} [Preorder α] [InfSet α] :
Equations
  • WithBot.instInfSet = { sInf := sSup }
theorem WithTop.sSup_eq {α : Type u_1} [Preorder α] [SupSet α] {s : Set (WithTop α)} (hs : ¬ s) (hs' : BddAbove (WithTop.some ⁻¹' s)) :
sSup s = ↑(sSup (WithTop.some ⁻¹' s))
theorem WithTop.sInf_eq {α : Type u_1} [InfSet α] {s : Set (WithTop α)} (hs : ¬s {}) :
sInf s = ↑(sInf (WithTop.some ⁻¹' s))
theorem WithBot.sInf_eq {α : Type u_1} [Preorder α] [InfSet α] {s : Set (WithBot α)} (hs : ¬ s) (hs' : BddBelow (WithBot.some ⁻¹' s)) :
sInf s = ↑(sInf (WithBot.some ⁻¹' s))
theorem WithBot.sSup_eq {α : Type u_1} [SupSet α] {s : Set (WithBot α)} (hs : ¬s {}) :
sSup s = ↑(sSup (WithBot.some ⁻¹' s))
@[simp]
theorem WithTop.sInf_empty {α : Type u_5} [InfSet α] :
@[simp]
theorem WithTop.iInf_empty {ι : Sort u_4} {α : Type u_5} [IsEmpty ι] [InfSet α] (f : ιWithTop α) :
⨅ (i : ι), f i =
theorem WithTop.coe_sInf' {α : Type u_1} [InfSet α] {s : Set α} (hs : Set.Nonempty s) :
↑(sInf s) = sInf ((fun a => a) '' s)
theorem WithTop.coe_iInf {α : Type u_1} {ι : Sort u_4} [Nonempty ι] [InfSet α] (f : ια) :
↑(⨅ (i : ι), f i) = ⨅ (i : ι), ↑(f i)
theorem WithTop.coe_sSup' {α : Type u_1} [Preorder α] [SupSet α] {s : Set α} (hs : BddAbove s) :
↑(sSup s) = sSup ((fun a => a) '' s)
theorem WithTop.coe_iSup {α : Type u_1} {ι : Sort u_4} [Preorder α] [SupSet α] (f : ια) (h : BddAbove (Set.range f)) :
↑(⨆ (i : ι), f i) = ⨆ (i : ι), ↑(f i)
@[simp]
theorem WithBot.csSup_empty {α : Type u_5} [SupSet α] :
@[simp]
theorem WithBot.ciSup_empty {ι : Sort u_4} {α : Type u_5} [IsEmpty ι] [SupSet α] (f : ιWithBot α) :
⨆ (i : ι), f i =
theorem WithBot.coe_sSup' {α : Type u_1} [SupSet α] {s : Set α} (hs : Set.Nonempty s) :
↑(sSup s) = sSup ((fun a => a) '' s)
theorem WithBot.coe_iSup {α : Type u_1} {ι : Sort u_4} [Nonempty ι] [SupSet α] (f : ια) :
↑(⨆ (i : ι), f i) = ⨆ (i : ι), ↑(f i)
theorem WithBot.coe_sInf' {α : Type u_1} [Preorder α] [InfSet α] {s : Set α} (hs : BddBelow s) :
↑(sInf s) = sInf ((fun a => a) '' s)
theorem WithBot.coe_iInf {α : Type u_1} {ι : Sort u_4} [Preorder α] [InfSet α] (f : ια) (h : BddBelow (Set.range f)) :
↑(⨅ (i : ι), f i) = ⨅ (i : ι), ↑(f i)
class ConditionallyCompleteLattice (α : Type u_5) extends Lattice , SupSet , InfSet :
Type u_5
  • sup : ααα
  • le : ααProp
  • lt : ααProp
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • le_sup_left : ∀ (a b : α), a a b
  • le_sup_right : ∀ (a b : α), b a b
  • sup_le : ∀ (a b c : α), a cb ca b c
  • inf : ααα
  • inf_le_left : ∀ (a b : α), a b a
  • inf_le_right : ∀ (a b : α), a b b
  • le_inf : ∀ (a b c : α), a ba ca b c
  • sSup : Set αα
  • sInf : Set αα
  • le_csSup : ∀ (s_1 : Set α) (a : α), BddAbove s_1a s_1a sSup s_1

    a ≤ sSup s for all a ∈ s.

  • csSup_le : ∀ (s_1 : Set α) (a : α), Set.Nonempty s_1a upperBounds s_1sSup s_1 a

    sSup s ≤ a for all a ∈ upperBounds s.

  • csInf_le : ∀ (s_1 : Set α) (a : α), BddBelow s_1a s_1sInf s_1 a

    sInf s ≤ a for all a ∈ s.

  • le_csInf : ∀ (s_1 : Set α) (a : α), Set.Nonempty s_1a lowerBounds s_1a sInf s_1

    a ≤ sInf s for all a ∈ lowerBounds s.

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 subₛ by a c everywhere. The same statements should hold in both worlds, sometimes with additional assumptions of nonemptiness or boundedness.

Instances

    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.

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

      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.

      Instances
        Equations
        • ConditionallyCompleteLinearOrderBot.toOrderBot = OrderBot.mk (_ : ∀ (x : α), x)

        A complete lattice is a conditionally complete lattice, as there are no restrictions on the properties of sInf and sSup in a complete lattice.

        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        • One or more equations did not get rendered due to their size.
        @[reducible]
        noncomputable def IsWellOrder.conditionallyCompleteLinearOrderBot (α : Type u_5) [i₁ : LinearOrder α] [i₂ : OrderBot α] [h : IsWellOrder α fun x x_1 => x < x_1] :

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

        Equations
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          • One or more equations did not get rendered due to their size.
          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 sSet.Nonempty sIsLUB s (sSup s)) :

          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
            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 sSet.Nonempty sIsGLB s (sInf s)) :

            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
              def conditionallyCompleteLatticeOfLatticeOfsSup (α : Type u_5) [H1 : Lattice α] [SupSet α] (isLUB_sSup : ∀ (s : Set α), BddAbove sSet.Nonempty sIsLUB s (sSup s)) :

              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
                def conditionallyCompleteLatticeOfLatticeOfsInf (α : Type u_5) [H1 : Lattice α] [InfSet α] (isGLB_sInf : ∀ (s : Set α), BddBelow sSet.Nonempty sIsGLB s (sInf s)) :

                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
                  theorem le_csSup {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (h₁ : BddAbove s) (h₂ : a s) :
                  a sSup s
                  theorem csSup_le {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (h₁ : Set.Nonempty s) (h₂ : ∀ (b : α), b sb a) :
                  sSup s a
                  theorem csInf_le {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (h₁ : BddBelow s) (h₂ : a s) :
                  sInf s a
                  theorem le_csInf {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (h₁ : Set.Nonempty s) (h₂ : ∀ (b : α), b sa b) :
                  a sInf s
                  theorem le_csSup_of_le {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} {b : α} (hs : BddAbove s) (hb : b s) (h : a b) :
                  a sSup s
                  theorem csInf_le_of_le {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} {b : α} (hs : BddBelow s) (hb : b s) (h : b a) :
                  sInf s a
                  theorem csSup_le_csSup {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {t : Set α} (ht : BddAbove t) (hs : Set.Nonempty s) (h : s t) :
                  theorem csInf_le_csInf {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {t : Set α} (ht : BddBelow t) (hs : Set.Nonempty s) (h : s t) :
                  theorem le_csSup_iff {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (h : BddAbove s) (hs : Set.Nonempty s) :
                  a sSup s ∀ (b : α), b upperBounds sa b
                  theorem csInf_le_iff {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (h : BddBelow s) (hs : Set.Nonempty s) :
                  sInf s a ∀ (b : α), b lowerBounds sb a
                  theorem isLUB_csSup {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (ne : Set.Nonempty s) (H : BddAbove s) :
                  IsLUB s (sSup s)
                  theorem isLUB_ciSup {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] [Nonempty ι] {f : ια} (H : BddAbove (Set.range f)) :
                  IsLUB (Set.range f) (⨆ (i : ι), f i)
                  theorem isLUB_ciSup_set {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : βα} {s : Set β} (H : BddAbove (f '' s)) (Hne : Set.Nonempty s) :
                  IsLUB (f '' s) (⨆ (i : s), f i)
                  theorem isGLB_csInf {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (ne : Set.Nonempty s) (H : BddBelow s) :
                  IsGLB s (sInf s)
                  theorem isGLB_ciInf {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] [Nonempty ι] {f : ια} (H : BddBelow (Set.range f)) :
                  IsGLB (Set.range f) (⨅ (i : ι), f i)
                  theorem isGLB_ciInf_set {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : βα} {s : Set β} (H : BddBelow (f '' s)) (Hne : Set.Nonempty s) :
                  IsGLB (f '' s) (⨅ (i : s), f i)
                  theorem ciSup_le_iff {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] [Nonempty ι] {f : ια} {a : α} (hf : BddAbove (Set.range f)) :
                  iSup f a ∀ (i : ι), f i a
                  theorem le_ciInf_iff {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] [Nonempty ι] {f : ια} {a : α} (hf : BddBelow (Set.range f)) :
                  a iInf f ∀ (i : ι), a f i
                  theorem ciSup_set_le_iff {α : Type u_1} [ConditionallyCompleteLattice α] {ι : Type u_5} {s : Set ι} {f : ια} {a : α} (hs : Set.Nonempty s) (hf : BddAbove (f '' s)) :
                  ⨆ (i : s), f i a ∀ (i : ι), i sf i a
                  theorem le_ciInf_set_iff {α : Type u_1} [ConditionallyCompleteLattice α] {ι : Type u_5} {s : Set ι} {f : ια} {a : α} (hs : Set.Nonempty s) (hf : BddBelow (f '' s)) :
                  a ⨅ (i : s), f i ∀ (i : ι), i sa f i
                  theorem IsLUB.csSup_eq {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsLUB s a) (ne : Set.Nonempty s) :
                  sSup s = a
                  theorem IsLUB.ciSup_eq {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] {a : α} [Nonempty ι] {f : ια} (H : IsLUB (Set.range f) a) :
                  ⨆ (i : ι), f i = a
                  theorem IsLUB.ciSup_set_eq {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {a : α} {s : Set β} {f : βα} (H : IsLUB (f '' s) a) (Hne : Set.Nonempty s) :
                  ⨆ (i : s), f i = a
                  theorem IsGreatest.csSup_eq {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsGreatest s a) :
                  sSup s = a

                  A greatest element of a set is the supremum of this set.

                  theorem IsGreatest.csSup_mem {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsGreatest s a) :
                  sSup s s
                  theorem IsGLB.csInf_eq {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsGLB s a) (ne : Set.Nonempty s) :
                  sInf s = a
                  theorem IsGLB.ciInf_eq {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] {a : α} [Nonempty ι] {f : ια} (H : IsGLB (Set.range f) a) :
                  ⨅ (i : ι), f i = a
                  theorem IsGLB.ciInf_set_eq {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {a : α} {s : Set β} {f : βα} (H : IsGLB (f '' s) a) (Hne : Set.Nonempty s) :
                  ⨅ (i : s), f i = a
                  theorem IsLeast.csInf_eq {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsLeast s a) :
                  sInf s = a

                  A least element of a set is the infimum of this set.

                  theorem IsLeast.csInf_mem {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsLeast s a) :
                  sInf s s
                  theorem subset_Icc_csInf_csSup {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (hb : BddBelow s) (ha : BddAbove s) :
                  s Set.Icc (sInf s) (sSup s)
                  theorem csSup_le_iff {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (hb : BddAbove s) (hs : Set.Nonempty s) :
                  sSup s a ∀ (b : α), b sb a
                  theorem le_csInf_iff {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (hb : BddBelow s) (hs : Set.Nonempty s) :
                  a sInf s ∀ (b : α), b sa b
                  theorem not_mem_of_lt_csInf {α : Type u_1} [ConditionallyCompleteLattice α] {x : α} {s : Set α} (h : x < sInf s) (hs : BddBelow s) :
                  ¬x s
                  theorem not_mem_of_csSup_lt {α : Type u_1} [ConditionallyCompleteLattice α] {x : α} {s : Set α} (h : sSup s < x) (hs : BddAbove s) :
                  ¬x s
                  theorem csSup_eq_of_forall_le_of_forall_lt_exists_gt {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {b : α} (hs : Set.Nonempty s) (H : ∀ (a : α), a sa b) (H' : ∀ (w : α), w < ba, a s w < a) :
                  sSup s = b

                  Introduction rule to prove that b is the supremum of s: it suffices to check that b is larger than all elements of s, and that this is not the case of any w. See sSup_eq_of_forall_le_of_forall_lt_exists_gt for a version in complete lattices.

                  theorem csInf_eq_of_forall_ge_of_forall_gt_exists_lt {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {b : α} :
                  Set.Nonempty s(∀ (a : α), a sb a) → (∀ (w : α), b < wa, a s a < w) → sInf s = b

                  Introduction rule to prove that b is the infimum of s: it suffices to check that b is smaller than all elements of s, and that this is not the case of any w>b. See sInf_eq_of_forall_ge_of_forall_gt_exists_lt for a version in complete lattices.

                  theorem lt_csSup_of_lt {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} {b : α} (hs : BddAbove s) (ha : a s) (h : b < a) :
                  b < sSup s

                  b < sSup s when there is an element a in s with b < a, when s is bounded above. This is essentially an iff, except that the assumptions for the two implications are slightly different (one needs boundedness above for one direction, nonemptiness and linear order for the other one), so we formulate separately the two implications, contrary to the CompleteLattice case.

                  theorem csInf_lt_of_lt {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} {b : α} :
                  BddBelow sa sa < bsInf s < b

                  sInf s < b when there is an element a in s with a < b, when s is bounded below. This is essentially an iff, except that the assumptions for the two implications are slightly different (one needs boundedness below for one direction, nonemptiness and linear order for the other one), so we formulate separately the two implications, contrary to the CompleteLattice case.

                  theorem exists_between_of_forall_le {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {t : Set α} (sne : Set.Nonempty s) (tne : Set.Nonempty t) (hst : ∀ (x : α), x s∀ (y : α), y tx y) :

                  If all elements of a nonempty set s are less than or equal to all elements of a nonempty set t, then there exists an element between these sets.

                  @[simp]
                  theorem csSup_singleton {α : Type u_1} [ConditionallyCompleteLattice α] (a : α) :
                  sSup {a} = a

                  The supremum of a singleton is the element of the singleton

                  @[simp]
                  theorem csInf_singleton {α : Type u_1} [ConditionallyCompleteLattice α] (a : α) :
                  sInf {a} = a

                  The infimum of a singleton is the element of the singleton

                  @[simp]
                  theorem csSup_pair {α : Type u_1} [ConditionallyCompleteLattice α] (a : α) (b : α) :
                  sSup {a, b} = a b
                  @[simp]
                  theorem csInf_pair {α : Type u_1} [ConditionallyCompleteLattice α] (a : α) (b : α) :
                  sInf {a, b} = a b
                  theorem csInf_le_csSup {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (hb : BddBelow s) (ha : BddAbove s) (ne : Set.Nonempty s) :

                  If a set is bounded below and above, and nonempty, its infimum is less than or equal to its supremum.

                  theorem csSup_union {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {t : Set α} (hs : BddAbove s) (sne : Set.Nonempty s) (ht : BddAbove t) (tne : Set.Nonempty t) :
                  sSup (s t) = sSup s sSup t

                  The sSup of a union of two sets is the max of the suprema of each subset, under the assumptions that all sets are bounded above and nonempty.

                  theorem csInf_union {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {t : Set α} (hs : BddBelow s) (sne : Set.Nonempty s) (ht : BddBelow t) (tne : Set.Nonempty t) :
                  sInf (s t) = sInf s sInf t

                  The sInf of a union of two sets is the min of the infima of each subset, under the assumptions that all sets are bounded below and nonempty.

                  theorem csSup_inter_le {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {t : Set α} (hs : BddAbove s) (ht : BddAbove t) (hst : Set.Nonempty (s t)) :
                  sSup (s t) sSup s sSup t

                  The supremum of an intersection of two sets is bounded by the minimum of the suprema of each set, if all sets are bounded above and nonempty.

                  theorem le_csInf_inter {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {t : Set α} :
                  BddBelow sBddBelow tSet.Nonempty (s t)sInf s sInf t sInf (s t)

                  The infimum of an intersection of two sets is bounded below by the maximum of the infima of each set, if all sets are bounded below and nonempty.

                  theorem csSup_insert {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (hs : BddAbove s) (sne : Set.Nonempty s) :
                  sSup (insert a s) = a sSup s

                  The supremum of insert a s is the maximum of a and the supremum of s, if s is nonempty and bounded above.

                  theorem csInf_insert {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (hs : BddBelow s) (sne : Set.Nonempty s) :
                  sInf (insert a s) = a sInf s

                  The infimum of insert a s is the minimum of a and the infimum of s, if s is nonempty and bounded below.

                  @[simp]
                  theorem csInf_Icc {α : Type u_1} [ConditionallyCompleteLattice α] {a : α} {b : α} (h : a b) :
                  sInf (Set.Icc a b) = a
                  @[simp]
                  theorem csInf_Ici {α : Type u_1} [ConditionallyCompleteLattice α] {a : α} :
                  sInf (Set.Ici a) = a
                  @[simp]
                  theorem csInf_Ico {α : Type u_1} [ConditionallyCompleteLattice α] {a : α} {b : α} (h : a < b) :
                  sInf (Set.Ico a b) = a
                  @[simp]
                  theorem csInf_Ioc {α : Type u_1} [ConditionallyCompleteLattice α] {a : α} {b : α} [DenselyOrdered α] (h : a < b) :
                  sInf (Set.Ioc a b) = a
                  @[simp]
                  theorem csInf_Ioi {α : Type u_1} [ConditionallyCompleteLattice α] {a : α} [NoMaxOrder α] [DenselyOrdered α] :
                  sInf (Set.Ioi a) = a
                  @[simp]
                  theorem csInf_Ioo {α : Type u_1} [ConditionallyCompleteLattice α] {a : α} {b : α} [DenselyOrdered α] (h : a < b) :
                  sInf (Set.Ioo a b) = a
                  @[simp]
                  theorem csSup_Icc {α : Type u_1} [ConditionallyCompleteLattice α] {a : α} {b : α} (h : a b) :
                  sSup (Set.Icc a b) = b
                  @[simp]
                  theorem csSup_Ico {α : Type u_1} [ConditionallyCompleteLattice α] {a : α} {b : α} [DenselyOrdered α] (h : a < b) :
                  sSup (Set.Ico a b) = b
                  @[simp]
                  theorem csSup_Iic {α : Type u_1} [ConditionallyCompleteLattice α] {a : α} :
                  sSup (Set.Iic a) = a
                  @[simp]
                  theorem csSup_Iio {α : Type u_1} [ConditionallyCompleteLattice α] {a : α} [NoMinOrder α] [DenselyOrdered α] :
                  sSup (Set.Iio a) = a
                  @[simp]
                  theorem csSup_Ioc {α : Type u_1} [ConditionallyCompleteLattice α] {a : α} {b : α} (h : a < b) :
                  sSup (Set.Ioc a b) = b
                  @[simp]
                  theorem csSup_Ioo {α : Type u_1} [ConditionallyCompleteLattice α] {a : α} {b : α} [DenselyOrdered α] (h : a < b) :
                  sSup (Set.Ioo a b) = b
                  theorem ciSup_le {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] [Nonempty ι] {f : ια} {c : α} (H : ∀ (x : ι), f x c) :
                  iSup f c

                  The indexed supremum of a function is bounded above by a uniform bound

                  theorem le_ciSup {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] {f : ια} (H : BddAbove (Set.range f)) (c : ι) :
                  f c iSup f

                  The indexed supremum of a function is bounded below by the value taken at one point

                  theorem le_ciSup_of_le {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] {a : α} {f : ια} (H : BddAbove (Set.range f)) (c : ι) (h : a f c) :
                  a iSup f
                  theorem ciSup_mono {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] {f : ια} {g : ια} (B : BddAbove (Set.range g)) (H : ∀ (x : ι), f x g x) :

                  The indexed supremum of two functions are comparable if the functions are pointwise comparable

                  theorem le_ciSup_set {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : βα} {s : Set β} (H : BddAbove (f '' s)) {c : β} (hc : c s) :
                  f c ⨆ (i : s), f i
                  theorem ciInf_mono {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] {f : ια} {g : ια} (B : BddBelow (Set.range f)) (H : ∀ (x : ι), f x g x) :

                  The indexed infimum of two functions are comparable if the functions are pointwise comparable

                  theorem le_ciInf {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] [Nonempty ι] {f : ια} {c : α} (H : ∀ (x : ι), c f x) :
                  c iInf f

                  The indexed minimum of a function is bounded below by a uniform lower bound

                  theorem ciInf_le {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] {f : ια} (H : BddBelow (Set.range f)) (c : ι) :
                  iInf f f c

                  The indexed infimum of a function is bounded above by the value taken at one point

                  theorem ciInf_le_of_le {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] {a : α} {f : ια} (H : BddBelow (Set.range f)) (c : ι) (h : f c a) :
                  iInf f a
                  theorem ciInf_set_le {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : βα} {s : Set β} (H : BddBelow (f '' s)) {c : β} (hc : c s) :
                  ⨅ (i : s), f i f c
                  @[simp]
                  theorem ciSup_const {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] [hι : Nonempty ι] {a : α} :
                  ⨆ (x : ι), a = a
                  @[simp]
                  theorem ciInf_const {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] [Nonempty ι] {a : α} :
                  ⨅ (x : ι), a = a
                  @[simp]
                  theorem ciSup_unique {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] [Unique ι] {s : ια} :
                  ⨆ (i : ι), s i = s default
                  @[simp]
                  theorem ciInf_unique {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] [Unique ι] {s : ια} :
                  ⨅ (i : ι), s i = s default
                  theorem ciSup_subsingleton {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] [Subsingleton ι] (i : ι) (s : ια) :
                  ⨆ (i : ι), s i = s i
                  theorem ciInf_subsingleton {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] [Subsingleton ι] (i : ι) (s : ια) :
                  ⨅ (i : ι), s i = s i
                  @[simp]
                  theorem ciSup_pos {α : Type u_1} [ConditionallyCompleteLattice α] {p : Prop} {f : pα} (hp : p) :
                  ⨆ (h : p), f h = f hp
                  @[simp]
                  theorem ciInf_pos {α : Type u_1} [ConditionallyCompleteLattice α] {p : Prop} {f : pα} (hp : p) :
                  ⨅ (h : p), f h = f hp
                  theorem ciSup_neg {α : Type u_1} [ConditionallyCompleteLattice α] {p : Prop} {f : pα} (hp : ¬p) :
                  ⨆ (h : p), f h = sSup
                  theorem ciInf_neg {α : Type u_1} [ConditionallyCompleteLattice α] {p : Prop} {f : pα} (hp : ¬p) :
                  ⨅ (h : p), f h = sInf
                  theorem ciSup_eq_ite {α : Type u_1} [ConditionallyCompleteLattice α] {p : Prop} [Decidable p] {f : pα} :
                  ⨆ (h : p), f h = if h : p then f h else sSup
                  theorem ciInf_eq_ite {α : Type u_1} [ConditionallyCompleteLattice α] {p : Prop} [Decidable p] {f : pα} :
                  ⨅ (h : p), f h = if h : p then f h else sInf
                  theorem cbiSup_eq_of_forall {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] {p : ιProp} {f : Subtype pα} (hp : (i : ι) → p i) :
                  ⨆ (i : ι) (h : p i), f { val := i, property := h } = iSup f
                  theorem cbiInf_eq_of_forall {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] {p : ιProp} {f : Subtype pα} (hp : (i : ι) → p i) :
                  ⨅ (i : ι) (h : p i), f { val := i, property := h } = iInf f
                  theorem ciSup_eq_of_forall_le_of_forall_lt_exists_gt {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] {b : α} [Nonempty ι] {f : ια} (h₁ : ∀ (i : ι), f i b) (h₂ : ∀ (w : α), w < bi, w < f i) :
                  ⨆ (i : ι), f i = b

                  Introduction rule to prove that b is the supremum of f: it suffices to check that b is larger than f i for all i, and that this is not the case of any w. See iSup_eq_of_forall_le_of_forall_lt_exists_gt for a version in complete lattices.

                  theorem ciInf_eq_of_forall_ge_of_forall_gt_exists_lt {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] {b : α} [Nonempty ι] {f : ια} (h₁ : ∀ (i : ι), b f i) (h₂ : ∀ (w : α), b < wi, f i < w) :
                  ⨅ (i : ι), f i = b

                  Introduction rule to prove that b is the infimum of f: it suffices to check that b is smaller than f i for all i, and that this is not the case of any w>b. See iInf_eq_of_forall_ge_of_forall_gt_exists_lt for a version in complete lattices.

                  theorem Monotone.ciSup_mem_Inter_Icc_of_antitone {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [SemilatticeSup β] {f : βα} {g : βα} (hf : Monotone f) (hg : Antitone g) (h : f g) :
                  ⨆ (n : β), f n ⋂ (n : β), Set.Icc (f n) (g n)

                  Nested intervals lemma: if f is a monotone sequence, g is an antitone sequence, and f n ≤ g n for all n, then ⨆ n, f n belongs to all the intervals [f n, g n].

                  theorem ciSup_mem_Inter_Icc_of_antitone_Icc {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [SemilatticeSup β] {f : βα} {g : βα} (h : Antitone fun n => Set.Icc (f n) (g n)) (h' : ∀ (n : β), f n g n) :
                  ⨆ (n : β), f n ⋂ (n : β), Set.Icc (f n) (g n)

                  Nested intervals lemma: if [f n, g n] is an antitone sequence of nonempty closed intervals, then ⨆ n, f n belongs to all the intervals [f n, g n].

                  theorem csSup_eq_of_is_forall_le_of_forall_le_imp_ge {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {b : α} (hs : Set.Nonempty s) (h_is_ub : ∀ (a : α), a sa b) (h_b_le_ub : ∀ (ub : α), (∀ (a : α), a sa ub) → b ub) :
                  sSup s = b

                  Introduction rule to prove that b is the supremum of s: it suffices to check that

                  1. b is an upper bound
                  2. every other upper bound b' satisfies b ≤ b'.
                  theorem Set.Iic_ciInf {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] [Nonempty ι] {f : ια} (hf : BddBelow (Set.range f)) :
                  Set.Iic (⨅ (i : ι), f i) = ⋂ (i : ι), Set.Iic (f i)
                  theorem Set.Ici_ciSup {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] [Nonempty ι] {f : ια} (hf : BddAbove (Set.range f)) :
                  Set.Ici (⨆ (i : ι), f i) = ⋂ (i : ι), Set.Ici (f i)
                  instance Pi.conditionallyCompleteLattice {ι : Type u_5} {α : ιType u_6} [(i : ι) → ConditionallyCompleteLattice (α i)] :
                  ConditionallyCompleteLattice ((i : ι) → α i)
                  Equations
                  • One or more equations did not get rendered due to their size.
                  theorem exists_lt_of_lt_csSup {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} {b : α} (hs : Set.Nonempty s) (hb : b < sSup s) :
                  a, a s b < a

                  When b < sSup s, there is an element a in s with b < a, if s is nonempty and the order is a linear order.

                  theorem exists_lt_of_lt_ciSup {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrder α] {b : α} [Nonempty ι] {f : ια} (h : b < iSup f) :
                  i, b < f i

                  Indexed version of the above lemma exists_lt_of_lt_csSup. When b < iSup f, there is an element i such that b < f i.

                  theorem exists_lt_of_csInf_lt {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} {b : α} (hs : Set.Nonempty s) (hb : sInf s < b) :
                  a, a s a < b

                  When sInf s < b, there is an element a in s with a < b, if s is nonempty and the order is a linear order.

                  theorem exists_lt_of_ciInf_lt {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrder α] {a : α} [Nonempty ι] {f : ια} (h : iInf f < a) :
                  i, f i < a

                  Indexed version of the above lemma exists_lt_of_csInf_lt When iInf f < a, there is an element i such that f i < a.

                  theorem csSup_eq_csSup_of_forall_exists_le {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} {t : Set α} (hs : ∀ (x : α), x sy, y t x y) (ht : ∀ (y : α), y tx, x s y x) :
                  sSup s = sSup t

                  When every element of a set s is bounded by an element of a set t, and conversely, then s and t have the same supremum. This holds even when the sets may be empty or unbounded.

                  theorem csInf_eq_csInf_of_forall_exists_le {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} {t : Set α} (hs : ∀ (x : α), x sy, y t y x) (ht : ∀ (y : α), y tx, x s x y) :
                  sInf s = sInf t

                  When every element of a set s is bounded by an element of a set t, and conversely, then s and t have the same supremum. This holds even when the sets may be empty or unbounded.

                  theorem sSup_iUnion_Iic {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrder α] (f : ια) :
                  sSup (⋃ (i : ι), Set.Iic (f i)) = ⨆ (i : ι), f i
                  theorem sInf_iUnion_Ici {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrder α] (f : ια) :
                  sInf (⋃ (i : ι), Set.Ici (f i)) = ⨅ (i : ι), f i
                  theorem cbiSup_eq_of_not_forall {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrder α] {p : ιProp} {f : Subtype pα} (hp : ¬((i : ι) → p i)) :
                  ⨆ (i : ι) (h : p i), f { val := i, property := h } = iSup f sSup
                  theorem cbiInf_eq_of_not_forall {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrder α] {p : ιProp} {f : Subtype pα} (hp : ¬((i : ι) → p i)) :
                  ⨅ (i : ι) (h : p i), f { val := i, property := h } = iInf f sInf
                  theorem sInf_eq_argmin_on {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} [IsWellOrder α fun x x_1 => x < x_1] (hs : Set.Nonempty s) :
                  sInf s = Function.argminOn id (_ : WellFounded fun x x_1 => x < x_1) s hs
                  theorem isLeast_csInf {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} [IsWellOrder α fun x x_1 => x < x_1] (hs : Set.Nonempty s) :
                  theorem le_csInf_iff' {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} {b : α} [IsWellOrder α fun x x_1 => x < x_1] (hs : Set.Nonempty s) :
                  theorem csInf_mem {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} [IsWellOrder α fun x x_1 => x < x_1] (hs : Set.Nonempty s) :
                  sInf s s
                  theorem ciInf_mem {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrder α] [IsWellOrder α fun x x_1 => x < x_1] [Nonempty ι] (f : ια) :
                  theorem MonotoneOn.map_csInf {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} [IsWellOrder α fun x x_1 => x < x_1] {β : Type u_5} [ConditionallyCompleteLattice β] {f : αβ} (hf : MonotoneOn f s) (hs : Set.Nonempty s) :
                  f (sInf s) = sInf (f '' s)
                  theorem Monotone.map_csInf {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} [IsWellOrder α fun x x_1 => x < x_1] {β : Type u_5} [ConditionallyCompleteLattice β] {f : αβ} (hf : Monotone f) (hs : Set.Nonempty s) :
                  f (sInf s) = sInf (f '' s)

                  Lemmas about a conditionally complete linear order with bottom element #

                  In this case we have Sup ∅ = ⊥, so we can drop some Nonempty/Set.Nonempty assumptions.

                  @[simp]
                  theorem ciSup_of_empty {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrderBot α] [IsEmpty ι] (f : ια) :
                  ⨆ (i : ι), f i =
                  theorem ciSup_false {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] (f : Falseα) :
                  ⨆ (i : False), f i =
                  @[simp]
                  theorem csInf_univ {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] :
                  sInf Set.univ =
                  theorem isLUB_csSup' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} (hs : BddAbove s) :
                  IsLUB s (sSup s)
                  theorem csSup_le_iff' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} (hs : BddAbove s) {a : α} :
                  sSup s a ∀ (x : α), x sx a
                  theorem csSup_le' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (h : a upperBounds s) :
                  sSup s a
                  theorem le_csSup_iff' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (h : BddAbove s) :
                  a sSup s ∀ (b : α), b upperBounds sa b
                  theorem le_ciSup_iff' {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrderBot α] {s : ια} {a : α} (h : BddAbove (Set.range s)) :
                  a iSup s ∀ (b : α), (∀ (i : ι), s i b) → a b
                  theorem le_csInf_iff'' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (ne : Set.Nonempty s) :
                  a sInf s ∀ (b : α), b sa b
                  theorem le_ciInf_iff' {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrderBot α] [Nonempty ι] {f : ια} {a : α} :
                  a iInf f ∀ (i : ι), a f i
                  theorem csInf_le' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (h : a s) :
                  sInf s a
                  theorem ciInf_le' {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrderBot α] (f : ια) (i : ι) :
                  iInf f f i
                  theorem exists_lt_of_lt_csSup' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (h : a < sSup s) :
                  b, b s a < b
                  theorem ciSup_le_iff' {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrderBot α] {f : ια} (h : BddAbove (Set.range f)) {a : α} :
                  ⨆ (i : ι), f i a ∀ (i : ι), f i a
                  theorem ciSup_le' {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrderBot α] {f : ια} {a : α} (h : ∀ (i : ι), f i a) :
                  ⨆ (i : ι), f i a
                  theorem exists_lt_of_lt_ciSup' {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrderBot α] {f : ια} {a : α} (h : a < ⨆ (i : ι), f i) :
                  i, a < f i
                  theorem ciSup_mono' {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrderBot α] {ι' : Sort u_5} {f : ια} {g : ι'α} (hg : BddAbove (Set.range g)) (h : ∀ (i : ι), i', f i g i') :
                  theorem csInf_le_csInf' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {t : Set α} (h₁ : Set.Nonempty t) (h₂ : t s) :
                  theorem WithTop.isLUB_sSup' {β : Type u_5} [ConditionallyCompleteLattice β] {s : Set (WithTop β)} (hs : Set.Nonempty s) :
                  IsLUB s (sSup s)

                  The sSup of a non-empty set is its least upper bound for a conditionally complete lattice with a top.

                  theorem WithTop.isGLB_sInf' {β : Type u_5} [ConditionallyCompleteLattice β] {s : Set (WithTop β)} (hs : BddBelow s) :
                  IsGLB s (sInf s)

                  The sInf of a bounded-below set is its greatest lower bound for a conditionally complete lattice with a top.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  theorem WithTop.coe_sSup {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} (hb : BddAbove s) :
                  ↑(sSup s) = ⨆ (a : α) (_ : a s), a

                  A version of WithTop.coe_sSup' with a more convenient but less general statement.

                  theorem WithTop.coe_sInf {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} (hs : Set.Nonempty s) :
                  ↑(sInf s) = ⨅ (a : α) (_ : a s), a

                  A version of WithTop.coe_sInf' with a more convenient but less general statement.

                  A monotone function into a conditionally complete lattice preserves the ordering properties of sSup and sInf.

                  theorem Monotone.le_csSup_image {α : Type u_1} {β : Type u_2} [Preorder α] [ConditionallyCompleteLattice β] {f : αβ} (h_mono : Monotone f) {s : Set α} {c : α} (hcs : c s) (h_bdd : BddAbove s) :
                  f c sSup (f '' s)
                  theorem Monotone.csSup_image_le {α : Type u_1} {β : Type u_2} [Preorder α] [ConditionallyCompleteLattice β] {f : αβ} (h_mono : Monotone f) {s : Set α} (hs : Set.Nonempty s) {B : α} (hB : B upperBounds s) :
                  sSup (f '' s) f B
                  theorem Monotone.csInf_image_le {α : Type u_1} {β : Type u_2} [Preorder α] [ConditionallyCompleteLattice β] {f : αβ} (h_mono : Monotone f) {s : Set α} {c : α} (hcs : c s) (h_bdd : BddBelow s) :
                  sInf (f '' s) f c
                  theorem Monotone.le_csInf_image {α : Type u_1} {β : Type u_2} [Preorder α] [ConditionallyCompleteLattice β] {f : αβ} (h_mono : Monotone f) {s : Set α} (hs : Set.Nonempty s) {B : α} (hB : B lowerBounds s) :
                  f B sInf (f '' s)
                  theorem GaloisConnection.l_csSup {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] {l : αβ} {u : βα} (gc : GaloisConnection l u) {s : Set α} (hne : Set.Nonempty s) (hbdd : BddAbove s) :
                  l (sSup s) = ⨆ (x : s), l x
                  theorem GaloisConnection.l_csSup' {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] {l : αβ} {u : βα} (gc : GaloisConnection l u) {s : Set α} (hne : Set.Nonempty s) (hbdd : BddAbove s) :
                  l (sSup s) = sSup (l '' s)
                  theorem GaloisConnection.l_ciSup {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [Nonempty ι] {l : αβ} {u : βα} (gc : GaloisConnection l u) {f : ια} (hf : BddAbove (Set.range f)) :
                  l (⨆ (i : ι), f i) = ⨆ (i : ι), l (f i)
                  theorem GaloisConnection.l_ciSup_set {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] {l : αβ} {u : βα} (gc : GaloisConnection l u) {s : Set γ} {f : γα} (hf : BddAbove (f '' s)) (hne : Set.Nonempty s) :
                  l (⨆ (i : s), f i) = ⨆ (i : s), l (f i)
                  theorem GaloisConnection.u_csInf {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] {l : αβ} {u : βα} (gc : GaloisConnection l u) {s : Set β} (hne : Set.Nonempty s) (hbdd : BddBelow s) :
                  u (sInf s) = ⨅ (x : s), u x
                  theorem GaloisConnection.u_csInf' {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] {l : αβ} {u : βα} (gc : GaloisConnection l u) {s : Set β} (hne : Set.Nonempty s) (hbdd : BddBelow s) :
                  u (sInf s) = sInf (u '' s)
                  theorem GaloisConnection.u_ciInf {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [Nonempty ι] {l : αβ} {u : βα} (gc : GaloisConnection l u) {f : ιβ} (hf : BddBelow (Set.range f)) :
                  u (⨅ (i : ι), f i) = ⨅ (i : ι), u (f i)
                  theorem GaloisConnection.u_ciInf_set {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] {l : αβ} {u : βα} (gc : GaloisConnection l u) {s : Set γ} {f : γβ} (hf : BddBelow (f '' s)) (hne : Set.Nonempty s) :
                  u (⨅ (i : s), f i) = ⨅ (i : s), u (f i)
                  theorem OrderIso.map_csSup {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] (e : α ≃o β) {s : Set α} (hne : Set.Nonempty s) (hbdd : BddAbove s) :
                  e (sSup s) = ⨆ (x : s), e x
                  theorem OrderIso.map_csSup' {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] (e : α ≃o β) {s : Set α} (hne : Set.Nonempty s) (hbdd : BddAbove s) :
                  e (sSup s) = sSup (e '' s)
                  theorem OrderIso.map_ciSup {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [Nonempty ι] (e : α ≃o β) {f : ια} (hf : BddAbove (Set.range f)) :
                  e (⨆ (i : ι), f i) = ⨆ (i : ι), e (f i)
                  theorem OrderIso.map_ciSup_set {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] (e : α ≃o β) {s : Set γ} {f : γα} (hf : BddAbove (f '' s)) (hne : Set.Nonempty s) :
                  e (⨆ (i : s), f i) = ⨆ (i : s), e (f i)
                  theorem OrderIso.map_csInf {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] (e : α ≃o β) {s : Set α} (hne : Set.Nonempty s) (hbdd : BddBelow s) :
                  e (sInf s) = ⨅ (x : s), e x
                  theorem OrderIso.map_csInf' {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] (e : α ≃o β) {s : Set α} (hne : Set.Nonempty s) (hbdd : BddBelow s) :
                  e (sInf s) = sInf (e '' s)
                  theorem OrderIso.map_ciInf {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [Nonempty ι] (e : α ≃o β) {f : ια} (hf : BddBelow (Set.range f)) :
                  e (⨅ (i : ι), f i) = ⨅ (i : ι), e (f i)
                  theorem OrderIso.map_ciInf_set {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] (e : α ≃o β) {s : Set γ} {f : γα} (hf : BddBelow (f '' s)) (hne : Set.Nonempty s) :
                  e (⨅ (i : s), f i) = ⨅ (i : s), e (f i)

                  Supremum/infimum of Set.image2 #

                  A collection of lemmas showing what happens to the suprema/infima of s and t when mapped under a binary function whose partial evaluations are lower/upper adjoints of Galois connections.

                  theorem csSup_image2_eq_csSup_csSup {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {l : αβγ} {u₁ : βγα} {u₂ : αγβ} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)) (hs₀ : Set.Nonempty s) (hs₁ : BddAbove s) (ht₀ : Set.Nonempty t) (ht₁ : BddAbove t) :
                  sSup (Set.image2 l s t) = l (sSup s) (sSup t)
                  theorem csSup_image2_eq_csSup_csInf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {l : αβγ} {u₁ : βγα} {u₂ : αγβ} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a OrderDual.ofDual) (OrderDual.toDual u₂ a)) :
                  Set.Nonempty sBddAbove sSet.Nonempty tBddBelow tsSup (Set.image2 l s t) = l (sSup s) (sInf t)
                  theorem csSup_image2_eq_csInf_csSup {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {l : αβγ} {u₁ : βγα} {u₂ : αγβ} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b OrderDual.ofDual) (OrderDual.toDual u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)) :
                  Set.Nonempty sBddBelow sSet.Nonempty tBddAbove tsSup (Set.image2 l s t) = l (sInf s) (sSup t)
                  theorem csSup_image2_eq_csInf_csInf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {l : αβγ} {u₁ : βγα} {u₂ : αγβ} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b OrderDual.ofDual) (OrderDual.toDual u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a OrderDual.ofDual) (OrderDual.toDual u₂ a)) :
                  Set.Nonempty sBddBelow sSet.Nonempty tBddBelow tsSup (Set.image2 l s t) = l (sInf s) (sInf t)
                  theorem csInf_image2_eq_csInf_csInf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {u : αβγ} {l₁ : βγα} {l₂ : αγβ} (h₁ : ∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a)) :
                  Set.Nonempty sBddBelow sSet.Nonempty tBddBelow tsInf (Set.image2 u s t) = u (sInf s) (sInf t)
                  theorem csInf_image2_eq_csInf_csSup {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {u : αβγ} {l₁ : βγα} {l₂ : αγβ} (h₁ : ∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (OrderDual.toDual l₂ a) (u a OrderDual.ofDual)) :
                  Set.Nonempty sBddBelow sSet.Nonempty tBddAbove tsInf (Set.image2 u s t) = u (sInf s) (sSup t)
                  theorem csInf_image2_eq_csSup_csInf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {u : αβγ} {l₁ : βγα} {l₂ : αγβ} (h₁ : ∀ (b : β), GaloisConnection (OrderDual.toDual l₁ b) (Function.swap u b OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a)) :
                  Set.Nonempty sBddAbove sSet.Nonempty tBddBelow tsInf (Set.image2 u s t) = u (sSup s) (sInf t)
                  theorem csInf_image2_eq_csSup_csSup {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {u : αβγ} {l₁ : βγα} {l₂ : αγβ} (h₁ : ∀ (b : β), GaloisConnection (OrderDual.toDual l₁ b) (Function.swap u b OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (OrderDual.toDual l₂ a) (u a OrderDual.ofDual)) :
                  Set.Nonempty sBddAbove sSet.Nonempty tBddAbove tsInf (Set.image2 u s t) = u (sSup s) (sSup t)

                  Complete lattice structure on WithTop (WithBot α) #

                  If α is a ConditionallyCompleteLattice, then we show that WithTop α and WithBot α also inherit the structure of conditionally complete lattices. Furthermore, we show that WithTop (WithBot α) and WithBot (WithTop α) naturally inherit the structure of a complete lattice. Note that for α a conditionally complete lattice, sSup and sInf both return junk values for sets which are empty or unbounded. The extension of sSup to WithTop α fixes the unboundedness problem and the extension to WithBot α fixes the problem with the empty set.

                  This result can be used to show that the extended reals [-∞, ∞] are a complete linear order.

                  Adding a top element to a conditionally complete lattice gives a conditionally complete lattice

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

                  Adding a bottom element to a conditionally complete lattice gives a conditionally complete lattice

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Equations
                  • One or more equations did not get rendered due to their size.
                  theorem WithTop.iSup_coe_eq_top {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrderBot α] {f : ια} :
                  ⨆ (x : ι), ↑(f x) = ¬BddAbove (Set.range f)
                  theorem WithTop.iSup_coe_lt_top {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrderBot α] {f : ια} :
                  ⨆ (x : ι), ↑(f x) < BddAbove (Set.range f)
                  theorem WithTop.iInf_coe_eq_top {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrderBot α] {f : ια} :
                  ⨅ (x : ι), ↑(f x) = IsEmpty ι
                  theorem WithTop.iInf_coe_lt_top {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrderBot α] {f : ια} :
                  ⨅ (i : ι), ↑(f i) < Nonempty ι