English
Let mab: α → β and mba: β → α, with f a filter on α and g a filter on β. If mab ∘ mba equals the identity on tail g (mab ∘ mba =ᶠ[g] id) and mba tends from g to f (Tendsto mba g f), then g is refined by mab-exact image of f, i.e. g ≤ map mab f.
Русский
Пусть mab: α → β и mba: β → α, фильтры f на α и g на β. Если mab ∘ mba эквивалентно тождественному отображению на хвосте g (mab ∘ mba =ᶠ[g] id) и mba диаграмма стремления переводит g в f (Tendsto mba g f), тогда g полезнее/строже чем образ f через mab: g ≤ map mab f.
LaTeX
$$$\\forall mab:\\alpha \\to \\beta, \\forall mba:\\beta \\to \\alpha, \\forall f:\\mathrm{Filter}(\\alpha), \\forall g:\\mathrm{Filter}(\\beta),\\; (mab \\circ mba =_{g} \\mathrm{id}) \\land \\mathrm{Tendsto}(mba)\\; g\\; f \\Rightarrow g \\le \\mathrm{map}(mab)\\; f$$$
Lean4
theorem le_map_of_right_inverse {mab : α → β} {mba : β → α} {f : Filter α} {g : Filter β} (h₁ : mab ∘ mba =ᶠ[g] id)
(h₂ : Tendsto mba g f) : g ≤ map mab f :=
by
rw [← @map_id _ g, ← map_congr h₁, ← map_map]
exact map_mono h₂
