fst — Mathlib

English

The projection to the first component, (f x)1, preserves C^n regularity: if f is ContMDiffWithinAt, then its first component is ContMDiffWithinAt.

Русский

Проекция на первую компоненту сохраняет гладкость C^n.

LaTeX

$$ContMDiffWithinAt (I.prod J) I n Prod.fst s p → ContMDiffWithinAt J I n Prod.fst s p$$

Lean4

theorem fst {f : N → M × M'} {s : Set N} {x : N} (hf : ContMDiffWithinAt J (I.prod I') n f s x) :
    ContMDiffWithinAt J I n (fun x => (f x).1) s x :=
  contMDiffWithinAt_fst.comp x hf (mapsTo_image f s)

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