English
Another simplication lemma in the maximal atlas setting.
Русский
Ещё одна упрощенная лемма в рамках атласа максимального диапазона.
LaTeX
$$$contMDiffOn\_iff\_of\_mem\_maximalAtlas'\_simp\_1\_1$$$
Lean4
/-- One can reformulate being `C^n` on a set as continuity on this set, and being `C^n` in any
extended chart in the target. -/
theorem contMDiffOn_iff_target :
ContMDiffOn I I' n f s ↔
ContinuousOn f s ∧
∀ y : M', ContMDiffOn I 𝓘(𝕜, E') n (extChartAt I' y ∘ f) (s ∩ f ⁻¹' (extChartAt I' y).source) :=
by
simp only [contMDiffOn_iff, ModelWithCorners.source_eq, chartAt_self_eq, OpenPartialHomeomorph.refl_partialEquiv,
PartialEquiv.refl_trans, extChartAt, OpenPartialHomeomorph.extend, Set.preimage_univ, Set.inter_univ,
and_congr_right_iff]
intro h
constructor
· refine fun h' y => ⟨?_, fun x _ => h' x y⟩
have h'' : ContinuousOn _ univ := (ModelWithCorners.continuous I').continuousOn
convert (h''.comp_inter (chartAt H' y).continuousOn_toFun).comp_inter h
simp
· exact fun h' x y => (h' y).2 x 0
