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ₛ.

source

ink

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

subsetSupSet s = { supₛ := fun t => if ht : supₛ (Subtype.val '' t) ∈ s then { val := supₛ (Subtype.val '' t), property := ht } else default }

source

ink

@[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

source

ink

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)

source

ink

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

subsetInfSet s = { infₛ := fun t => if ht : infₛ (Subtype.val '' t) ∈ s then { val := infₛ (Subtype.val '' t), property := ht } else default }

source

ink

@[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

source

ink

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)

source

ink

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

source

ink

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.

source

ink

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.

source

ink

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

ConditionallyCompleteLinearOrder ↑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.