liftPropAt_chart — Mathlib

English

From the LocalInvariantProp, the lift property holds for chartAt H x.

Русский

Из локальной инвариантности следует, что lift свойство верно для chartAt H x.

LaTeX

$$LiftPropAt Q (chartAt (H := H) x).toFun' x$$

Lean4

theorem liftPropAt_chart [HasGroupoid M G] (hG : G.LocalInvariantProp G Q) (hQ : ∀ y, Q id univ y) :
    LiftPropAt Q (chartAt (H := H) x) x :=
  hG.liftPropAt_of_mem_maximalAtlas hQ (chart_mem_maximalAtlas G x) (mem_chart_source H x)

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