English
Let g be a left inverse of f on a set s ⊆ α. Then the induced maps on filters satisfy that the composition map g after map f acts as the identity on every filter contained in the principal filter on s; equivalently, for every F with F ≤ 𝓟(s), map g (map f F) = F.
Русский
Пусть g является левым обратным к f на множестве s ⊆ α. Тогда индуцированные отображения на фильтрах удовлетворяют, что композиция map g после map f действует как тождественное отображение на каждом фильтре, содержащемся в главном фильтре 𝓟(s); то есть для каждого F с F ≤ 𝓟(s) выполнится map g (map f F) = F.
LaTeX
$$$LeftInvOn\\ g\\ f\\ s \\Rightarrow LeftInvOn\\ (map\\ g)\\ (map\\ f)\\ (Iic\\ (\\mathcal{P}(s)))$$$
Lean4
theorem _root_.Set.LeftInvOn.filter_map_Iic {f : α → β} {g : β → α} (hfg : LeftInvOn g f s) :
LeftInvOn (map g) (map f) (Iic <| 𝓟 s) := fun F (hF : F ≤ 𝓟 s) ↦
by
have : (g ∘ f) =ᶠ[𝓟 s] id := by simpa only [eventuallyEq_principal] using hfg
rw [map_map, map_congr (this.filter_mono hF), map_id]
