trans_refl

Mathlib.Topology.OpenPartialHomeomorph

URI: https://scilib.ai/kg/mathlib#OpenPartialHomeomorph.trans_refl

English

Composing with a reflexive identity on Y yields the original map: e.trans refl Y = e.

Русский

Сложение с тождественным отображением на Y возвращает исходное отображение: e.trans refl Y = e.

LaTeX

$$$ e.trans(\\mathrm{refl}~Y) = e $$$

Lean4

@[simp, mfld_simps]
theorem trans_refl : e.trans (OpenPartialHomeomorph.refl Y) = e :=
  toPartialEquiv_injective e.1.trans_refl

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

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

Разделы

Аффилиация

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