inv_hom_id_apply

Mathlib.CategoryTheory.FintypeCat

URI: https://scilib.ai/kg/mathlib#FintypeCat.inv_hom_id_apply

English

If f: X ≅ Y, then f.hom ∘ f.inv = id_Y (and f.inv ∘ f.hom = id_X).

Русский

Если f: X ≅ Y, то f.hom ∘ f.inv = id_Y и f.inv ∘ f.hom = id_X.

LaTeX

$$$f \\circ f^{-1} = \\mathrm{id}_Y \\quad\\text{and}\\quad f^{-1} \\circ f = \\mathrm{id}_X$$$

Lean4

theorem inv_hom_id_apply {X Y : FintypeCat} (f : X ≅ Y) (y : Y) : f.hom (f.inv y) = y :=
  congr_fun f.inv_hom_id y

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

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

Разделы

Аффилиация

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