English
The uniform structure on α →ᵤ[𝔖] β is the infimum, over S ∈ 𝔖, of the pullback of the uniform structure on S →ᵤ β by restriction to S.
Русский
Равномерная структура на α →ᵤ[𝔖] β есть наименьшее (перводимое) по S ∈ 𝔖 вытягивание равномерной структуры на S →ᵤ β через ограничение к S.
LaTeX
$$$\mathcal U(α→ᵤ[𝔖]β) = \bigwedge_{S∈𝔖}\mathrm{comap}\big( S.restrict \circ \mathrm{UniformOnFun.toFun} 𝔖 \big)\mathcal U(S,β).$$$
Lean4
/-- Uniform structure of `𝔖`-convergence, i.e uniform convergence on the elements of `𝔖`,
declared as an instance on `α →ᵤ[𝔖] β`. It is defined as the infimum, for `S ∈ 𝔖`, of the pullback
by `S.restrict`, the map of restriction to `S`, of the uniform structure `𝒰(s, β, uβ)` on
`↥S →ᵤ β`. We will denote it `𝒱(α, β, 𝔖, uβ)`, where `uβ` is the uniform structure on `β`. -/
instance uniformSpace : UniformSpace (α →ᵤ[𝔖] β) :=
⨅ (s : Set α) (_ : s ∈ 𝔖), .comap (UniformFun.ofFun ∘ s.restrict ∘ UniformOnFun.toFun 𝔖) 𝒰(s, β, _)
