liftPropOn_chart_symm — Mathlib

English

From LocalInvariantProp, LiftPropOn for chartAt H x and its source holds.

Русский

Из локальной инвариантности следует LiftPropOn для chartAt H x и его source.

LaTeX

$$LiftPropOn Q (chartAt H x).toFun' (chartAt H x).source$$

Lean4

theorem liftPropOn_chart_symm [HasGroupoid M G] (hG : G.LocalInvariantProp G Q) (hQ : ∀ y, Q id univ y) :
    LiftPropOn Q (chartAt (H := H) x).symm (chartAt H x).target :=
  hG.liftPropOn_symm_of_mem_maximalAtlas hQ (chart_mem_maximalAtlas G x)

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