Documentation

Mathlib.Order.CompleteLatticeIntervals

Subtypes of conditionally complete linear orders #

In this file we give conditions on a subset of a conditionally complete linear order, to ensure that the subtype is itself conditionally complete.

We check that an OrdConnected set satisfies these conditions.

TODO #

Add appropriate instances for all Set.Ixx. This requires a refactor that will allow different default values for sSup and sInf.

noncomputable def subsetSupSet {α : Type u_2} (s : Set α) [Preorder α] [SupSet α] [Inhabited s] :
SupSet s

SupSet structure on a nonempty subset s of a preorder with SupSet. This definition is non-canonical (it uses default s); it should be used only as here, as an auxiliary instance in the construction of the ConditionallyCompleteLinearOrder structure.

Equations
Instances For
    @[simp]
    theorem subset_sSup_def {α : Type u_2} (s : Set α) [Preorder α] [SupSet α] [Inhabited s] :
    sSup = fun (t : Set s) => if ht : t.Nonempty BddAbove t sSup (Subtype.val '' t) s then sSup (Subtype.val '' t), else default
    theorem subset_sSup_of_within {α : Type u_2} (s : Set α) [Preorder α] [SupSet α] [Inhabited s] {t : Set s} (h' : t.Nonempty) (h'' : BddAbove t) (h : sSup (Subtype.val '' t) s) :
    sSup (Subtype.val '' t) = (sSup t)
    theorem subset_sSup_emptyset {α : Type u_2} (s : Set α) [Preorder α] [SupSet α] [Inhabited s] :
    sSup = default
    theorem subset_sSup_of_not_bddAbove {α : Type u_2} (s : Set α) [Preorder α] [SupSet α] [Inhabited s] {t : Set s} (ht : ¬BddAbove t) :
    sSup t = default
    noncomputable def subsetInfSet {α : Type u_2} (s : Set α) [Preorder α] [InfSet α] [Inhabited s] :
    InfSet s

    InfSet structure on a nonempty subset s of a preorder with InfSet. This definition is non-canonical (it uses default s); it should be used only as here, as an auxiliary instance in the construction of the ConditionallyCompleteLinearOrder structure.

    Equations
    Instances For
      @[simp]
      theorem subset_sInf_def {α : Type u_2} (s : Set α) [Preorder α] [InfSet α] [Inhabited s] :
      sInf = fun (t : Set s) => if ht : t.Nonempty BddBelow t sInf (Subtype.val '' t) s then sInf (Subtype.val '' t), else default
      theorem subset_sInf_of_within {α : Type u_2} (s : Set α) [Preorder α] [InfSet α] [Inhabited s] {t : Set s} (h' : t.Nonempty) (h'' : BddBelow t) (h : sInf (Subtype.val '' t) s) :
      sInf (Subtype.val '' t) = (sInf t)
      theorem subset_sInf_emptyset {α : Type u_2} (s : Set α) [Preorder α] [InfSet α] [Inhabited s] :
      sInf = default
      theorem subset_sInf_of_not_bddBelow {α : Type u_2} (s : Set α) [Preorder α] [InfSet α] [Inhabited s] {t : Set s} (ht : ¬BddBelow t) :
      sInf t = default
      @[reducible, inline]
      noncomputable abbrev subsetConditionallyCompleteLinearOrder {α : Type u_2} (s : Set α) [ConditionallyCompleteLinearOrder α] [Inhabited s] (h_Sup : ∀ {t : Set s}, t.NonemptyBddAbove tsSup (Subtype.val '' t) s) (h_Inf : ∀ {t : Set s}, t.NonemptyBddBelow tsInf (Subtype.val '' t) s) :

      For a nonempty subset of a conditionally complete linear order to be a conditionally complete linear order, it suffices that it contain the sSup of all its nonempty bounded-above subsets, and the sInf of all its nonempty bounded-below subsets. See note [reducible non-instances].

      Equations
      Instances For
        theorem sSup_within_of_ordConnected {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Set α} [hs : s.OrdConnected] ⦃t : Set s (ht : t.Nonempty) (h_bdd : BddAbove t) :
        sSup (Subtype.val '' t) s

        The sSup function on a nonempty OrdConnected set s in a conditionally complete linear order takes values within s, for all nonempty bounded-above subsets of s.

        theorem sInf_within_of_ordConnected {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Set α} [hs : s.OrdConnected] ⦃t : Set s (ht : t.Nonempty) (h_bdd : BddBelow t) :
        sInf (Subtype.val '' t) s

        The sInf function on a nonempty OrdConnected set s in a conditionally complete linear order takes values within s, for all nonempty bounded-below subsets of s.

        A nonempty OrdConnected set in a conditionally complete linear order is naturally a conditionally complete linear order.

        Equations
        noncomputable def Set.Icc.completeLattice {α : Type u_2} [ConditionallyCompleteLattice α] {a : α} {b : α} (h : a b) :

        Complete lattice structure on Set.Icc

        Equations
        Instances For
          noncomputable def Set.Icc.completeLinearOrder {α : Type u_2} [ConditionallyCompleteLinearOrder α] {a : α} {b : α} (h : a b) :

          Complete linear order structure on Set.Icc

          Equations
          Instances For
            theorem Set.Icc.coe_sSup {α : Type u_2} [ConditionallyCompleteLattice α] {a : α} {b : α} (h : a b) {S : Set (Set.Icc a b)} (hS : S.Nonempty) :
            (sSup S) = sSup (Subtype.val '' S)
            theorem Set.Icc.coe_sInf {α : Type u_2} [ConditionallyCompleteLattice α] {a : α} {b : α} (h : a b) {S : Set (Set.Icc a b)} (hS : S.Nonempty) :
            (sInf S) = sInf (Subtype.val '' S)
            theorem Set.Icc.coe_iSup {ι : Sort u_1} {α : Type u_2} [ConditionallyCompleteLattice α] {a : α} {b : α} (h : a b) [Nonempty ι] {S : ι(Set.Icc a b)} :
            (iSup S) = ⨆ (i : ι), (S i)
            theorem Set.Icc.coe_iInf {ι : Sort u_1} {α : Type u_2} [ConditionallyCompleteLattice α] {a : α} {b : α} (h : a b) [Nonempty ι] {S : ι(Set.Icc a b)} :
            (iInf S) = ⨅ (i : ι), (S i)
            instance Set.Iic.instCompleteLattice {α : Type u_2} [CompleteLattice α] {a : α} :
            Equations
            @[simp]
            theorem Set.Iic.coe_sSup {α : Type u_2} [CompleteLattice α] {a : α} (S : Set (Set.Iic a)) :
            (sSup S) = sSup (Subtype.val '' S)
            @[simp]
            theorem Set.Iic.coe_iSup {ι : Sort u_1} {α : Type u_2} [CompleteLattice α] {a : α} (f : ι(Set.Iic a)) :
            (⨆ (i : ι), f i) = ⨆ (i : ι), (f i)
            theorem Set.Iic.coe_biSup {ι : Sort u_1} {α : Type u_2} [CompleteLattice α] {a : α} (f : ι(Set.Iic a)) (p : ιProp) :
            (⨆ (i : ι), ⨆ (_ : p i), f i) = ⨆ (i : ι), ⨆ (_ : p i), (f i)
            @[simp]
            theorem Set.Iic.coe_sInf {α : Type u_2} [CompleteLattice α] {a : α} (S : Set (Set.Iic a)) :
            (sInf S) = a sInf (Subtype.val '' S)
            @[simp]
            theorem Set.Iic.coe_iInf {ι : Sort u_1} {α : Type u_2} [CompleteLattice α] {a : α} (f : ι(Set.Iic a)) :
            (⨅ (i : ι), f i) = a ⨅ (i : ι), (f i)
            theorem Set.Iic.coe_biInf {ι : Sort u_1} {α : Type u_2} [CompleteLattice α] {a : α} (f : ι(Set.Iic a)) (p : ιProp) :
            (⨅ (i : ι), ⨅ (_ : p i), f i) = a ⨅ (i : ι), ⨅ (_ : p i), (f i)