contDiff — Mathlib

English

For every order n, smoothTransition is ContDiff of order n on the real line.

Русский

Для любого порядка n функция smoothTransition гладкая на ℝ (ContDiff для любого n).

LaTeX

$$$$ \operatorname{ContDiff}_{\mathbb{R}}(n, \operatorname{smoothTransition}) \quad \text{for all } n. $$$$

Lean4

@[fun_prop]
protected theorem contDiff {n : ℕ∞} : ContDiff ℝ n smoothTransition :=
  expNegInvGlue.contDiff.div
    (expNegInvGlue.contDiff.add <| expNegInvGlue.contDiff.comp <| contDiff_const.sub contDiff_id) fun x =>
    (pos_denom x).ne'

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