English
Same as above in a primed form, expressing equivalence between ContMDiffOn and its charted form when at paces in maximal atlases.
Русский
То же самое в форме с апострофом: эквивалентность ContMDiffOn и его координатной формы при мatan atlas.
LaTeX
$$$ContMDiffOn I I' n f s \;\Longleftrightarrow\; ContinuousOn f s \land ContDiffOn 𝕜 n (e'.extend I' \circ f \circ (e.extend I).symm) (e.extend I '' s)$$$
Lean4
theorem contMDiffOn_iff_of_mem_maximalAtlas' (he : e ∈ maximalAtlas I n M) (he' : e' ∈ maximalAtlas I' n M')
(hs : s ⊆ e.source) (h2s : MapsTo f s e'.source) :
ContMDiffOn I I' n f s ↔ ContDiffOn 𝕜 n (e'.extend I' ∘ f ∘ (e.extend I).symm) (e.extend I '' s) :=
(contMDiffOn_iff_of_mem_maximalAtlas he he' hs h2s).trans <|
and_iff_right_of_imp fun h ↦ (e.continuousOn_writtenInExtend_iff hs h2s).1 h.continuousOn
