nhds_basis_uniformity — Mathlib

English

There is a basis for the neighborhoods of x given by the sets ball x (s i) where s i form a basis of the uniformity.

Русский

Существует базис окрестностей x, заданный шаром x по множествам s_i, образующим базис равномерности.

LaTeX

$$$(nhds 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 => {y | (y, x) ∈ s i} :=
  by
  replace h := h.comap Prod.swap
  rw [comap_swap_uniformity] at h
  exact nhds_basis_uniformity' h

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