hasMFDerivAt_fst — Mathlib

English

Differentiability of the product map (fst, snd) along with differentiability of components.

Русский

Дифференцируемость произведения (fst, snd) вместе с дифференцируемостью компонент.

LaTeX

$$$ MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 E') f x \to MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 E'') g x $$$

Lean4

theorem hasMFDerivAt_fst (x : M × M') :
    HasMFDerivAt (I.prod I') I Prod.fst x (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)) :=
  by
  refine ⟨continuous_fst.continuousAt, ?_⟩
  have :
    ∀ᶠ y in 𝓝[range (I.prod I')] extChartAt (I.prod I') x x,
      (extChartAt I x.1 ∘ Prod.fst ∘ (extChartAt (I.prod I') x).symm) y = y.1 :=
    by
    /- porting note: was
        apply Filter.mem_of_superset (extChartAt_target_mem_nhdsWithin (I.prod I') x)
        mfld_set_tac
        -/

    filter_upwards [extChartAt_target_mem_nhdsWithin x] with y hy
    rw [extChartAt_prod] at hy
    exact (extChartAt I x.1).right_inv hy.1
  apply HasFDerivWithinAt.congr_of_eventuallyEq hasFDerivWithinAt_fst this
  exact (extChartAt I x.1).right_inv <| (extChartAt I x.1).map_source (mem_extChartAt_source _)

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