English
Let f: α → β, g1,g2: β → α, and filters fa on α, fb on β. If g1 ∘ f = id on fa eventually and f ∘ g2 = id on fb eventually, and Tendsto g2 fb fa, then g1 and g2 are eventually equal with respect to fb: g1 =ᶠ[fb] g2.
Русский
Пусть f: α → β, g1,g2: β → α и фильтры fa на α, fb на β. Если g1 ∘ f равно id на fa позднее по fa, и f ∘ g2 равно id на fb позднее по fb, и Tendsto g2 fb fa, тогда g1 и g2 совпадают на fb: g1 =ᶠ[fb] g2.
LaTeX
$$$\\forall f:\\alpha \\to \\beta, \\forall g_1,g_2:\\beta \\to \\alpha, \\forall fa:\\mathrm{Filter}(\\alpha), \\forall fb:\\mathrm{Filter}(\\beta),\\; (\\forall^\infty x\\in fa,\\; g_1(f(x))=x) \\land (\\forall^\infty y\\in fb,\\; f(g_2(y))=y) \\land \\mathrm{Tendsto}(g_2)\\; fb\\; fa \\Rightarrow g_1 =^{fb} g_2$$$
Lean4
theorem eventuallyEq_of_left_inv_of_right_inv {f : α → β} {g₁ g₂ : β → α} {fa : Filter α} {fb : Filter β}
(hleft : ∀ᶠ x in fa, g₁ (f x) = x) (hright : ∀ᶠ y in fb, f (g₂ y) = y) (htendsto : Tendsto g₂ fb fa) :
g₁ =ᶠ[fb] g₂ :=
(htendsto.eventually hleft).mp <| hright.mono fun _ hr hl => (congr_arg g₁ hr.symm).trans hl
