isOpen_iff_ball_subset — Mathlib

English

A set s is open iff for every x in s there exists V in the uniformity such that the ball around x with V is contained in s.

Русский

Множество открыто тогда и только тогда, когда для каждого x из него существует V из равномерности, такое что шар вокруг x ради V целиком содержится в s.

LaTeX

$$$\text{IsOpen}(s) \iff \forall x \in s, \exists V \in \mathcal U(\alpha), \operatorname{ball}(x,V) \subseteq s$$$

Lean4

/-- See also `isOpen_iff_isOpen_ball_subset`. -/
theorem isOpen_iff_ball_subset {s : Set α} : IsOpen s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s := by
  simp_rw [isOpen_iff_mem_nhds, nhds_eq_comap_uniformity, mem_comap, ball]

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