trans_apply

Mathlib.Topology.OpenPartialHomeomorph

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

English

Applying the composed open partial homeomorphism to a point x yields applying e first and then e'.

Русский

Применение составного открытого частичного гомеоморфизма к точке x даёт сначала применение e, затем e'.

LaTeX

$$$ (e.trans e')\\,x = e'\\,(e\\,x) $$$

Lean4

theorem trans_apply {x : X} : (e.trans e') x = e' (e x) :=
  rfl

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

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

Разделы

Аффилиация

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