English
If two charts e and e' produce the same preimage of the source sets, then Pathwise properties carried by P are equivalent.
Русский
Если два чарта дают одинаковые предобразные множества источника, то соответствующие свойства P совпадают.
LaTeX
$$$P(\mathrm{toFun}' f \circ g) = P(\mathrm{toFun}' f' \circ g).$$$
Lean4
/-- If a property of a germ of function `g` on a pointed set `(s, x)` is invariant under the
structure groupoid (by composition in the source space and in the target space), then
expressing it in charted spaces does not depend on the element of the maximal atlas one uses
both in the source and in the target manifolds, provided they are defined around `x` and `g x`
respectively, and provided `g` is continuous within `s` at `x` (otherwise, the local behavior
of `g` at `x` cannot be captured with a chart in the target). -/
theorem liftPropWithinAt_indep_chart_aux (he : e ∈ G.maximalAtlas M) (xe : x ∈ e.source) (he' : e' ∈ G.maximalAtlas M)
(xe' : x ∈ e'.source) (hf : f ∈ G'.maximalAtlas M') (xf : g x ∈ f.source) (hf' : f' ∈ G'.maximalAtlas M')
(xf' : g x ∈ f'.source) (hgs : ContinuousWithinAt g s x) :
P (f ∘ g ∘ e.symm) (e.symm ⁻¹' s) (e x) ↔ P (f' ∘ g ∘ e'.symm) (e'.symm ⁻¹' s) (e' x) := by
rw [← Function.comp_assoc, hG.liftPropWithinAt_indep_chart_source_aux (f ∘ g) he xe he' xe', Function.comp_assoc,
hG.liftPropWithinAt_indep_chart_target_aux xe' hf xf hf' xf' hgs]
