hom_inv_id_apply

Mathlib.CategoryTheory.FintypeCat

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

English

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

Русский

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

LaTeX

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

Lean4

theorem hom_inv_id_apply {X Y : FintypeCat} (f : X ≅ Y) (x : X) : f.inv (f.hom x) = x :=
  congr_fun f.hom_inv_id x

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

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

Разделы

Аффилиация

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