English
Let u_gamma be a uniform structure on γ, and f: α → β, g: β → γ. Then the uniform structure on α obtained by pulling back along g ∘ f equals the pullback along f of the pullback along g of u_γ.
Русский
Пусть u_γ — равномерная структура на γ, а f: α → β, g: β → γ. Тогда структура u_α, полученная как обратный образ по композиции g ∘ f, совпадает с обратным образом по f от обратного образа по g от u_γ.
LaTeX
$$$\\mathrm{UniformSpace.comap}(g \\circ f) \\, u_\\gamma \;=\\; \\mathrm{UniformSpace.comap} f\\big(\\mathrm{UniformSpace.comap} g\\, u_\\gamma\\)$$$
Lean4
theorem comap_comap {α β γ} {uγ : UniformSpace γ} {f : α → β} {g : β → γ} :
UniformSpace.comap (g ∘ f) uγ = UniformSpace.comap f (UniformSpace.comap g uγ) :=
by
ext1
simp only [uniformity_comap, Filter.comap_comap, Prod.map_comp_map]
