nhds_basis_uniformity' — Mathlib

English

If a basis (p,s) for the uniformity is given, then the neighborhoods of x have a basis consisting of balls centered at x with the sets s i.

Русский

Если дана база (p,s) для равномерности, окрестности x имеют базис шаров, центрируемых в x и использующих множества s i.

LaTeX

$$$(\mathcal N_x) \text{ has basis } p \text{ with } i \mapsto \operatorname{ball}(x, s_i)$$$

Lean4

theorem nhds_basis_uniformity' {p : ι → Prop} {s : ι → Set (α × α)} (h : (𝓤 α).HasBasis p s) {x : α} :
    (𝓝 x).HasBasis p fun i => ball x (s i) :=
  by
  rw [nhds_eq_comap_uniformity]
  exact h.comap (Prod.mk x)

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