fst'' — Mathlib

English

The first projection composed with a ContDiff function is ContDiff.

Русский

Первая проекция после композиции с функцией ContDiff — остаётся ContDiff.

LaTeX

$$$\forall x,\; \ContDiff 𝕜 n g \rightarrow \ContDiffAt 𝕜 n (\lambda p: (g p).1) x$$$

Lean4

/-- Precomposing `f` with `Prod.fst` is `C^n` at `x : E × F` -/
theorem fst'' {f : E → G} {x : E × F} (hf : ContDiffAt 𝕜 n f x.1) : ContDiffAt 𝕜 n (fun x : E × F => f x.1) x :=
  hf.comp x contDiffAt_fst

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