hom_inv_id_apply

Mathlib.Topology.Category.TopCat.Basic

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

English

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

Русский

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

LaTeX

$$$f^{-1}(f(x)) = x$$$

Lean4

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

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

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

Разделы

Аффилиация

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