English
If IsManifold I n M and IsManifold I' n M' with hn ≠ ∞, ContMDiffAt I I' n f x is equivalent to the existence of a neighborhood on which ContMDiffOn holds.
Русский
Если существуют условия IsManifold I n M и IsManifold I' n M' с hn ≠ ∞, то ContMDiffAt I I' n f x эквивалентно существованию окрестности, на которой ContMDiffOn выполняется.
LaTeX
$$$ ContMDiffAt I I' n f x \iff ∃ u ∈ 𝓝 x, ContMDiffOn I I' n f u $$$
Lean4
theorem contMDiffOn_iff_source_of_mem_maximalAtlas [IsManifold I n M] (he : e ∈ maximalAtlas I n M)
(hs : s ⊆ e.source) : ContMDiffOn I I' n f s ↔ ContMDiffOn 𝓘(𝕜, E) I' n (f ∘ (e.extend I).symm) (e.extend I '' s) :=
by
simp_rw [ContMDiffOn, Set.forall_mem_image]
refine forall₂_congr fun x hx => ?_
rw [contMDiffWithinAt_iff_source_of_mem_maximalAtlas he (hs hx)]
apply contMDiffWithinAt_congr_set
simp_rw [e.extend_symm_preimage_inter_range_eventuallyEq hs (hs hx)]
