English
If certain atlas compatibilities hold and g is continuous within s at x, then P(f∘g, s, x) is equal to P(f'∘g, s, x) for two target charts f, f'.
Русский
При совместимости атласов и непрерывности g в s при x свойство P для выражений через f и через f' совпадает.
LaTeX
$$$P (f \circ g)\, s\, x \iff P (f' \circ g)\, s\, x.$$$
Lean4
/-- `LiftPropWithinAt P f s x` is equivalent to a definition where we restrict the set we are
considering to the domain of the charts at `x` and `f x`. -/
theorem liftPropWithinAt_iff {f : M → M'} :
LiftPropWithinAt P f s x ↔
ContinuousWithinAt f s x ∧
P (chartAt H' (f x) ∘ f ∘ (chartAt H x).symm)
((chartAt H x).target ∩ (chartAt H x).symm ⁻¹' (s ∩ f ⁻¹' (chartAt H' (f x)).source)) (chartAt H x x) :=
by
rw [liftPropWithinAt_iff']
refine and_congr_right fun hf ↦ hG.congr_set ?_
exact
OpenPartialHomeomorph.preimage_eventuallyEq_target_inter_preimage_inter hf (mem_chart_source H x)
(chart_source_mem_nhds H' (f x))
