isOpen_iff_isOpen_ball_subset — Mathlib

English

A set s is open iff for every x ∈ s there exists an entourage V with V open and ball x V ⊆ s.

Русский

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

LaTeX

$$$IsOpen s \iff \forall x \in s, \exists V ∈ 𝓤 α, IsOpen V ∧ ball\, x\, V ⊆ s$$$

Lean4

theorem isOpen_iff_isOpen_ball_subset {s : Set α} : IsOpen s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen V ∧ ball x V ⊆ s :=
  by
  rw [isOpen_iff_ball_subset]
  constructor <;> intro h x hx
  · obtain ⟨V, hV, hV'⟩ := h x hx
    exact ⟨interior V, interior_mem_uniformity hV, isOpen_interior, (ball_mono interior_subset x).trans hV'⟩
  · obtain ⟨V, hV, -, hV'⟩ := h x hx
    exact ⟨V, hV, hV'⟩

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