English
Invariance under source atlas changes yields equivalence of germ expressions when preimages are respected.
Русский
При изменении источника сохраняется эквивалентность выражений жерма.
LaTeX
$$$P((f\circ g)\circ e^{-1})(s)(x) \iff P((f'\circ g)\circ e^{-1})(s)(x).$$$
Lean4
/-- A version of `liftPropWithinAt_indep_chart`, that uses `LiftPropWithinAt` on both sides. -/
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 ∧ LiftPropWithinAt P (f ∘ g ∘ e.symm) (e.symm ⁻¹' s) (e x) :=
by
rw [hG.liftPropWithinAt_indep_chart he xe hf xf, liftPropWithinAt_self, and_left_comm, Iff.comm,
and_iff_right_iff_imp]
intro h
have h1 := (e.symm.continuousWithinAt_iff_continuousWithinAt_comp_right xe).mp h.1
have : ContinuousAt f ((g ∘ e.symm) (e x)) := by simp_rw [Function.comp, e.left_inv xe, f.continuousAt xf]
exact this.comp_continuousWithinAt h1
