English
Let φ: α → β and ψ: β → α with φ ∘ ψ = id. If hφ: Tendsto φ f g and hψ: Tendsto ψ g f, then map φ f = g.
Русский
Пусть φ: α → β и ψ: β → α, φ ∘ ψ = id. Если Tendsto φ f g и Tendsto ψ g f, то map φ f = g.
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{map} \\phi f = g$$$
Lean4
theorem map_eq_of_inverse {f : Filter α} {g : Filter β} {φ : α → β} (ψ : β → α) (eq : φ ∘ ψ = id) (hφ : Tendsto φ f g)
(hψ : Tendsto ψ g f) : map φ f = g :=
by
refine le_antisymm hφ (le_trans ?_ (map_mono hψ))
rw [map_map, eq, map_id]
