lift_openEmbedding_trans_apply — Mathlib

English

If e and e' are open partial homeomorphisms X→Z, and f is an open embedding, then lifting along f preserves the composition: the lifted inverse composition equals the original composition.

Русский

Пусть e и e' — открытые частичные гомеоморфизмы X→Z, и f — открытое вложение; подъем вдоль f сохраняет композицию: поднятая обратная композиция равна исходной композиции.

LaTeX

$$$(e.lift_openEmbedding hf)^{-1} \\circ (e'.lift_openEmbedding hf) = e^{-1} \\circ e'\\;$ как функции, применяемые к аргумента Z$$

Lean4

theorem lift_openEmbedding_trans_apply (e e' : OpenPartialHomeomorph X Z) (hf : IsOpenEmbedding f) (z : Z) :
    (e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf) z = (e.symm.trans e') z := by
  simp [hf.injective.extend_apply e']

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