# 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 : ] [inst : ] :
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
• = { supₛ := fun t => if ht : supₛ (Subtype.val '' t) s then { val := supₛ (Subtype.val '' t), property := ht } else default }
@[simp]
theorem subset_supₛ_def {α : Type u_1} (s : Set α) [inst : ] [inst : ] :
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 : ] [inst : ] {t : Set s} (h : supₛ (Subtype.val '' t) s) :
supₛ (Subtype.val '' t) = ↑(supₛ t)
noncomputable def subsetInfSet {α : Type u_1} (s : Set α) [inst : ] [inst : ] :
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
• = { infₛ := fun t => if ht : infₛ (Subtype.val '' t) s then { val := infₛ (Subtype.val '' t), property := ht } else default }
@[simp]
theorem subset_infₛ_def {α : Type u_1} (s : Set α) [inst : ] [inst : ] :
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 : ] [inst : ] {t : Set s} (h : infₛ (Subtype.val '' t) s) :
infₛ (Subtype.val '' t) = ↑(infₛ t)
noncomputable def subsetConditionallyCompleteLinearOrder {α : Type u_1} (s : Set α) [inst : ] [inst : ] (h_Sup : ∀ {t : Set s}, supₛ (Subtype.val '' t) s) (h_Inf : ∀ {t : Set s}, infₛ (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 : ] {s : Set α} [hs : ] ⦃t : Set s (ht : ) (h_bdd : ) :
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 : ] {s : Set α} [hs : ] ⦃t : Set s (ht : ) (h_bdd : ) :
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.

noncomputable instance ordConnectedSubsetConditionallyCompleteLinearOrder {α : Type u_1} (s : Set α) [inst : ] [inst : ] [inst : ] :

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.