fst — Mathlib

English

For p in the tangent bundle of the product, the tangent mapWithin for Prod.fst with set s coincides with the same output ⟨p.proj.1, p.2.1⟩.

Русский

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

LaTeX

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

Lean4

theorem fst {f : N → M × M'} {s : Set N} {x : N} (hf : MDifferentiableWithinAt J (I.prod I') f s x) :
    MDifferentiableWithinAt J I (fun x => (f x).1) s x :=
  mdifferentiableAt_fst.comp_mdifferentiableWithinAt x hf

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