lift_openEmbedding_apply — Mathlib

English

The action of lift_openEmbedding on a point f x equals e x, i.e., lifting preserves original values on the image of f.

Русский

Действие lift_openEmbedding на точке f(x) равно e(x), то есть подъем сохраняет значения на образе f.

LaTeX

$$$ (e.lift_openEmbedding hf).toFun' (f x) = e.toFun' x $$$

Lean4

theorem lift_openEmbedding_apply (e : OpenPartialHomeomorph X Z) (hf : IsOpenEmbedding f) {x : X} :
    (lift_openEmbedding e hf) (f x) = e x :=
  by
  simp_rw [e.lift_openEmbedding_toFun]
  apply hf.injective.extend_apply

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