hasMFDerivAt_snd — Mathlib

English

The first projection is MF-differentiable as a map from the product to the base, i.e. MDifferentiable (I.prod I′) I Prod.fst.

Русский

Первая проекция является MF-дифференцируемой отображением из произведения в основание.

LaTeX

$$$\mathrm{MDifferentiable}(I\prod I',\,I,\,\mathrm{Prod.fst})$$$

Lean4

theorem hasMFDerivAt_snd (x : M × M') :
    HasMFDerivAt (I.prod I') I' Prod.snd x (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)) :=
  by
  refine ⟨continuous_snd.continuousAt, ?_⟩
  have :
    ∀ᶠ y in 𝓝[range (I.prod I')] extChartAt (I.prod I') x x,
      (extChartAt I' x.2 ∘ Prod.snd ∘ (extChartAt (I.prod I') x).symm) y = y.2 :=
    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.2).right_inv hy.2
  apply HasFDerivWithinAt.congr_of_eventuallyEq hasFDerivWithinAt_snd this
  exact (extChartAt I' x.2).right_inv <| (extChartAt I' x.2).map_source (mem_extChartAt_source _)

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