Subtypes of conditionally complete linear orders #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

subset_has_Sup s = {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)}

source

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

source

theorem subset_Sup_of_within {α : Type u_1} (s : set α) [has_Sup α] [inhabited ↥s] {t : set ↥s} (h : has_Sup.Sup (coe '' t) ∈ s) :

has_Sup.Sup (coe '' t) = ↑(has_Sup.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

subset_has_Inf s = {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)}

source

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

source

theorem subset_Inf_of_within {α : Type u_1} (s : set α) [has_Inf α] [inhabited ↥s] {t : set ↥s} (h : has_Inf.Inf (coe '' t) ∈ s) :

has_Inf.Inf (coe '' t) = ↑(has_Inf.Inf t)

source

@[reducible]

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 → has_Sup.Sup (coe '' t) ∈ s) (h_Inf : ∀ {t : set ↥s}, t.nonempty → bdd_below t → has_Inf.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

subset_conditionally_complete_linear_order s h_Sup h_Inf = {sup := lattice.sup (distrib_lattice.to_lattice ↥s), le := lattice.le (distrib_lattice.to_lattice ↥s), lt := lattice.lt (distrib_lattice.to_lattice ↥s), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf (distrib_lattice.to_lattice ↥s), inf_le_left := _, inf_le_right := _, le_inf := _, Sup := has_Sup.Sup (subset_has_Sup s), Inf := has_Inf.Inf (subset_has_Inf s), le_cSup := _, cSup_le := _, cInf_le := _, le_cInf := _, le_total := _, decidable_le := linear_order.decidable_le infer_instance, decidable_eq := linear_order.decidable_eq infer_instance, decidable_lt := linear_order.decidable_lt infer_instance, max_def := _, min_def := _}

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) :

has_Sup.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) :

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

ord_connected_subset_conditionally_complete_linear_order s = subset_conditionally_complete_linear_order s Sup_within_of_ord_connected Inf_within_of_ord_connected