English
Let 𝔖 be a family of subsets of α and V a subset of β × β. Then the basic entourage on α →ᵤ[𝔖] β corresponding to (S, V) is exactly the preimage of the basic entourage on S →ᵤ β under the restriction map to S. In other words, UniformOnFun.gen 𝔖 S V is the pullback of UniformFun.gen S β V along the map that sends a pair (f, g) to the pair (f|S, g|S).
Русский
Пусть 𝔖 — семейство подмножеств α и V ⊆ β × β. Тогда базовое окружение в пространстве α →ᵤ[𝔖] β, соответствующее паре (S, V), есть точная предобразка базового окружения в S →ᵤ β по тождественному ограничению к S.
LaTeX
$$$\displaystyle \ UniformOnFun.gen\ 𝔖\ S\ V = \big(\mathrm{Prod.map}(S\restriction \circ \mathrm{UniformFun.toFun},\; S\restriction \circ \mathrm{UniformFun.toFun})\big)^{-1}\big(\mathrm{UniformFun.gen}\ S\ β\ V\big) $$$
Lean4
/-- For `S : Set α` and `V : Set (β × β)`, we have
`UniformOnFun.gen 𝔖 S V = (S.restrict × S.restrict) ⁻¹' (UniformFun.gen S β V)`.
This is the crucial fact for proving that the family `UniformOnFun.gen S V` for `S ∈ 𝔖` and
`V ∈ 𝓤 β` is indeed a basis for the uniformity `α →ᵤ[𝔖] β` endowed with `𝒱(α, β, 𝔖, uβ)`
the uniform structure of `𝔖`-convergence, as defined in `UniformOnFun.uniformSpace`. -/
protected theorem gen_eq_preimage_restrict {𝔖} (S : Set α) (V : Set (β × β)) :
UniformOnFun.gen 𝔖 S V =
Prod.map (S.restrict ∘ UniformFun.toFun) (S.restrict ∘ UniformFun.toFun) ⁻¹' UniformFun.gen S β V :=
by
ext uv
exact ⟨fun h ⟨x, hx⟩ => h x hx, fun h x hx => h ⟨x, hx⟩⟩
