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