English
A secondary simp lemma variant for contMDiffOn with maximal atlas.
Русский
Вторичная упрощенная лемма для contMDiffOn в рамках максимального атласа.
LaTeX
$$$contMDiffOn\_iff\_of\_mem\_maximalAtlas'\_simp\_1\_2$$$
Lean4
/-- zero-smoothness on a set is equivalent to continuity on this set. -/
theorem contMDiffOn_zero_iff : ContMDiffOn I I' 0 f s ↔ ContinuousOn f s :=
by
rw [contMDiffOn_iff]
refine ⟨fun h ↦ h.1, fun h ↦ ⟨h, ?_⟩⟩
intro x y
rw [contDiffOn_zero]
apply (continuousOn_extChartAt _).comp
· apply h.comp ((continuousOn_extChartAt_symm _).mono inter_subset_left) (fun z hz ↦ ?_)
simp only [preimage_inter, mem_inter_iff, mem_preimage] at hz
exact hz.2.1
· intro z hz
simp only [preimage_inter, mem_inter_iff, mem_preimage] at hz
exact hz.2.2
