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_2} (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.

Equations

• subsetSupSet s = { sSup := fun (t : Set ↑s) => if ht : t.Nonempty ∧ BddAbove t ∧ sSup (Subtype.val '' t) ∈ s then ⟨sSup (Subtype.val '' t), ⋯⟩ else default }

@[simp]

theorem subset_sSup_def {α : Type u_2} (s : Set α) [Preorder α] [SupSet α] [Inhabited ↑s] : sSup = fun (t : Set ↑s) => if ht : t.Nonempty ∧ BddAbove t ∧ sSup (Subtype.val '' t) ∈ s then ⟨sSup (Subtype.val '' t), ⋯⟩ else default

theorem subset_sSup_of_within {α : Type u_2} (s : Set α) [Preorder α] [SupSet α] [Inhabited ↑s] {t : Set ↑s} (h' : t.Nonempty) (h'' : BddAbove t) (h : sSup (Subtype.val '' t) ∈ s) : sSup (Subtype.val '' t) = ↑(sSup t)

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

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

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

Equations

• subsetInfSet s = { sInf := fun (t : Set ↑s) => if ht : t.Nonempty ∧ BddBelow t ∧ sInf (Subtype.val '' t) ∈ s then ⟨sInf (Subtype.val '' t), ⋯⟩ else default }

@[simp]

theorem subset_sInf_def {α : Type u_2} (s : Set α) [Preorder α] [InfSet α] [Inhabited ↑s] : sInf = fun (t : Set ↑s) => if ht : t.Nonempty ∧ BddBelow t ∧ sInf (Subtype.val '' t) ∈ s then ⟨sInf (Subtype.val '' t), ⋯⟩ else default

theorem subset_sInf_of_within {α : Type u_2} (s : Set α) [Preorder α] [InfSet α] [Inhabited ↑s] {t : Set ↑s} (h' : t.Nonempty) (h'' : BddBelow t) (h : sInf (Subtype.val '' t) ∈ s) : sInf (Subtype.val '' t) = ↑(sInf t)

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

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

@[reducible, inline]

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

Equations

• subsetConditionallyCompleteLinearOrder s h_Sup h_Inf = ConditionallyCompleteLinearOrder.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯

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

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

Equations

• ordConnectedSubsetConditionallyCompleteLinearOrder s = subsetConditionallyCompleteLinearOrder s ⋯ ⋯

noncomputable instance Set.Icc.completeLattice {α : Type u_2} [ConditionallyCompleteLattice α] {a b : α} [Fact (a ≤ b)] : CompleteLattice ↑(Set.Icc a b)

Complete lattice structure on Set.Icc

Equations

• Set.Icc.completeLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable instance instCompleteLinearOrderElemIccOfFactLe {α : Type u_2} [ConditionallyCompleteLinearOrder α] {a b : α} [Fact (a ≤ b)] : CompleteLinearOrder ↑(Set.Icc a b)

Complete linear order structure on Set.Icc

Equations

• instCompleteLinearOrderElemIccOfFactLe = CompleteLinearOrder.mk ⋯ ⋯ ⋯ ⋯ ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT

theorem Set.Icc.coe_sSup {α : Type u_2} [ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b) {S : Set ↑(Set.Icc a b)} (hS : S.Nonempty) : let_fun this := ⋯; ↑(sSup S) = sSup (Subtype.val '' S)

theorem Set.Icc.coe_sInf {α : Type u_2} [ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b) {S : Set ↑(Set.Icc a b)} (hS : S.Nonempty) : let_fun this := ⋯; ↑(sInf S) = sInf (Subtype.val '' S)

theorem Set.Icc.coe_iSup {ι : Sort u_1} {α : Type u_2} [ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b) [Nonempty ι] {S : ι → ↑(Set.Icc a b)} : let_fun this := ⋯; ↑(iSup S) = ⨆ (i : ι), ↑(S i)

theorem Set.Icc.coe_iInf {ι : Sort u_1} {α : Type u_2} [ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b) [Nonempty ι] {S : ι → ↑(Set.Icc a b)} : let_fun this := ⋯; ↑(iInf S) = ⨅ (i : ι), ↑(S i)

instance Set.Iic.instCompleteLattice {α : Type u_2} [CompleteLattice α] {a : α} : CompleteLattice ↑(Set.Iic a)

Equations

• Set.Iic.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem Set.Iic.coe_sSup {α : Type u_2} [CompleteLattice α] {a : α} (S : Set ↑(Set.Iic a)) : ↑(sSup S) = sSup (Subtype.val '' S)

@[simp]

theorem Set.Iic.coe_iSup {ι : Sort u_1} {α : Type u_2} [CompleteLattice α] {a : α} (f : ι → ↑(Set.Iic a)) : ↑(⨆ (i : ι), f i) = ⨆ (i : ι), ↑(f i)

theorem Set.Iic.coe_biSup {ι : Sort u_1} {α : Type u_2} [CompleteLattice α] {a : α} (f : ι → ↑(Set.Iic a)) (p : ι → Prop) : ↑(⨆ (i : ι), ⨆ (_ : p i), f i) = ⨆ (i : ι), ⨆ (_ : p i), ↑(f i)

@[simp]

theorem Set.Iic.coe_sInf {α : Type u_2} [CompleteLattice α] {a : α} (S : Set ↑(Set.Iic a)) : ↑(sInf S) = a ⊓ sInf (Subtype.val '' S)

@[simp]

theorem Set.Iic.coe_iInf {ι : Sort u_1} {α : Type u_2} [CompleteLattice α] {a : α} (f : ι → ↑(Set.Iic a)) : ↑(⨅ (i : ι), f i) = a ⊓ ⨅ (i : ι), ↑(f i)

theorem Set.Iic.coe_biInf {ι : Sort u_1} {α : Type u_2} [CompleteLattice α] {a : α} (f : ι → ↑(Set.Iic a)) (p : ι → Prop) : ↑(⨅ (i : ι), ⨅ (_ : p i), f i) = a ⊓ ⨅ (i : ι), ⨅ (_ : p i), ↑(f i)