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 supₛ and infₛ.

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

SupSet structure on a nonempty subset s of an object 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
@[simp]
theorem subset_supₛ_def {α : Type u_1} (s : Set α) [inst : SupSet α] [inst : Inhabited s] :
supₛ = fun t => if ht : supₛ (Subtype.val '' t) s then { val := supₛ (Subtype.val '' t), property := ht } else default
theorem subset_supₛ_of_within {α : Type u_1} (s : Set α) [inst : SupSet α] [inst : Inhabited s] {t : Set s} (h : supₛ (Subtype.val '' t) s) :
supₛ (Subtype.val '' t) = ↑(supₛ t)
noncomputable def subsetInfSet {α : Type u_1} (s : Set α) [inst : InfSet α] [inst : Inhabited s] :
InfSet s

InfSet structure on a nonempty subset s of an object 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
@[simp]
theorem subset_infₛ_def {α : Type u_1} (s : Set α) [inst : InfSet α] [inst : Inhabited s] :
infₛ = fun t => if ht : infₛ (Subtype.val '' t) s then { val := infₛ (Subtype.val '' t), property := ht } else default
theorem subset_infₛ_of_within {α : Type u_1} (s : Set α) [inst : InfSet α] [inst : Inhabited s] {t : Set s} (h : infₛ (Subtype.val '' t) s) :
infₛ (Subtype.val '' t) = ↑(infₛ t)
noncomputable def subsetConditionallyCompleteLinearOrder {α : Type u_1} (s : Set α) [inst : ConditionallyCompleteLinearOrder α] [inst : Inhabited s] (h_Sup : ∀ {t : Set s}, Set.Nonempty tBddAbove tsupₛ (Subtype.val '' t) s) (h_Inf : ∀ {t : Set s}, Set.Nonempty tBddBelow tinfₛ (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 supₛ of all its nonempty bounded-above subsets, and the infₛ of all its nonempty bounded-below subsets. See note [reducible non-instances].

Equations
  • One or more equations did not get rendered due to their size.
theorem supₛ_within_of_ordConnected {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} [hs : Set.OrdConnected s] ⦃t : Set s (ht : Set.Nonempty t) (h_bdd : BddAbove t) :
supₛ (Subtype.val '' t) s

The supₛ 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 infₛ_within_of_ordConnected {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} [hs : Set.OrdConnected s] ⦃t : Set s (ht : Set.Nonempty t) (h_bdd : BddBelow t) :
infₛ (Subtype.val '' t) s

The infₛ 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
  • One or more equations did not get rendered due to their size.