rightInverse_bijInv

Mathlib.Data.Fintype.Inv

URI: https://scilib.ai/kg/mathlib#Fintype.rightInverse_bijInv

English

If f is bijective, then bijInv f_bij is a right inverse of f; i.e., f∘bijInv f_bij equals id on β.

Русский

Если f биективно, то bijInv f_bij является правым обратным к f; то есть f( bijInv f_bij(b) ) = b.

LaTeX

$$$\\text{RightInverse } (bijInv f\\_bij)\\ f$$$

Lean4

theorem rightInverse_bijInv (f_bij : Bijective f) : RightInverse (bijInv f_bij) f := fun b =>
  choose_spec (fun a' => f a' = b) _

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

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

Разделы

Аффилиация

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