inclusionMapIso_inv

Mathlib.Topology.Category.TopCat.OpenNhds

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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