contDiffWithinAt_snd — Mathlib

English

If g: E1 × E2 → G, f1: F → E1, f2: F → E2 are C^n, then the map x ↦ g(f1(x), f2(x)) is C^n.

Русский

Если g: E1 × E2 → G, f1: F → E1, f2: F → E2 гладкие порядка n, то x ↦ g(f1(x), f2(x)) гладко порядка n.

LaTeX

$$$\mathrm{ContDiff}_{\mathbb{k}}\ n\ g \to\ (f_1, f_2) \mapsto g(f_1(x), f_2(x))$ is ContDiff 𝕜 n.$$

Lean4

/-- The second projection within a domain at a point in a product is `C^∞`. -/
@[fun_prop]
theorem contDiffWithinAt_snd {s : Set (E × F)} {p : E × F} : ContDiffWithinAt 𝕜 n (Prod.snd : E × F → F) s p :=
  contDiff_snd.contDiffWithinAt

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