dense_iff_exists_between — Mathlib

English

For a densely ordered, nontrivial type α with order topology, a set s is dense iff for all a<b there exists c∈s with a<c<b.

Русский

Для плотно упорядоченного непустого типа α с порядковой топологией множество s плотное тогда и только тогда, когда для всех a<b существует c∈s с a<c<b.

LaTeX

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

Lean4

/-- A set in a nontrivial densely linear ordered type is dense in the sense of topology if and only if for any `a < b` there exists `c ∈ s`, `a < c < b`. Each implication requires less typeclass assumptions. -/ theorem dense_iff_exists_between [OrderTopology α] [DenselyOrdered α] [Nontrivial α] {s : Set α} : Dense s ↔ ∀ a b, a < b → ∃ c ∈ s, a < c ∧ c < b := ⟨fun h _ _ hab => h.exists_between hab, dense_of_exists_between⟩

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