lift_openEmbedding_symm_target — Mathlib

English

The target of the inverse lift_openEmbedding is the image of e.source under f.

Русский

Цель обратного поднятого отображения равна изображению источника e под действием f.

LaTeX

$$$ (e.lift_openEmbedding hf).symm.target = f '' e.source $$$

Lean4

@[simp, mfld_simps]
theorem lift_openEmbedding_symm_target (e : OpenPartialHomeomorph X Z) (hf : IsOpenEmbedding f) :
    (e.lift_openEmbedding hf).symm.target = f '' e.source := by
  rw [OpenPartialHomeomorph.symm_target, e.lift_openEmbedding_source]

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