lift_openEmbedding_symm_source — Mathlib

English

The source of the inverse lift_openEmbedding equals the target of the original open partial homeomorphism.

Русский

Источник обратного lifts равен цели исходного открытого частичного гомеоморфизма.

LaTeX

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

Lean4

@[simp, mfld_simps]
theorem lift_openEmbedding_symm_source (e : OpenPartialHomeomorph X Z) (hf : IsOpenEmbedding f) :
    (e.lift_openEmbedding hf).symm.source = e.target :=
  rfl

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