liftPropWithinAt_indep_chart — Mathlib

English

Equivalence of LiftPropWithinAt expressions when using charts both on source and target under invariance assumptions.

Русский

Эквивалентность выражений LiftPropWithinAt при использовании чартов и на источнике, и на цели.

LaTeX

$$$\mathrm{LiftPropWithinAt}(P,g, s, x) \iff \mathrm{LiftPropWithinAt}(P,g, s, x).$$$

Lean4

theorem liftPropWithinAt_indep_chart [HasGroupoid M G] [HasGroupoid M' G'] (he : e ∈ G.maximalAtlas M)
    (xe : x ∈ e.source) (hf : f ∈ G'.maximalAtlas M') (xf : g x ∈ f.source) :
    LiftPropWithinAt P g s x ↔ ContinuousWithinAt g s x ∧ P (f ∘ g ∘ e.symm) (e.symm ⁻¹' s) (e x) :=
  by
  simp only [liftPropWithinAt_iff']
  exact
    and_congr_right <|
      hG.liftPropWithinAt_indep_chart_aux (chart_mem_maximalAtlas _ _) (mem_chart_source _ _) he xe
        (chart_mem_maximalAtlas _ _) (mem_chart_source _ _) hf xf

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