contMDiffWithinAt_proj — Mathlib

English

The projection π F E is ContMDiffAt when restricted to any set s inside the total space, i.e., within At, the projection map is differentiable of class C^n.

Русский

Проекция π F E гладка внутри множества s в общем пространстве, то есть на уровне ContMDiffWithinAt.

LaTeX

$$$\displaystyle \operatorname{ContMDiffWithinAt} (IB. prod 𝓘(𝕜, F)) IB n \; \pi F E\ s\ x.$$$

Lean4

theorem contMDiffWithinAt_proj {s : Set (TotalSpace F E)} {p : TotalSpace F E} :
    ContMDiffWithinAt (IB.prod 𝓘(𝕜, F)) IB n (π F E) s p :=
  (contMDiffAt_proj E).contMDiffWithinAt

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