instDenselyOrdered — Mathlib

English

In a densely ordered ambient order, any OrdConnected subset is densely ordered.

Русский

В плотно упорядоченном окружении любой OrdConnected подпоследовательность плотна упорядочена.

LaTeX

$$$[\text{DenselyOrdered }\alpha] \Rightarrow [s: Set\alpha][\;s.OrdConnected\;] \Rightarrow \operatorname{DenselyOrdered}(s)$$$

Lean4

/-- In a dense order `α`, the subtype from an `OrdConnected` set is also densely ordered. -/
instance instDenselyOrdered [DenselyOrdered α] {s : Set α} [hs : OrdConnected s] : DenselyOrdered s :=
  ⟨fun a b (h : (a : α) < b) =>
    let ⟨x, H⟩ := exists_between h
    ⟨⟨x, (hs.out a.2 b.2) (Ioo_subset_Icc_self H)⟩, H⟩⟩

Похожие утверждения