hasMFDerivWithinAt_fst — Mathlib

English

The first projection map is differentiable at (x,y) from a product manifold.

Русский

Первая проекция на произведении гладкая в точке (x,y).

LaTeX

$$$ mdifferentiableAt_fst {x} : MDifferentiableAt (I . prod I') I Prod.fst x $$$

Lean4

theorem hasMFDerivWithinAt_fst (s : Set (M × M')) (x : M × M') :
    HasMFDerivWithinAt (I.prod I') I Prod.fst s x
      (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)) :=
  (hasMFDerivAt_fst x).hasMFDerivWithinAt

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