fst — Mathlib

English

If g is C^n at y and f is C^n within s at x with f(x)=y, then g ∘ f is ContDiffWithinAt on s at x.

Русский

Если g — C^n в y и f — C^n внутри s в x с условием f(x)=y, то g∘f — ContDiffWithinAt на s в x.

LaTeX

$$$\forall x,\; \ContDiffAt 𝕜 n g y \rightarrow \ContDiffWithinAt 𝕜 n f s x \rightarrow f x = y \rightarrow \ContDiffWithinAt 𝕜 n (g \circ f) s x$$$

Lean4

/-- Postcomposing `f` with `Prod.fst` is `C^n` -/
@[fun_prop]
theorem fst {f : E → F × G} (hf : ContDiff 𝕜 n f) : ContDiff 𝕜 n fun x => (f x).1 :=
  contDiff_fst.comp hf

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