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⟩⟩