# 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_1} (s : Set α) [] [] [] :
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.

Instances For
@[simp]
theorem subset_sSup_def {α : Type u_1} (s : Set α) [] [] [] :
sSup = fun t => if ht : sSup (Subtype.val '' t) s then { val := sSup (Subtype.val '' t), property := (_ : sSup (Subtype.val '' t) s) } else default
theorem subset_sSup_of_within {α : Type u_1} (s : Set α) [] [] [] {t : Set s} (h' : ) (h'' : ) (h : sSup (Subtype.val '' t) s) :
sSup (Subtype.val '' t) = ↑(sSup t)
theorem subset_sSup_emptyset {α : Type u_1} (s : Set α) [] [] [] :
= default
theorem subset_sSup_of_not_bddAbove {α : Type u_1} (s : Set α) [] [] [] {t : Set s} (ht : ) :
sSup t = default
noncomputable def subsetInfSet {α : Type u_1} (s : Set α) [] [] [] :
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.

Instances For
@[simp]
theorem subset_sInf_def {α : Type u_1} (s : Set α) [] [] [] :
sInf = fun t => if ht : sInf (Subtype.val '' t) s then { val := sInf (Subtype.val '' t), property := (_ : sInf (Subtype.val '' t) s) } else default
theorem subset_sInf_of_within {α : Type u_1} (s : Set α) [] [] [] {t : Set s} (h' : ) (h'' : ) (h : sInf (Subtype.val '' t) s) :
sInf (Subtype.val '' t) = ↑(sInf t)
theorem subset_sInf_emptyset {α : Type u_1} (s : Set α) [] [] [] :
= default
theorem subset_sInf_of_not_bddBelow {α : Type u_1} (s : Set α) [] [] [] {t : Set s} (ht : ) :
sInf t = default
@[reducible]
noncomputable def subsetConditionallyCompleteLinearOrder {α : Type u_1} (s : Set α) [] (h_Sup : ∀ {t : Set s}, sSup (Subtype.val '' t) s) (h_Inf : ∀ {t : Set s}, sInf (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].

Instances For
theorem sSup_within_of_ordConnected {α : Type u_1} {s : Set α} [hs : ] ⦃t : Set s (ht : ) (h_bdd : ) :
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_1} {s : Set α} [hs : ] ⦃t : Set s (ht : ) (h_bdd : ) :
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.

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

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