leftInverse_bijInv

Mathlib.Data.Fintype.Inv

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

English

If f is bijective, then bijInv f_bij is a left inverse of f; i.e., (bijInv f_bij) followed by f equals the identity.

Русский

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

LaTeX

$$$\\text{LeftInverse } (bijInv\_f)\\ f$$$

Lean4

theorem leftInverse_bijInv (f_bij : Bijective f) : LeftInverse (bijInv f_bij) f := fun a =>
  f_bij.left (choose_spec (fun a' => f a' = f a) _)

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

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

Разделы

Аффилиация

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