mfderivWithin_fst — Mathlib

English

For a subset s of M × M′, the tangent mapWithin for Prod.fst agrees with the tangential projection: tangentMapWithin (I.prod I′) I Prod.fst s p = ⟨p.proj.1, p.2.1⟩.

Русский

Для подмножества s произведения касательных отображений верно равенство tangentMapWithin для Prod.fst: ⟨p.proj.1, p.2.1⟩.

LaTeX

$$$\mathrm{tangentMapWithin}(I\prod I',\,I,\,Prod.fst\,s)\;p = \langle p.\mathrm{proj}.1,\; p.\mathrm{snd}.1\rangle$$$

Lean4

theorem mfderivWithin_fst {s : Set (M × M')} {x : M × M'} (hxs : UniqueMDiffWithinAt (I.prod I') s x) :
    mfderivWithin (I.prod I') I Prod.fst s x = ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2) :=
  by rw [MDifferentiable.mfderivWithin mdifferentiableAt_fst hxs]; exact mfderiv_fst

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