English
Duplicate formulation under the same hypothesis as the previous item, reaffirming the lifted equality.
Русский
Дубликат формулировки под тем же предположением, повторяющий перенос равенства.
LaTeX
$$ContMDiffWithinAt I I' n f s x \iff ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (e.extend I).symm) ((e.extend I).symm ⁻¹' s ∩ range I) (e.extend I x)$$
Lean4
/-- One can reformulate being `Cⁿ` within a set at a point as being `Cⁿ` in the source space when
composing with the extended chart. -/
theorem contMDiffWithinAt_iff_source :
ContMDiffWithinAt I I' n f s x ↔
ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (extChartAt I x).symm) ((extChartAt I x).symm ⁻¹' s ∩ range I)
(extChartAt I x x) :=
by
simp_rw [ContMDiffWithinAt, liftPropWithinAt_iff']
have :
ContinuousWithinAt f s x ↔
ContinuousWithinAt (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (extChartAt I x x) :=
by
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· apply h.comp_of_eq
· exact (continuousAt_extChartAt_symm x).continuousWithinAt
· exact (mapsTo_preimage _ _).mono_left inter_subset_left
· exact extChartAt_to_inv x
· rw [← continuousWithinAt_inter (extChartAt_source_mem_nhds (I := I) x)]
have : ContinuousWithinAt ((f ∘ ↑(extChartAt I x).symm) ∘ ↑(extChartAt I x)) (s ∩ (extChartAt I x).source) x :=
by
apply h.comp (continuousAt_extChartAt x).continuousWithinAt
intro y hy
have : (chartAt H x).symm ((chartAt H x) y) = y := OpenPartialHomeomorph.left_inv _ (by simpa using hy.2)
simpa [this] using hy.1
apply this.congr
· intro y hy
have : (chartAt H x).symm ((chartAt H x) y) = y := OpenPartialHomeomorph.left_inv _ (by simpa using hy.2)
simp [this]
· simp
rw [← this]
simp only [ContDiffWithinAtProp, mfld_simps, preimage_comp, comp_assoc]
