coe_trans

Mathlib.Topology.OpenPartialHomeomorph

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

English

The coercion of the trans composition to a function is the same as composing the functions in the reverse order.

Русский

Переход к функции от композиции trans совпадает с композицией функций в обратном порядке.

LaTeX

$$$ (\\mathrm{e.trans}\\mathrm{e'} : X \\to Z) = \\mathrm{e'} \\circ \\mathrm{e} $$$

Lean4

@[simp, mfld_simps]
theorem coe_trans : (e.trans e' : X → Z) = e' ∘ e :=
  rfl

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

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

Разделы

Аффилиация

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