dense_of_exists_between — Mathlib

English

Let α be a nontrivial densely ordered OrderTopology. A set s is dense iff for every a<b there exists c∈s with a<c<b.

Русский

Пусть α — не тривиальная плотно упорядоченная множество с OrderTopology. Множество s плотное тогда и только тогда, когда для любых a<b существует c∈s с a<c<b.

LaTeX

$$$\\text{Dense}(s) \\iff \\forall a,b\\ (a

Lean4

theorem dense_of_exists_between [OrderTopology α] [Nontrivial α] {s : Set α} (h : ∀ ⦃a b⦄, a < b → ∃ c ∈ s, a < c ∧ c < b) : Dense s := by refine dense_iff_inter_open.2 fun U U_open U_nonempty => ?_ obtain ⟨a, b, hab, H⟩ : ∃ a b : α, a < b ∧ Ioo a b ⊆ U := U_open.exists_Ioo_subset U_nonempty obtain ⟨x, xs, hx⟩ : ∃ x ∈ s, a < x ∧ x < b := h hab exact ⟨x, ⟨H hx, xs⟩⟩

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