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 supₛ s and infₛ 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 supₛ and infₛ in conditionally complete lattices.

To differentiate the statements between complete lattices and conditionally complete lattices, we prefix infₛ and supₛ in the statements by c, giving cinfₛ and csupₛ. For instance, infₛ_le is a statement in complete lattices ensuring infₛ s ≤ x≤ x, while cinfₛ_le is the same statement in conditionally complete lattices with an additional assumption that s is bounded below.

Extension of supₛ and infₛ from a preorder α to WithTop α and WithBot α

noncomputable instance instSupSetWithTop {α : Type u_1} [inst : Preorder α] [inst : SupSet α] :
Equations
noncomputable instance instInfSetWithTop {α : Type u_1} [inst : InfSet α] :
Equations
  • instInfSetWithTop = { infₛ := fun S => if S {} then else ↑(infₛ ((fun a => a) ⁻¹' S)) }
noncomputable instance instSupSetWithBot {α : Type u_1} [inst : SupSet α] :
Equations
  • instSupSetWithBot = { supₛ := infₛ }
noncomputable instance instInfSetWithBot {α : Type u_1} [inst : Preorder α] [inst : InfSet α] :
Equations
  • instInfSetWithBot = { infₛ := supₛ }
@[simp]
theorem WithTop.infₛ_empty {α : Type u_1} [inst : InfSet α] :
@[simp]
theorem WithTop.infᵢ_empty {ι : Sort u_2} {α : Type u_1} [inst : IsEmpty ι] [inst : InfSet α] (f : ιWithTop α) :
(i, f i) =
theorem WithTop.coe_infₛ' {α : Type u_1} [inst : InfSet α] {s : Set α} (hs : Set.Nonempty s) :
↑(infₛ s) = infₛ ((fun a => a) '' s)
theorem WithTop.coe_infᵢ {α : Type u_2} {ι : Sort u_1} [inst : Nonempty ι] [inst : InfSet α] (f : ια) :
↑(i, f i) = i, ↑(f i)
theorem WithTop.coe_supₛ' {α : Type u_1} [inst : Preorder α] [inst : SupSet α] {s : Set α} (hs : BddAbove s) :
↑(supₛ s) = supₛ ((fun a => a) '' s)
theorem WithTop.coe_supᵢ {α : Type u_1} {ι : Sort u_2} [inst : Preorder α] [inst : SupSet α] (f : ια) (h : BddAbove (Set.range f)) :
↑(i, f i) = i, ↑(f i)
@[simp]
theorem WithBot.supₛ_empty {α : Type u_1} [inst : SupSet α] :
@[simp]
theorem WithBot.supᵢ_empty {ι : Sort u_2} {α : Type u_1} [inst : IsEmpty ι] [inst : SupSet α] (f : ιWithBot α) :
(i, f i) =
theorem WithBot.coe_supₛ' {α : Type u_1} [inst : SupSet α] {s : Set α} (hs : Set.Nonempty s) :
↑(supₛ s) = supₛ ((fun a => a) '' s)
theorem WithBot.coe_supᵢ {α : Type u_2} {ι : Sort u_1} [inst : Nonempty ι] [inst : SupSet α] (f : ια) :
↑(i, f i) = i, ↑(f i)
theorem WithBot.coe_infₛ' {α : Type u_1} [inst : Preorder α] [inst : InfSet α] {s : Set α} (hs : BddBelow s) :
↑(infₛ s) = infₛ ((fun a => a) '' s)
theorem WithBot.coe_infᵢ {α : Type u_1} {ι : Sort u_2} [inst : Preorder α] [inst : InfSet α] (f : ια) (h : BddBelow (Set.range f)) :
↑(i, f i) = i, ↑(f i)
class ConditionallyCompleteLattice (α : Type u_1) extends Lattice , SupSet , InfSet :
Type u_1

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 infₛ 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 infₛ and supₛ 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.
      • ⊥⊥ is the least element

        bot_le : ∀ (x : α), x
      • The supremum of the empty set is ⊥⊥

        csupₛ_empty : supₛ =

      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 infₛ and supₛ 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 infₛ and supₛ 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.
        noncomputable def IsWellOrder.conditionallyCompleteLinearOrderBot (α : Type u_1) [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
        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 conditionallyCompleteLatticeOfSupₛ (α : Type u_1) [H1 : PartialOrder α] [H2 : SupSet α] (bddAbove_pair : ∀ (a b : α), BddAbove {a, b}) (bddBelow_pair : ∀ (a b : α), BddBelow {a, b}) (isLUB_supₛ : ∀ (s : Set α), BddAbove sSet.Nonempty sIsLUB s (supₛ 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, infₛ
          ..conditionallyCompleteLatticeOfSupₛ my_T _ }
        
        Equations
        • One or more equations did not get rendered due to their size.
        def conditionallyCompleteLatticeOfInfₛ (α : Type u_1) [H1 : PartialOrder α] [H2 : InfSet α] (bddAbove_pair : ∀ (a b : α), BddAbove {a, b}) (bddBelow_pair : ∀ (a b : α), BddBelow {a, b}) (isGLB_infₛ : ∀ (s : Set α), BddBelow sSet.Nonempty sIsGLB s (infₛ 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, supₛ
          ..conditionallyCompleteLatticeOfInfₛ my_T _ }
        
        Equations
        • One or more equations did not get rendered due to their size.
        def conditionallyCompleteLatticeOfLatticeOfSupₛ (α : Type u_1) [H1 : Lattice α] [inst : SupSet α] (isLUB_supₛ : ∀ (s : Set α), BddAbove sSet.Nonempty sIsLUB s (supₛ s)) :

        A version of conditionallyCompleteLatticeOfSupₛ 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.
        def conditionallyCompleteLatticeOfLatticeOfInfₛ (α : Type u_1) [H1 : Lattice α] [inst : InfSet α] (isGLB_infₛ : ∀ (s : Set α), BddBelow sSet.Nonempty sIsGLB s (infₛ s)) :

        A version of conditionallyCompleteLatticeOfInfₛ 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.
        theorem le_csupₛ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α} (h₁ : BddAbove s) (h₂ : a s) :
        theorem csupₛ_le {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α} (h₁ : Set.Nonempty s) (h₂ : ∀ (b : α), b sb a) :
        theorem cinfₛ_le {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α} (h₁ : BddBelow s) (h₂ : a s) :
        theorem le_cinfₛ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α} (h₁ : Set.Nonempty s) (h₂ : ∀ (b : α), b sa b) :
        theorem le_csupₛ_of_le {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α} {b : α} (hs : BddAbove s) (hb : b s) (h : a b) :
        theorem cinfₛ_le_of_le {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α} {b : α} (hs : BddBelow s) (hb : b s) (h : b a) :
        theorem csupₛ_le_csupₛ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {t : Set α} (ht : BddAbove t) (hs : Set.Nonempty s) (h : s t) :
        theorem cinfₛ_le_cinfₛ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {t : Set α} (ht : BddBelow t) (hs : Set.Nonempty s) (h : s t) :
        theorem le_csupₛ_iff {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α} (h : BddAbove s) (hs : Set.Nonempty s) :
        a supₛ s ∀ (b : α), b upperBounds sa b
        theorem cinfₛ_le_iff {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α} (h : BddBelow s) (hs : Set.Nonempty s) :
        infₛ s a ∀ (b : α), b lowerBounds sb a
        theorem isLUB_csupₛ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} (ne : Set.Nonempty s) (H : BddAbove s) :
        theorem isLUB_csupᵢ {α : Type u_2} {ι : Sort u_1} [inst : ConditionallyCompleteLattice α] [inst : Nonempty ι] {f : ια} (H : BddAbove (Set.range f)) :
        IsLUB (Set.range f) (i, f i)
        theorem isLUB_csupᵢ_set {α : Type u_2} {β : Type u_1} [inst : ConditionallyCompleteLattice α] {f : βα} {s : Set β} (H : BddAbove (f '' s)) (Hne : Set.Nonempty s) :
        IsLUB (f '' s) (i, f i)
        theorem isGLB_cinfₛ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} (ne : Set.Nonempty s) (H : BddBelow s) :
        theorem isGLB_cinfᵢ {α : Type u_2} {ι : Sort u_1} [inst : ConditionallyCompleteLattice α] [inst : Nonempty ι] {f : ια} (H : BddBelow (Set.range f)) :
        IsGLB (Set.range f) (i, f i)
        theorem isGLB_cinfᵢ_set {α : Type u_2} {β : Type u_1} [inst : ConditionallyCompleteLattice α] {f : βα} {s : Set β} (H : BddBelow (f '' s)) (Hne : Set.Nonempty s) :
        IsGLB (f '' s) (i, f i)
        theorem csupᵢ_le_iff {α : Type u_2} {ι : Sort u_1} [inst : ConditionallyCompleteLattice α] [inst : Nonempty ι] {f : ια} {a : α} (hf : BddAbove (Set.range f)) :
        supᵢ f a ∀ (i : ι), f i a
        theorem le_cinfᵢ_iff {α : Type u_2} {ι : Sort u_1} [inst : ConditionallyCompleteLattice α] [inst : Nonempty ι] {f : ια} {a : α} (hf : BddBelow (Set.range f)) :
        a infᵢ f ∀ (i : ι), a f i
        theorem csupᵢ_set_le_iff {α : Type u_2} [inst : ConditionallyCompleteLattice α] {ι : Type u_1} {s : Set ι} {f : ια} {a : α} (hs : Set.Nonempty s) (hf : BddAbove (f '' s)) :
        (i, f i) a ∀ (i : ι), i sf i a
        theorem le_cinfᵢ_set_iff {α : Type u_2} [inst : ConditionallyCompleteLattice α] {ι : Type u_1} {s : Set ι} {f : ια} {a : α} (hs : Set.Nonempty s) (hf : BddBelow (f '' s)) :
        (a i, f i) ∀ (i : ι), i sa f i
        theorem IsLUB.csupₛ_eq {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsLUB s a) (ne : Set.Nonempty s) :
        supₛ s = a
        theorem IsLUB.csupᵢ_eq {α : Type u_2} {ι : Sort u_1} [inst : ConditionallyCompleteLattice α] {a : α} [inst : Nonempty ι] {f : ια} (H : IsLUB (Set.range f) a) :
        (i, f i) = a
        theorem IsLUB.csupᵢ_set_eq {α : Type u_2} {β : Type u_1} [inst : ConditionallyCompleteLattice α] {a : α} {s : Set β} {f : βα} (H : IsLUB (f '' s) a) (Hne : Set.Nonempty s) :
        (i, f i) = a
        theorem IsGreatest.csupₛ_eq {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsGreatest s a) :
        supₛ s = a

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

        theorem IsGreatest.csupₛ_mem {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsGreatest s a) :
        theorem IsGLB.cinfₛ_eq {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsGLB s a) (ne : Set.Nonempty s) :
        infₛ s = a
        theorem IsGLB.cinfᵢ_eq {α : Type u_2} {ι : Sort u_1} [inst : ConditionallyCompleteLattice α] {a : α} [inst : Nonempty ι] {f : ια} (H : IsGLB (Set.range f) a) :
        (i, f i) = a
        theorem IsGLB.cinfᵢ_set_eq {α : Type u_2} {β : Type u_1} [inst : ConditionallyCompleteLattice α] {a : α} {s : Set β} {f : βα} (H : IsGLB (f '' s) a) (Hne : Set.Nonempty s) :
        (i, f i) = a
        theorem IsLeast.cinfₛ_eq {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsLeast s a) :
        infₛ s = a

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

        theorem IsLeast.cinfₛ_mem {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsLeast s a) :
        theorem subset_Icc_cinfₛ_csupₛ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} (hb : BddBelow s) (ha : BddAbove s) :
        theorem csupₛ_le_iff {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α} (hb : BddAbove s) (hs : Set.Nonempty s) :
        supₛ s a ∀ (b : α), b sb a
        theorem le_cinfₛ_iff {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α} (hb : BddBelow s) (hs : Set.Nonempty s) :
        a infₛ s ∀ (b : α), b sa b
        theorem not_mem_of_lt_cinfₛ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {x : α} {s : Set α} (h : x < infₛ s) (hs : BddBelow s) :
        ¬x s
        theorem not_mem_of_csupₛ_lt {α : Type u_1} [inst : ConditionallyCompleteLattice α] {x : α} {s : Set α} (h : supₛ s < x) (hs : BddAbove s) :
        ¬x s
        theorem csupₛ_eq_of_forall_le_of_forall_lt_exists_gt {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {b : α} (hs : Set.Nonempty s) (H : ∀ (a : α), a sa b) (H' : ∀ (w : α), w < ba, a s w < a) :
        supₛ 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 supₛ_eq_of_forall_le_of_forall_lt_exists_gt for a version in complete lattices.

        theorem cinfₛ_eq_of_forall_ge_of_forall_gt_exists_lt {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {b : α} :
        Set.Nonempty s(∀ (a : α), a sb a) → (∀ (w : α), b < wa, a s a < w) → infₛ 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 infₛ_eq_of_forall_ge_of_forall_gt_exists_lt for a version in complete lattices.

        theorem lt_csupₛ_of_lt {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α} {b : α} (hs : BddAbove s) (ha : a s) (h : b < a) :
        b < supₛ s

        b < supₛ 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 cinfₛ_lt_of_lt {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α} {b : α} :
        BddBelow sa sa < binfₛ s < b

        infₛ 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} [inst : 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 csupₛ_singleton {α : Type u_1} [inst : ConditionallyCompleteLattice α] (a : α) :
        supₛ {a} = a

        The supremum of a singleton is the element of the singleton

        @[simp]
        theorem cinfₛ_singleton {α : Type u_1} [inst : ConditionallyCompleteLattice α] (a : α) :
        infₛ {a} = a

        The infimum of a singleton is the element of the singleton

        @[simp]
        theorem csupₛ_pair {α : Type u_1} [inst : ConditionallyCompleteLattice α] (a : α) (b : α) :
        supₛ {a, b} = a b
        @[simp]
        theorem cinfₛ_pair {α : Type u_1} [inst : ConditionallyCompleteLattice α] (a : α) (b : α) :
        infₛ {a, b} = a b
        theorem cinfₛ_le_csupₛ {α : Type u_1} [inst : 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 csupₛ_union {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {t : Set α} (hs : BddAbove s) (sne : Set.Nonempty s) (ht : BddAbove t) (tne : Set.Nonempty t) :

        The supₛ 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 cinfₛ_union {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {t : Set α} (hs : BddBelow s) (sne : Set.Nonempty s) (ht : BddBelow t) (tne : Set.Nonempty t) :

        The infₛ 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 csupₛ_inter_le {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {t : Set α} (hs : BddAbove s) (ht : BddAbove t) (hst : Set.Nonempty (s 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_cinfₛ_inter {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {t : Set α} :
        BddBelow sBddBelow tSet.Nonempty (s t)infₛ s infₛ t infₛ (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 csupₛ_insert {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α} (hs : BddAbove s) (sne : Set.Nonempty 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 cinfₛ_insert {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α} (hs : BddBelow s) (sne : Set.Nonempty 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 cinfₛ_Icc {α : Type u_1} [inst : ConditionallyCompleteLattice α] {a : α} {b : α} (h : a b) :
        infₛ (Set.Icc a b) = a
        @[simp]
        theorem cinfₛ_Ici {α : Type u_1} [inst : ConditionallyCompleteLattice α] {a : α} :
        @[simp]
        theorem cinfₛ_Ico {α : Type u_1} [inst : ConditionallyCompleteLattice α] {a : α} {b : α} (h : a < b) :
        infₛ (Set.Ico a b) = a
        @[simp]
        theorem cinfₛ_Ioc {α : Type u_1} [inst : ConditionallyCompleteLattice α] {a : α} {b : α} [inst : DenselyOrdered α] (h : a < b) :
        infₛ (Set.Ioc a b) = a
        @[simp]
        theorem cinfₛ_Ioi {α : Type u_1} [inst : ConditionallyCompleteLattice α] {a : α} [inst : NoMaxOrder α] [inst : DenselyOrdered α] :
        @[simp]
        theorem cinfₛ_Ioo {α : Type u_1} [inst : ConditionallyCompleteLattice α] {a : α} {b : α} [inst : DenselyOrdered α] (h : a < b) :
        infₛ (Set.Ioo a b) = a
        @[simp]
        theorem csupₛ_Icc {α : Type u_1} [inst : ConditionallyCompleteLattice α] {a : α} {b : α} (h : a b) :
        supₛ (Set.Icc a b) = b
        @[simp]
        theorem csupₛ_Ico {α : Type u_1} [inst : ConditionallyCompleteLattice α] {a : α} {b : α} [inst : DenselyOrdered α] (h : a < b) :
        supₛ (Set.Ico a b) = b
        @[simp]
        theorem csupₛ_Iic {α : Type u_1} [inst : ConditionallyCompleteLattice α] {a : α} :
        @[simp]
        theorem csupₛ_Iio {α : Type u_1} [inst : ConditionallyCompleteLattice α] {a : α} [inst : NoMinOrder α] [inst : DenselyOrdered α] :
        @[simp]
        theorem csupₛ_Ioc {α : Type u_1} [inst : ConditionallyCompleteLattice α] {a : α} {b : α} (h : a < b) :
        supₛ (Set.Ioc a b) = b
        @[simp]
        theorem csupₛ_Ioo {α : Type u_1} [inst : ConditionallyCompleteLattice α] {a : α} {b : α} [inst : DenselyOrdered α] (h : a < b) :
        supₛ (Set.Ioo a b) = b
        theorem csupᵢ_le {α : Type u_2} {ι : Sort u_1} [inst : ConditionallyCompleteLattice α] [inst : Nonempty ι] {f : ια} {c : α} (H : ∀ (x : ι), f x c) :

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

        theorem le_csupᵢ {α : Type u_1} {ι : Sort u_2} [inst : ConditionallyCompleteLattice α] {f : ια} (H : BddAbove (Set.range f)) (c : ι) :
        f c supᵢ f

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

        theorem le_csupᵢ_of_le {α : Type u_1} {ι : Sort u_2} [inst : ConditionallyCompleteLattice α] {a : α} {f : ια} (H : BddAbove (Set.range f)) (c : ι) (h : a f c) :
        theorem csupᵢ_mono {α : Type u_1} {ι : Sort u_2} [inst : 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_csupᵢ_set {α : Type u_2} {β : Type u_1} [inst : ConditionallyCompleteLattice α] {f : βα} {s : Set β} (H : BddAbove (f '' s)) {c : β} (hc : c s) :
        f c i, f i
        theorem cinfᵢ_mono {α : Type u_1} {ι : Sort u_2} [inst : 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_cinfᵢ {α : Type u_2} {ι : Sort u_1} [inst : ConditionallyCompleteLattice α] [inst : Nonempty ι] {f : ια} {c : α} (H : ∀ (x : ι), c f x) :

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

        theorem cinfᵢ_le {α : Type u_1} {ι : Sort u_2} [inst : ConditionallyCompleteLattice α] {f : ια} (H : BddBelow (Set.range f)) (c : ι) :
        infᵢ f f c

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

        theorem cinfᵢ_le_of_le {α : Type u_1} {ι : Sort u_2} [inst : ConditionallyCompleteLattice α] {a : α} {f : ια} (H : BddBelow (Set.range f)) (c : ι) (h : f c a) :
        theorem cinfᵢ_set_le {α : Type u_2} {β : Type u_1} [inst : ConditionallyCompleteLattice α] {f : βα} {s : Set β} (H : BddBelow (f '' s)) {c : β} (hc : c s) :
        (i, f i) f c
        @[simp]
        theorem csupᵢ_const {α : Type u_2} {ι : Sort u_1} [inst : ConditionallyCompleteLattice α] [hι : Nonempty ι] {a : α} :
        (_b, a) = a
        @[simp]
        theorem cinfᵢ_const {α : Type u_2} {ι : Sort u_1} [inst : ConditionallyCompleteLattice α] [inst : Nonempty ι] {a : α} :
        (_b, a) = a
        @[simp]
        theorem csupᵢ_unique {α : Type u_2} {ι : Sort u_1} [inst : ConditionallyCompleteLattice α] [inst : Unique ι] {s : ια} :
        (i, s i) = s default
        @[simp]
        theorem cinfᵢ_unique {α : Type u_2} {ι : Sort u_1} [inst : ConditionallyCompleteLattice α] [inst : Unique ι] {s : ια} :
        (i, s i) = s default
        theorem csupᵢ_subsingleton {α : Type u_2} {ι : Sort u_1} [inst : ConditionallyCompleteLattice α] [inst : Subsingleton ι] (i : ι) (s : ια) :
        (i, s i) = s i
        theorem cinfᵢ_subsingleton {α : Type u_2} {ι : Sort u_1} [inst : ConditionallyCompleteLattice α] [inst : Subsingleton ι] (i : ι) (s : ια) :
        (i, s i) = s i
        @[simp]
        theorem csupᵢ_pos {α : Type u_1} [inst : ConditionallyCompleteLattice α] {p : Prop} {f : pα} (hp : p) :
        (h, f h) = f hp
        @[simp]
        theorem cinfᵢ_pos {α : Type u_1} [inst : ConditionallyCompleteLattice α] {p : Prop} {f : pα} (hp : p) :
        (h, f h) = f hp
        theorem csupᵢ_eq_of_forall_le_of_forall_lt_exists_gt {α : Type u_2} {ι : Sort u_1} [inst : ConditionallyCompleteLattice α] {b : α} [inst : 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 supᵢ_eq_of_forall_le_of_forall_lt_exists_gt for a version in complete lattices.

        theorem cinfᵢ_eq_of_forall_ge_of_forall_gt_exists_lt {α : Type u_2} {ι : Sort u_1} [inst : ConditionallyCompleteLattice α] {b : α} [inst : 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 infᵢ_eq_of_forall_ge_of_forall_gt_exists_lt for a version in complete lattices.

        theorem Monotone.csupᵢ_mem_Inter_Icc_of_antitone {α : Type u_2} {β : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : SemilatticeSup β] {f : βα} {g : βα} (hf : Monotone f) (hg : Antitone g) (h : f g) :
        (n, f n) Set.interᵢ fun 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≤ g n for all n, then ⨆ n, f n⨆ n, f n belongs to all the intervals [f n, g n].

        theorem csupᵢ_mem_Inter_Icc_of_antitone_Icc {α : Type u_2} {β : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : SemilatticeSup β] {f : βα} {g : βα} (h : Antitone fun n => Set.Icc (f n) (g n)) (h' : ∀ (n : β), f n g n) :
        (n, f n) Set.interᵢ fun 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⨆ n, f n belongs to all the intervals [f n, g n].

        theorem csupₛ_eq_of_is_forall_le_of_forall_le_imp_ge {α : Type u_1} [inst : 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) :
        supₛ 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'≤ b'.
        instance Pi.conditionallyCompleteLattice {ι : Type u_1} {α : ιType u_2} [inst : (i : ι) → ConditionallyCompleteLattice (α i)] :
        ConditionallyCompleteLattice ((i : ι) → α i)
        Equations
        • One or more equations did not get rendered due to their size.
        theorem exists_lt_of_lt_csupₛ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} {b : α} (hs : Set.Nonempty s) (hb : b < supₛ s) :
        a, a s b < a

        When b < supₛ 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_csupᵢ {α : Type u_2} {ι : Sort u_1} [inst : ConditionallyCompleteLinearOrder α] {b : α} [inst : Nonempty ι] {f : ια} (h : b < supᵢ f) :
        i, b < f i

        Indexed version of the above lemma exists_lt_of_lt_csupₛ. When b < supᵢ f, there is an element i such that b < f i.

        theorem exists_lt_of_cinfₛ_lt {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} {b : α} (hs : Set.Nonempty s) (hb : infₛ s < b) :
        a, a s a < b

        When infₛ 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_cinfᵢ_lt {α : Type u_2} {ι : Sort u_1} [inst : ConditionallyCompleteLinearOrder α] {a : α} [inst : Nonempty ι] {f : ια} (h : infᵢ f < a) :
        i, f i < a

        Indexed version of the above lemma exists_lt_of_cinfₛ_lt When infᵢ f < a, there is an element i such that f i < a.

        theorem infₛ_eq_argmin_on {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} [inst : IsWellOrder α fun x x_1 => x < x_1] (hs : Set.Nonempty s) :
        infₛ s = Function.argminOn id (_ : WellFounded fun x x_1 => x < x_1) s hs
        theorem isLeast_cinfₛ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} [inst : IsWellOrder α fun x x_1 => x < x_1] (hs : Set.Nonempty s) :
        theorem le_cinfₛ_iff' {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} {b : α} [inst : IsWellOrder α fun x x_1 => x < x_1] (hs : Set.Nonempty s) :
        theorem cinfₛ_mem {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} [inst : IsWellOrder α fun x x_1 => x < x_1] (hs : Set.Nonempty s) :
        theorem cinfᵢ_mem {α : Type u_2} {ι : Sort u_1} [inst : ConditionallyCompleteLinearOrder α] [inst : IsWellOrder α fun x x_1 => x < x_1] [inst : Nonempty ι] (f : ια) :
        theorem MonotoneOn.map_cinfₛ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} [inst : IsWellOrder α fun x x_1 => x < x_1] {β : Type u_1} [inst : ConditionallyCompleteLattice β] {f : αβ} (hf : MonotoneOn f s) (hs : Set.Nonempty s) :
        f (infₛ s) = infₛ (f '' s)
        theorem Monotone.map_cinfₛ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} [inst : IsWellOrder α fun x x_1 => x < x_1] {β : Type u_1} [inst : ConditionallyCompleteLattice β] {f : αβ} (hf : Monotone f) (hs : Set.Nonempty s) :
        f (infₛ s) = infₛ (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 csupᵢ_of_empty {α : Type u_2} {ι : Sort u_1} [inst : ConditionallyCompleteLinearOrderBot α] [inst : IsEmpty ι] (f : ια) :
        (i, f i) =
        theorem csupᵢ_false {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] (f : Falseα) :
        (i, f i) =
        @[simp]
        theorem cinfₛ_univ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] :
        infₛ Set.univ =
        theorem isLUB_csupₛ' {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α} (hs : BddAbove s) :
        theorem csupₛ_le_iff' {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α} (hs : BddAbove s) {a : α} :
        supₛ s a ∀ (x : α), x sx a
        theorem csupₛ_le' {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (h : a upperBounds s) :
        theorem le_csupₛ_iff' {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (h : BddAbove s) :
        a supₛ s ∀ (b : α), b upperBounds sa b
        theorem le_csupᵢ_iff' {α : Type u_1} {ι : Sort u_2} [inst : ConditionallyCompleteLinearOrderBot α] {s : ια} {a : α} (h : BddAbove (Set.range s)) :
        a supᵢ s ∀ (b : α), (∀ (i : ι), s i b) → a b
        theorem le_cinfₛ_iff'' {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (ne : Set.Nonempty s) :
        a infₛ s ∀ (b : α), b sa b
        theorem le_cinfᵢ_iff' {α : Type u_2} {ι : Sort u_1} [inst : ConditionallyCompleteLinearOrderBot α] [inst : Nonempty ι] {f : ια} {a : α} :
        a infᵢ f ∀ (i : ι), a f i
        theorem cinfₛ_le' {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (h : a s) :
        theorem cinfᵢ_le' {α : Type u_1} {ι : Sort u_2} [inst : ConditionallyCompleteLinearOrderBot α] (f : ια) (i : ι) :
        infᵢ f f i
        theorem exists_lt_of_lt_csupₛ' {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (h : a < supₛ s) :
        b, b s a < b
        theorem csupᵢ_le_iff' {α : Type u_1} {ι : Sort u_2} [inst : ConditionallyCompleteLinearOrderBot α] {f : ια} (h : BddAbove (Set.range f)) {a : α} :
        (i, f i) a ∀ (i : ι), f i a
        theorem csupᵢ_le' {α : Type u_1} {ι : Sort u_2} [inst : ConditionallyCompleteLinearOrderBot α] {f : ια} {a : α} (h : ∀ (i : ι), f i a) :
        (i, f i) a
        theorem exists_lt_of_lt_csupᵢ' {α : Type u_1} {ι : Sort u_2} [inst : ConditionallyCompleteLinearOrderBot α] {f : ια} {a : α} (h : a < i, f i) :
        i, a < f i
        theorem csupᵢ_mono' {α : Type u_2} {ι : Sort u_3} [inst : ConditionallyCompleteLinearOrderBot α] {ι' : Sort u_1} {f : ια} {g : ι'α} (hg : BddAbove (Set.range g)) (h : ∀ (i : ι), i', f i g i') :
        theorem cinfₛ_le_cinfₛ' {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α} {t : Set α} (h₁ : Set.Nonempty t) (h₂ : t s) :
        theorem WithTop.isLUB_supₛ' {β : Type u_1} [inst : ConditionallyCompleteLattice β] {s : Set (WithTop β)} (hs : Set.Nonempty s) :

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

        theorem WithTop.isGLB_infₛ' {β : Type u_1} [inst : ConditionallyCompleteLattice β] {s : Set (WithTop β)} (hs : BddBelow s) :

        The infₛ 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_supₛ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α} (hb : BddAbove s) :
        ↑(supₛ s) = a, h, a

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

        theorem WithTop.coe_infₛ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α} (hs : Set.Nonempty s) :
        ↑(infₛ s) = a, h, a

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

        A monotone function into a conditionally complete lattice preserves the ordering properties of supₛ and infₛ.

        theorem Monotone.le_csupₛ_image {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : ConditionallyCompleteLattice β] {f : αβ} (h_mono : Monotone f) {s : Set α} {c : α} (hcs : c s) (h_bdd : BddAbove s) :
        f c supₛ (f '' s)
        theorem Monotone.csupₛ_image_le {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : ConditionallyCompleteLattice β] {f : αβ} (h_mono : Monotone f) {s : Set α} (hs : Set.Nonempty s) {B : α} (hB : B upperBounds s) :
        supₛ (f '' s) f B
        theorem Monotone.cinfₛ_image_le {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : ConditionallyCompleteLattice β] {f : αβ} (h_mono : Monotone f) {s : Set α} {c : α} (hcs : c s) (h_bdd : BddBelow s) :
        infₛ (f '' s) f c
        theorem Monotone.le_cinfₛ_image {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : ConditionallyCompleteLattice β] {f : αβ} (h_mono : Monotone f) {s : Set α} (hs : Set.Nonempty s) {B : α} (hB : B lowerBounds s) :
        f B infₛ (f '' s)
        theorem GaloisConnection.l_csupₛ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] {l : αβ} {u : βα} (gc : GaloisConnection l u) {s : Set α} (hne : Set.Nonempty s) (hbdd : BddAbove s) :
        l (supₛ s) = x, l x
        theorem GaloisConnection.l_csupₛ' {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] {l : αβ} {u : βα} (gc : GaloisConnection l u) {s : Set α} (hne : Set.Nonempty s) (hbdd : BddAbove s) :
        l (supₛ s) = supₛ (l '' s)
        theorem GaloisConnection.l_csupᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] [inst : Nonempty ι] {l : αβ} {u : βα} (gc : GaloisConnection l u) {f : ια} (hf : BddAbove (Set.range f)) :
        l (i, f i) = i, l (f i)
        theorem GaloisConnection.l_csupᵢ_set {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] {l : αβ} {u : βα} (gc : GaloisConnection l u) {s : Set γ} {f : γα} (hf : BddAbove (f '' s)) (hne : Set.Nonempty s) :
        l (i, f i) = i, l (f i)
        theorem GaloisConnection.u_cinfₛ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] {l : αβ} {u : βα} (gc : GaloisConnection l u) {s : Set β} (hne : Set.Nonempty s) (hbdd : BddBelow s) :
        u (infₛ s) = x, u x
        theorem GaloisConnection.u_cinfₛ' {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] {l : αβ} {u : βα} (gc : GaloisConnection l u) {s : Set β} (hne : Set.Nonempty s) (hbdd : BddBelow s) :
        u (infₛ s) = infₛ (u '' s)
        theorem GaloisConnection.u_cinfᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] [inst : Nonempty ι] {l : αβ} {u : βα} (gc : GaloisConnection l u) {f : ιβ} (hf : BddBelow (Set.range f)) :
        u (i, f i) = i, u (f i)
        theorem GaloisConnection.u_cinfᵢ_set {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] {l : αβ} {u : βα} (gc : GaloisConnection l u) {s : Set γ} {f : γβ} (hf : BddBelow (f '' s)) (hne : Set.Nonempty s) :
        u (i, f i) = i, u (f i)
        theorem OrderIso.map_csupₛ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] (e : α ≃o β) {s : Set α} (hne : Set.Nonempty s) (hbdd : BddAbove s) :
        (RelIso.toRelEmbedding e).toEmbedding (supₛ s) = x, (RelIso.toRelEmbedding e).toEmbedding x
        theorem OrderIso.map_csupₛ' {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] (e : α ≃o β) {s : Set α} (hne : Set.Nonempty s) (hbdd : BddAbove s) :
        (RelIso.toRelEmbedding e).toEmbedding (supₛ s) = supₛ ((RelIso.toRelEmbedding e).toEmbedding '' s)
        theorem OrderIso.map_csupᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] [inst : Nonempty ι] (e : α ≃o β) {f : ια} (hf : BddAbove (Set.range f)) :
        (RelIso.toRelEmbedding e).toEmbedding (i, f i) = i, (RelIso.toRelEmbedding e).toEmbedding (f i)
        theorem OrderIso.map_csupᵢ_set {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] (e : α ≃o β) {s : Set γ} {f : γα} (hf : BddAbove (f '' s)) (hne : Set.Nonempty s) :
        (RelIso.toRelEmbedding e).toEmbedding (i, f i) = i, (RelIso.toRelEmbedding e).toEmbedding (f i)
        theorem OrderIso.map_cinfₛ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] (e : α ≃o β) {s : Set α} (hne : Set.Nonempty s) (hbdd : BddBelow s) :
        (RelIso.toRelEmbedding e).toEmbedding (infₛ s) = x, (RelIso.toRelEmbedding e).toEmbedding x
        theorem OrderIso.map_cinfₛ' {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] (e : α ≃o β) {s : Set α} (hne : Set.Nonempty s) (hbdd : BddBelow s) :
        (RelIso.toRelEmbedding e).toEmbedding (infₛ s) = infₛ ((RelIso.toRelEmbedding e).toEmbedding '' s)
        theorem OrderIso.map_cinfᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] [inst : Nonempty ι] (e : α ≃o β) {f : ια} (hf : BddBelow (Set.range f)) :
        (RelIso.toRelEmbedding e).toEmbedding (i, f i) = i, (RelIso.toRelEmbedding e).toEmbedding (f i)
        theorem OrderIso.map_cinfᵢ_set {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] (e : α ≃o β) {s : Set γ} {f : γα} (hf : BddBelow (f '' s)) (hne : Set.Nonempty s) :
        (RelIso.toRelEmbedding e).toEmbedding (i, f i) = i, (RelIso.toRelEmbedding e).toEmbedding (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 csupₛ_image2_eq_csupₛ_csupₛ {α : Type u_1} {β : Type u_3} {γ : Type u_2} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] [inst : 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) :
        supₛ (Set.image2 l s t) = l (supₛ s) (supₛ t)
        theorem csupₛ_image2_eq_csupₛ_cinfₛ {α : Type u_1} {β : Type u_3} {γ : Type u_2} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] [inst : 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 tsupₛ (Set.image2 l s t) = l (supₛ s) (infₛ t)
        theorem csupₛ_image2_eq_cinfₛ_csupₛ {α : Type u_1} {β : Type u_3} {γ : Type u_2} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] [inst : 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 tsupₛ (Set.image2 l s t) = l (infₛ s) (supₛ t)
        theorem csupₛ_image2_eq_cinfₛ_cinfₛ {α : Type u_1} {β : Type u_3} {γ : Type u_2} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] [inst : 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 tsupₛ (Set.image2 l s t) = l (infₛ s) (infₛ t)
        theorem cinfₛ_image2_eq_cinfₛ_cinfₛ {α : Type u_2} {β : Type u_3} {γ : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] [inst : 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 tinfₛ (Set.image2 u s t) = u (infₛ s) (infₛ t)
        theorem cinfₛ_image2_eq_cinfₛ_csupₛ {α : Type u_2} {β : Type u_3} {γ : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] [inst : 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 tinfₛ (Set.image2 u s t) = u (infₛ s) (supₛ t)
        theorem cinfₛ_image2_eq_csupₛ_cinfₛ {α : Type u_2} {β : Type u_3} {γ : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] [inst : 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 tinfₛ (Set.image2 u s t) = u (supₛ s) (infₛ t)
        theorem cinfₛ_image2_eq_csupₛ_csupₛ {α : Type u_2} {β : Type u_3} {γ : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] [inst : 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 tinfₛ (Set.image2 u s t) = u (supₛ s) (supₛ 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, supₛ and infₛ both return junk values for sets which are empty or unbounded. The extension of supₛ 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.supr_coe_eq_top {ι : Sort u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] (f : ια) :
        (x, ↑(f x)) = ¬BddAbove (Set.range f)
        theorem WithTop.supr_coe_lt_top {ι : Sort u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] (f : ια) :
        (x, ↑(f x)) < BddAbove (Set.range f)