English
A variant of the above equivalence using a different decomposition of the chart expression with target or source restrictions.
Русский
Еще одна версия эквивалентности; выражение через другую декомпозицию графа с ограничениями узла и образа.
LaTeX
$$ContMDiffWithinAt I I' n f s x \iff (ContinuousWithinAt f s x) \land ContDiffWithinAt 𝕜 n (extChartAt I' (f x) ∘ f ∘ (extChartAt I x).symm) ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)) (extChartAt I x x)$$
Lean4
/-- One can reformulate being `Cⁿ` within a set at a point as continuity within this set at this
point, and being `Cⁿ` in the corresponding extended chart in the target. -/
theorem contMDiffWithinAt_iff_target :
ContMDiffWithinAt I I' n f s x ↔
ContinuousWithinAt f s x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n (extChartAt I' (f x) ∘ f) s x :=
by
simp_rw [ContMDiffWithinAt, liftPropWithinAt_iff', ← and_assoc]
have cont : ContinuousWithinAt f s x ∧ ContinuousWithinAt (extChartAt I' (f x) ∘ f) s x ↔ ContinuousWithinAt f s x :=
and_iff_left_of_imp <| (continuousAt_extChartAt _).comp_continuousWithinAt
simp_rw [cont, ContDiffWithinAtProp, extChartAt, OpenPartialHomeomorph.extend, PartialEquiv.coe_trans,
ModelWithCorners.toPartialEquiv_coe, OpenPartialHomeomorph.coe_coe, modelWithCornersSelf_coe, chartAt_self_eq,
OpenPartialHomeomorph.refl_apply, id_comp]
rfl
