filter_map — Mathlib

English

If g is a left inverse of f, then map g is a left inverse of map f.

Русский

Если g является левой обратной для f, то map g является левой обратной для map f.

LaTeX

$$$ \text{Function.LeftInverse}(g,f) \Rightarrow \text{Function.LeftInverse}(\mathrm{Filter.map} g, \mathrm{Filter.map} f) $$$

Lean4

theorem _root_.Function.LeftInverse.filter_map {f : α → β} {g : β → α} (hfg : LeftInverse g f) :
    LeftInverse (map g) (map f) := fun F ↦ by rw [map_map, hfg.comp_eq_id, map_id]

Похожие утверждения