English
Let g be a right inverse of f on a set t ⊆ β. 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 t; equivalently, for every F with F ≤ 𝓟(t), map g (map f F) = F.
Русский
Пусть g является правым обратным к f на множество t ⊆ β. Тогда индуцированные отображения на фильтрах удовлетворяют, что композиция map g после map f действует как тождество на каждом фильтре, содержащемся в главном фильтре 𝓟(t); то есть для каждого F с F ≤ 𝓟(t) выполняется map g (map f F) = F.
LaTeX
$$$RightInvOn\\ g\\ f\\ t \\Rightarrow RightInvOn\\ (map\\ g)\\ (map\\ f)\\ (Iic\\ (\\mathcal{P}(t)))$$$
Lean4
nonrec theorem _root_.Set.RightInvOn.filter_map_Iic {f : α → β} {g : β → α} (hfg : RightInvOn g f t) :
RightInvOn (map g) (map f) (Iic <| 𝓟 t) :=
hfg.filter_map_Iic
