English
Let φ: α → β and ψ: β → α with ψ ∘ φ = id. If hφ: Tendsto φ f g and hψ: Tendsto ψ g f, then comap φ g = f.
Русский
Пусть φ: α → β и ψ: β → α, причём ψ ∘ φ = id. Если Tendsto φ f g и Tendsto ψ g f, то comap φ g = f.
LaTeX
$$$\\forall f:\\mathrm{Filter}(\\alpha), \\forall g:\\mathrm{Filter}(\\beta), \\forall \\phi:\\alpha \\to \\beta, \\forall \\psi:\\beta \\to \\alpha, \\; (\\psi \\circ \\phi) = \\mathrm{id} \\Rightarrow \\mathrm{Tendsto} \\phi f g \\Rightarrow \\mathrm{Tendsto} \\psi g f \\Rightarrow \\mathrm{comap} \\phi g = f$$$
Lean4
theorem comap_eq_of_inverse {f : Filter α} {g : Filter β} {φ : α → β} (ψ : β → α) (eq : ψ ∘ φ = id) (hφ : Tendsto φ f g)
(hψ : Tendsto ψ g f) : comap φ g = f :=
by
refine ((comap_mono <| map_le_iff_le_comap.1 hψ).trans ?_).antisymm (map_le_iff_le_comap.1 hφ)
rw [comap_comap, eq, comap_id]
