bijective_bijInv

Mathlib.Data.Fintype.Inv

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

English

If f is bijective, then bijInv f_bij is itself a bijection.

Русский

Если f биективна, то bijInv f_bij сама является биекция.

LaTeX

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

Lean4

theorem bijective_bijInv (f_bij : Bijective f) : Bijective (bijInv f_bij) :=
  ⟨(rightInverse_bijInv _).injective, (leftInverse_bijInv _).surjective⟩

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

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

Разделы

Аффилиация

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