mathlib documentation

order.complete_lattice_intervals

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 ord_connected 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
noncomputable def subset_has_Sup {α : Type u_1} (s : set α) [has_Sup α] [inhabited ↥s] :
has_Sup ↥s

has_Sup structure on a nonempty subset s of an object with has_Sup. 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 conditionally_complete_linear_order structure.

Equations
source
@[simp]
theorem subset_Sup_def {α : Type u_1} (s : set α) [has_Sup α] [inhabited ↥s] :
Sup = λ (t : set ↥s), dite (Sup (coe '' t) ∈ s) (λ (ht : Sup (coe '' t) ∈ s), ⟨Sup (coe '' t), ht⟩) (λ (ht : Sup (coe '' t) ∉ s), default)
source
theorem subset_Sup_of_within {α : Type u_1} (s : set α) [has_Sup α] [inhabited ↥s] {t : set ↥s} (h : Sup (coe '' t) ∈ s) :
Sup (coe '' t) = ↑(Sup t)
source
noncomputable def subset_has_Inf {α : Type u_1} (s : set α) [has_Inf α] [inhabited ↥s] :
has_Inf ↥s

has_Inf structure on a nonempty subset s of an object with has_Inf. 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 conditionally_complete_linear_order structure.

Equations
source
@[simp]
theorem subset_Inf_def {α : Type u_1} (s : set α) [has_Inf α] [inhabited ↥s] :
Inf = λ (t : set ↥s), dite (Inf (coe '' t) ∈ s) (λ (ht : Inf (coe '' t) ∈ s), ⟨Inf (coe '' t), ht⟩) (λ (ht : Inf (coe '' t) ∉ s), default)
source
theorem subset_Inf_of_within {α : Type u_1} (s : set α) [has_Inf α] [inhabited ↥s] {t : set ↥s} (h : Inf (coe '' t) ∈ s) :
Inf (coe '' t) = ↑(Inf t)
source
noncomputable def subset_conditionally_complete_linear_order {α : Type u_1} (s : set α) [conditionally_complete_linear_order α] [inhabited ↥s] (h_Sup : ∀ {t : set ↥s}, t.nonempty → bdd_above t → Sup (coe '' t) ∈ s) (h_Inf : ∀ {t : set ↥s}, t.nonempty → bdd_below t → Inf (coe '' t) ∈ s) :
conditionally_complete_linear_order ↥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
source
theorem Sup_within_of_ord_connected {α : Type u_1} [conditionally_complete_linear_order α] {s : set α} [hs : s.ord_connected] ⦃t : set ↥s⦄ (ht : t.nonempty) (h_bdd : bdd_above t) :
Sup (coe '' t) ∈ s

The Sup function on a nonempty ord_connected set s in a conditionally complete linear order takes values within s, for all nonempty bounded-above subsets of s.

source
theorem Inf_within_of_ord_connected {α : Type u_1} [conditionally_complete_linear_order α] {s : set α} [hs : s.ord_connected] ⦃t : set ↥s⦄ (ht : t.nonempty) (h_bdd : bdd_below t) :
Inf (coe '' t) ∈ s

The Inf function on a nonempty ord_connected set s in a conditionally complete linear order takes values within s, for all nonempty bounded-below subsets of s.

source
@[protected, instance]
noncomputable def ord_connected_subset_conditionally_complete_linear_order {α : Type u_1} (s : set α) [conditionally_complete_linear_order α] [inhabited ↥s] [s.ord_connected] :
conditionally_complete_linear_order ↥s

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

Equations