liftPropWithinAt_indep_chart_target

English

Analogous invariance result for the target side with respect to two charts f and f' in the atlas.

Русский

Аналогично, но для целевой стороны: инвариантность при смене чарта в атласе.

LaTeX

$$$P (f \circ g) (s) (x) \iff P (f' \circ g) (s) (x).$$$

Lean4

/-- A version of `liftPropWithinAt_indep_chart`, only for the target. -/
theorem liftPropWithinAt_indep_chart_target [HasGroupoid M' G'] (hf : f ∈ G'.maximalAtlas M') (xf : g x ∈ f.source) :
    LiftPropWithinAt P g s x ↔ ContinuousWithinAt g s x ∧ LiftPropWithinAt P (f ∘ g) s x :=
  by
  rw [liftPropWithinAt_self_target, liftPropWithinAt_iff', and_congr_right_iff]
  intro hg
  simp_rw [(f.continuousAt xf).comp_continuousWithinAt hg, true_and]
  exact
    hG.liftPropWithinAt_indep_chart_target_aux (mem_chart_source _ _) (chart_mem_maximalAtlas _ _)
      (mem_chart_source _ _) hf xf hg

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