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 α) [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.

@[simp]

theorem subset_sSup_def {α : Type u_1} (s : Set α) [Preorder α] [SupSet α] [Inhabited ↑s] : sSup = fun t => if ht : Set.Nonempty t ∧ BddAbove t ∧ 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 α) [Preorder α] [SupSet α] [Inhabited ↑s] {t : Set ↑s} (h' : Set.Nonempty t) (h'' : BddAbove t) (h : sSup (Subtype.val '' t) ∈ s) : sSup (Subtype.val '' t) = ↑(sSup t)

theorem subset_sSup_emptyset {α : Type u_1} (s : Set α) [Preorder α] [SupSet α] [Inhabited ↑s] : sSup ∅ = default

theorem subset_sSup_of_not_bddAbove {α : Type u_1} (s : Set α) [Preorder α] [SupSet α] [Inhabited ↑s] {t : Set ↑s} (ht : ¬BddAbove t) : sSup t = default

noncomputable def subsetInfSet {α : Type u_1} (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.

@[simp]

theorem subset_sInf_def {α : Type u_1} (s : Set α) [Preorder α] [InfSet α] [Inhabited ↑s] : sInf = fun t => if ht : Set.Nonempty t ∧ BddBelow t ∧ 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 α) [Preorder α] [InfSet α] [Inhabited ↑s] {t : Set ↑s} (h' : Set.Nonempty t) (h'' : BddBelow t) (h : sInf (Subtype.val '' t) ∈ s) : sInf (Subtype.val '' t) = ↑(sInf t)

theorem subset_sInf_emptyset {α : Type u_1} (s : Set α) [Preorder α] [InfSet α] [Inhabited ↑s] : sInf ∅ = default

theorem subset_sInf_of_not_bddBelow {α : Type u_1} (s : Set α) [Preorder α] [InfSet α] [Inhabited ↑s] {t : Set ↑s} (ht : ¬BddBelow t) : sInf t = default

@[reducible]

noncomputable def subsetConditionallyCompleteLinearOrder {α : Type u_1} (s : Set α) [ConditionallyCompleteLinearOrder α] [Inhabited ↑s] (h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s) (h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s) : ConditionallyCompleteLinearOrder ↑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].

theorem sSup_within_of_ordConnected {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} [hs : Set.OrdConnected s] ⦃t : Set ↑s⦄ (ht : Set.Nonempty t) (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_1} [ConditionallyCompleteLinearOrder α] {s : Set α} [hs : Set.OrdConnected s] ⦃t : Set ↑s⦄ (ht : Set.Nonempty t) (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.

noncomputable instance ordConnectedSubsetConditionallyCompleteLinearOrder {α : Type u_1} (s : Set α) [ConditionallyCompleteLinearOrder α] [Inhabited ↑s] [Set.OrdConnected s] : ConditionallyCompleteLinearOrder ↑s

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