lift_openEmbedding_toFun — Mathlib

English

The lifted open embedding is equal to extend f over e's toFun' function, i.e., lifted map coincides with the extension of e.

Русский

Поднятое отображение совпадает с продолжением f над функцией toFun' e.

LaTeX

$$$ (e.lift_openEmbedding hf).toFun' = \text{extend} f e.toFun' \text{ ... }$$$

Lean4

@[simp, mfld_simps]
theorem lift_openEmbedding_toFun (e : OpenPartialHomeomorph X Z) (hf : IsOpenEmbedding f) :
    (e.lift_openEmbedding hf) = extend f e (fun _ ↦ (Classical.arbitrary Z)) :=
  rfl

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