liftPropOn_of_mem_groupoid — Mathlib

English

If there exists a maximal atlas and the maximal atlas membership holds, LiftPropAt for any chart in the atlas holds.

Русский

Если существует максимальный атлас и выполняется членство, LiftPropAt для любого чарта атласа выполняется.

LaTeX

$$LiftPropAt Q e x$$

Lean4

theorem liftPropOn_of_mem_groupoid (hG : G.LocalInvariantProp G Q) (hQ : ∀ y, Q id univ y)
    {f : OpenPartialHomeomorph H H} (hf : f ∈ G) : LiftPropOn Q f f.source :=
  liftPropOn_of_mem_maximalAtlas hG hQ (G.mem_maximalAtlas_of_mem_groupoid hf)

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