pow — Mathlib

English

If every f_i is ContMDiffOn or ContMDiff at x, then the finite product ∏ i∈t f_i is ContMDiff at x.

Русский

Если каждый f_i дифференцируем по x, то конечное произведение дифференцируемо по x.

LaTeX

$$$\forall i, \ ContMDiff I' I n (f_i) \Rightarrow \ ContMDiff I' I n (\prod_{i} f_i) \, x$$$

Lean4

@[to_additive]
theorem pow (hg : ContMDiff I' I n g) (m : ℕ) : ContMDiff I' I n (fun x ↦ g x ^ m) := fun x ↦ (hg x).pow m

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