map_rightInverse_iff

Mathlib.Data.List.Basic

URI: https://scilib.ai/kg/mathlib#List.map_rightInverse_iff

English

RightInverse (map f) (map g) is equivalent to RightInverse f g.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem map_rightInverse_iff {f : α → β} {g : β → α} : RightInverse (map f) (map g) ↔ RightInverse f g :=
  map_leftInverse_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru