liftPropAt_symm_of_mem_maximalAtlas

English

If the LocalInvariantProp holds and the chart e is in the maximal atlas, then LiftPropAt Q e x holds for x in its source.

Русский

Если локальная инвариантность выполняется и чарт e принадлежит максимальному атласу, то LiftPropAt Q e x верно для x ∈ source.

LaTeX

$$LiftPropAt Q e x$$

Lean4

theorem liftPropAt_symm_of_mem_maximalAtlas [HasGroupoid M G] {x : H} (hG : G.LocalInvariantProp G Q)
    (hQ : ∀ y, Q id univ y) (he : e ∈ maximalAtlas M G) (hx : x ∈ e.target) : LiftPropAt Q e.symm x :=
  by
  suffices h : Q (e ∘ e.symm) univ x
    by
    have : e.symm x ∈ e.source := by simp only [hx, mfld_simps]
    rw [LiftPropAt, hG.liftPropWithinAt_indep_chart G.id_mem_maximalAtlas (mem_univ _) he this]
    refine ⟨(e.symm.continuousAt hx).continuousWithinAt, ?_⟩
    simp only [h, mfld_simps]
  exact hG.congr' (e.eventually_right_inverse hx) (hQ x)

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