rightInverse_symm

Mathlib.Logic.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#Equiv.rightInverse_symm

English

For a bijection f : α ≃ β, RightInverse f.symm f holds, i.e., f ∘ f.symm = id.

Русский

Для биекции f : α ≃ β выполнено правый обратный: f.symm ∘ f = id.

LaTeX

$$RightInverse (f.symm) f$$

Lean4

theorem rightInverse_symm (f : α ≃ β) : Function.RightInverse f.symm f :=
  f.right_inv

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

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

Разделы

Аффилиация

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