inv_hom_id_apply

Mathlib.Topology.Category.TopCat.Basic

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

English

For an isomorphism f: X ≅ Y and y ∈ Y, the composition f.hom (f.inv y) equals y.

Русский

Для изоморфизма f: X ≅ Y и y ∈ Y, композиция f.hom (f.inv y) равна y.

LaTeX

$$$f(hom)(f.inv(y)) = y$$$

Lean4

theorem inv_hom_id_apply {X Y : TopCat} (f : X ≅ Y) (y : Y) : f.hom (f.inv y) = y := by simp

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

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

Разделы

Аффилиация

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