snd — Mathlib

English

The second coordinate projection remains C^n after restricting to a subset.

Русский

Вторая координатная проекция остается C^n на подмножстве.

LaTeX

$$contMDiffWithinAt_snd {s : Set (M × N)} {p : M × N} : ContMDiffWithinAt (I.prod J) J n Prod.snd s p$$

Lean4

theorem snd {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).2) s x :=
  contMDiffWithinAt_snd.comp x hf (mapsTo_image f s)

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