English
An alternate form under the maximal atlas hypothesis: C^n within is equivalent to C^n in a lifted atlas via the maximal atlas membership.
Русский
Альтернативная форма при условии максимального атласа: ContMDiffWithinAt эквивалентно C^n в поднятом атласе.
LaTeX
$$theorem contMDiffWithinAt_iff_of_mem_maximalAtlas {x : M} (he : e ∈ maximalAtlas I n M) (he' : e' ∈ maximalAtlas I' n M') (hx : x ∈ e.source) (hy : f x ∈ e'.source) : ContMDiffWithinAt I I' n f s x ↔ ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (e'.extend I' ∘ f ∘ (e.extend I).symm) ((e.extend I).symm ⁻¹' s ∩ range I) (e.extend I x)$$
Lean4
theorem contMDiffWithinAt_iff_of_mem_maximalAtlas {x : M} (he : e ∈ maximalAtlas I n M)
(he' : e' ∈ maximalAtlas I' n M') (hx : x ∈ e.source) (hy : f x ∈ e'.source) :
ContMDiffWithinAt I I' n f s x ↔
ContinuousWithinAt f s x ∧
ContDiffWithinAt 𝕜 n (e'.extend I' ∘ f ∘ (e.extend I).symm) ((e.extend I).symm ⁻¹' s ∩ range I)
(e.extend I x) :=
(contDiffWithinAt_localInvariantProp n).liftPropWithinAt_indep_chart he hx he' hy
