hasBasis_nhds — Mathlib

English

There exists a basis of neighborhoods for nhds x consisting of balls with symmetric, uniformity-bounded sets as basis elements.

Русский

Существует базис окрестностей nhds x, состоящий из шаров с симметричными, ограниченными по равномерности множества.

LaTeX

$$$\text{HasBasis} (\mathcal N x) (\lambda s. s \in \mathcal U(\alpha) \land IsSymmetricRel s) (\lambda s. \operatorname{ball}(x,s))$$$

Lean4

theorem hasBasis_nhds (x : α) : HasBasis (𝓝 x) (fun s : Set (α × α) => s ∈ 𝓤 α ∧ IsSymmetricRel s) fun s => ball x s :=
  ⟨fun t => by simp [UniformSpace.mem_nhds_iff_symm, and_assoc]⟩

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