English
For any f : γ → β, 𝒱(α, γ, 𝔖, comap f) equals 𝒱(α, β, 𝔖, _) comapped by (f ∘ ·).
Русский
Для любого f: γ → β имеет место 𝒱(α, γ, 𝔖, comap f) = 𝒱(α, β, 𝔖, u) comap (f ∘ ·).
LaTeX
$$𝒱(α, γ, 𝔖, \\mathrm{comap}\, f) = 𝒱(α, β, 𝔖, _) .comap (f ∘ \\cdot).$$
Lean4
/-- If `u` is a uniform structure on `β` and `f : γ → β`, then
`𝒱(α, γ, 𝔖, comap f u) = comap (fun g ↦ f ∘ g) 𝒱(α, γ, 𝔖, u₁)`. -/
protected theorem comap_eq {f : γ → β} : 𝒱(α, γ, 𝔖, ‹UniformSpace β›.comap f) = 𝒱(α, β, 𝔖, _).comap (f ∘ ·) := by
-- We reduce this to `UniformFun.comap_eq` using the fact that `comap` distributes
-- on `iInf`.
simp_rw [UniformOnFun.uniformSpace, UniformSpace.comap_iInf, UniformFun.comap_eq, ← UniformSpace.comap_comap]
-- By definition, `∀ S ∈ 𝔖, (f ∘ —) ∘ S.restrict = S.restrict ∘ (f ∘ —)`.
rfl
