inclusionMapIso_hom

Mathlib.Topology.Category.TopCat.OpenNhds

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.OpenNhds.inclusionMapIso_hom

English

The horizontal component of the canonical isomorphism inclusionMapIso is the identity morphism.

Русский

Горизонтальная компонента канонического изоморфизма inclusionMapIso является тождественным мором.

LaTeX

$$$ (\mathrm{inclusionMapIso}\; f\; x).\mathrm{hom} = \mathrm{id} $$$

Lean4

@[simp]
theorem inclusionMapIso_hom (x : X) : (inclusionMapIso f x).hom = 𝟙 _ :=
  rfl

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

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

Разделы

Аффилиация

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