English
Under suitable hypotheses, the uniformity on UniformOnFun α β 𝔖 has a HasBasis described by pairs (S, V) with S ∈ 𝔖 and V a basis element of 𝓤 β, via UniformOnFun.gen 𝔖 S V.
Русский
При надлежащих гипотезах равномерность на UniformOnFun α β 𝔖 имеет HasBasis, задаваемый парами (S, V) с S∈𝔖 и V — базис 𝓤 β, через UniformOnFun.gen 𝔖 S V.
LaTeX
$$$\text{HasBasis }(\mathcal U(α→ᵤ[𝔖]β))\ (\lambda (S,i) => S∈𝔖 ∧ i∈ ?),\; (f,g) \mapsto \mathrm{UniformOnFun.gen} 𝔖 S (s i).$$$
Lean4
/-- For `f : α →ᵤ[𝔖] β`, where `𝔖 : Set (Set α)` is nonempty and directed, `𝓝 f` admits the
family `{g | ∀ x ∈ S, (f x, g x) ∈ V}` for `S ∈ 𝔖` and `V ∈ 𝓑` as a filter basis, for any basis
`𝓑` of `𝓤 β`. -/
protected theorem hasBasis_nhds_of_basis (f : α →ᵤ[𝔖] β) (h : 𝔖.Nonempty) (h' : DirectedOn (· ⊆ ·) 𝔖) {p : ι → Prop}
{s : ι → Set (β × β)} (hb : HasBasis (𝓤 β) p s) :
(𝓝 f).HasBasis (fun Si : Set α × ι => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si =>
{g | (g, f) ∈ UniformOnFun.gen 𝔖 Si.1 (s Si.2)} :=
letI : UniformSpace (α → β) := UniformOnFun.uniformSpace α β 𝔖
nhds_basis_uniformity (UniformOnFun.hasBasis_uniformity_of_basis α β 𝔖 h h' hb)
