contMDiffWithinAt_iff_target_of_mem_source

English

If x′ lies in the source of the chart x, then ContMDiffWithinAt is equivalent to a version with the source chart of x treated as the reference.

Русский

Если x′ лежит в источнике графа x, то ContMDiffWithinAt эквивалентно версии с источником графа x как опорной точкой.

LaTeX

$$ContMDiffWithinAt I I' n f s x' \iff ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) I' n (f ∘ (extChartAt I x).symm) (Set.preimage) ((extChartAt I x).symm ⁻¹' s ∩ range I) (extChartAt I x x')$$

Lean4

theorem contMDiffWithinAt_iff_target_of_mem_source [IsManifold I' n M'] {x : M} {y : M'}
    (hy : f x ∈ (chartAt H' y).source) :
    ContMDiffWithinAt I I' n f s x ↔
      ContinuousWithinAt f s x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n (extChartAt I' y ∘ f) s x :=
  by
  simp_rw [ContMDiffWithinAt]
  rw [(contDiffWithinAt_localInvariantProp n).liftPropWithinAt_indep_chart_target (chart_mem_maximalAtlas y) hy,
    and_congr_right]
  intro hf
  simp_rw [StructureGroupoid.liftPropWithinAt_self_target]
  simp_rw [((chartAt H' y).continuousAt hy).comp_continuousWithinAt hf]
  rw [← extChartAt_source (I := I')] at hy
  simp_rw [(continuousAt_extChartAt' hy).comp_continuousWithinAt hf]
  rfl

Похожие утверждения