hasBasis_nhds — Mathlib

English

The neighborhood basis at f in α →ᵤ β can be taken from the sets { (f,g) ∈ UniformFun.gen α β (V) } with V ∈ 𝓤β; equivalently, (𝓝 f) has a basis given by those sets.

Русский

Окрестности с,nf в α →ᵤβ можно задавать через множества { (f,g) ∈ UniformFun.gen α β (V) } с V ∈ 𝓤β.

LaTeX

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

Lean4

/-- For `f : α →ᵤ β`, `𝓝 f` admits the family `{g | ∀ x, (f x, g x) ∈ V}` for `V ∈ 𝓤 β` as a
filter basis. -/
protected theorem hasBasis_nhds (f) : (𝓝 f).HasBasis (fun V => V ∈ 𝓤 β) fun V => {g | (f, g) ∈ UniformFun.gen α β V} :=
  UniformFun.hasBasis_nhds_of_basis α β f (Filter.basis_sets _)

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