English
A further variant under the same hypothesis, providing another route to the lifted expression.
Русский
Еще одна вариация при тех же гипотезах, дающая другой путь к перенесенному выражению.
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
/-- An alternative formulation of `contMDiffWithinAt_iff_of_mem_maximalAtlas`
if the set if `s` lies in `e.source`. -/
theorem contMDiffWithinAt_iff_image {x : M} (he : e ∈ maximalAtlas I n M) (he' : e' ∈ maximalAtlas I' n M')
(hs : s ⊆ e.source) (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 '' s) (e.extend I x) :=
by
rw [contMDiffWithinAt_iff_of_mem_maximalAtlas he he' hx hy, and_congr_right_iff]
refine fun _ => contDiffWithinAt_congr_set ?_
simp_rw [e.extend_symm_preimage_inter_range_eventuallyEq hs hx]
