English
A simplified simp lemma variant of the maximal atlas condition for ContMDiffOn.
Русский
Упрощенная лемма для условия максимального атласа ContMDiffOn.
LaTeX
$$$contMDiffOn\_iff\_of\_mem\_maximalAtlas'\_simp\_1\_2$$$
Lean4
/-- One can reformulate being `C^n` on a set as continuity on this set, and being `C^n` in any
extended chart. -/
theorem contMDiffOn_iff :
ContMDiffOn I I' n f s ↔
ContinuousOn f s ∧
∀ (x : M) (y : M'),
ContDiffOn 𝕜 n (extChartAt I' y ∘ f ∘ (extChartAt I x).symm)
((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)) :=
by
constructor
· intro h
refine ⟨fun x hx => (h x hx).1, fun x y z hz => ?_⟩
simp only [mfld_simps] at hz
let w := (extChartAt I x).symm z
have : w ∈ s := by simp only [w, hz, mfld_simps]
specialize h w this
have w1 : w ∈ (chartAt H x).source := by simp only [w, hz, mfld_simps]
have w2 : f w ∈ (chartAt H' y).source := by simp only [w, hz, mfld_simps]
convert ((contMDiffWithinAt_iff_of_mem_source w1 w2).mp h).2.mono _
· simp only [w, hz, mfld_simps]
· mfld_set_tac
· rintro ⟨hcont, hdiff⟩ x hx
refine (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_iff.mpr ?_
refine ⟨hcont x hx, ?_⟩
dsimp [ContDiffWithinAtProp]
convert hdiff x (f x) (extChartAt I x x) (by simp only [hx, mfld_simps]) using 1
mfld_set_tac
