isOpen_iff — Mathlib

English

Characterization: open sets are exactly those where every point has a ball around it contained in the set.

Русский

Характеризация: открытые множества — именно те, в которых для каждой точки имеется шар вокруг неё, целиком лежащий в множестве.

LaTeX

$$$\mathrm{IsOpen}(s) \iff \forall x \in s, \exists \varepsilon>0: B(x, \varepsilon) \subseteq s$$$

Lean4

theorem isOpen_iff : IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ball x ε ⊆ s := by simp only [isOpen_iff_mem_nhds, mem_nhds_iff]

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