exists_Ioo_subset — Mathlib

English

In a densely ordered nontrivial type α with OrderTopology, Dense s 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 ∀ a

Lean4

theorem exists_Ioo_subset [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] {a : α} {p : α → Prop}
    (hp : ∀ᶠ x in 𝓝 a, p x) : ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ {x | p x} :=
  mem_nhds_iff_exists_Ioo_subset.1 hp

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