# mathlibdocumentation

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.

noncomputable def subset_has_Sup {α : Type u_1} (s : set α) [has_Sup α] [inhabited 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
@[simp]
theorem subset_Sup_def {α : Type u_1} (s : set α) [has_Sup α] [inhabited s] :
has_Sup.Sup = λ (t : set s), dite (has_Sup.Sup (coe '' t) s) (λ (ht : has_Sup.Sup (coe '' t) s), has_Sup.Sup (coe '' t), ht⟩) (λ (ht : has_Sup.Sup (coe '' t) s), inhabited.default)
theorem subset_Sup_of_within {α : Type u_1} (s : set α) [has_Sup α] [inhabited s] {t : set s} (h : has_Sup.Sup (coe '' t) s) :
noncomputable def subset_has_Inf {α : Type u_1} (s : set α) [has_Inf α] [inhabited 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
@[simp]
theorem subset_Inf_def {α : Type u_1} (s : set α) [has_Inf α] [inhabited s] :
has_Inf.Inf = λ (t : set s), dite (has_Inf.Inf (coe '' t) s) (λ (ht : has_Inf.Inf (coe '' t) s), has_Inf.Inf (coe '' t), ht⟩) (λ (ht : has_Inf.Inf (coe '' t) s), inhabited.default)
theorem subset_Inf_of_within {α : Type u_1} (s : set α) [has_Inf α] [inhabited s] {t : set s} (h : has_Inf.Inf (coe '' t) s) :
@[reducible]
noncomputable def subset_conditionally_complete_linear_order {α : Type u_1} (s : set α) [inhabited s] (h_Sup : ∀ {t : set s}, t.nonemptyhas_Sup.Sup (coe '' t) s) (h_Inf : ∀ {t : set s}, t.nonemptyhas_Inf.Inf (coe '' 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 Sup of all its nonempty bounded-above subsets, and the Inf of all its nonempty bounded-below subsets. See note [reducible non-instances].

Equations
theorem Sup_within_of_ord_connected {α : Type u_1} {s : set α} [hs : s.ord_connected] ⦃t : set s⦄ (ht : t.nonempty) (h_bdd : bdd_above t) :

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.

theorem Inf_within_of_ord_connected {α : Type u_1} {s : set α} [hs : s.ord_connected] ⦃t : set s⦄ (ht : t.nonempty) (h_bdd : bdd_below t) :

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.

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

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

Equations