map_leftInverse_iff — Mathlib

English

LeftInverse (map f) (map g) holds if and only if LeftInverse f g.

Русский

LeftInverse (map f) (map g) эквивалентно LeftInverse f g.

LaTeX

$$$\\\\operatorname{LeftInverse} (\\\\operatorname{List.map} f) (\\\\operatorname{List.map} g) \\\\iff \\\\operatorname{LeftInverse} f g.$$$

Lean4

@[simp]
theorem map_leftInverse_iff {f : α → β} {g : β → α} : LeftInverse (map f) (map g) ↔ LeftInverse f g :=
  ⟨fun h x => by injection h [x], (·.list_map)⟩

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