hasBasis_nhds_of_basis — Mathlib

English

For a fixed function f ∈ α →ᵤ β and a basis of 𝓤β, the neighborhoods of f in α →ᵤ β have a basis consisting of sets { g : (f,g) ∈ UniformFun.gen α β (s i) } as i ranges.

Русский

Для фиксированной функции f ∈ α →ᵤβ, если взять базис 𝓤β, базис окрестностей f в α →ᵤβ задается множествами { g : (f,g) ∈ UniformFun.gen α β (s i) }.

LaTeX

$$$$ (\mathcal N f) \text{ has basis } \{ g : (f,g) \in \mathrm{UniformFun.gen}(α,β,s_i) \} $$$$

Lean4

/-- For `f : α →ᵤ β`, `𝓝 f` admits the family `{g | ∀ x, (f x, g x) ∈ V}` for `V ∈ 𝓑` as a filter
basis, for any basis `𝓑` of `𝓤 β`. -/
protected theorem hasBasis_nhds_of_basis (f) {p : ι → Prop} {s : ι → Set (β × β)} (h : HasBasis (𝓤 β) p s) :
    (𝓝 f).HasBasis p fun i => {g | (f, g) ∈ UniformFun.gen α β (s i)} :=
  nhds_basis_uniformity' (UniformFun.hasBasis_uniformity_of_basis α β h)

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