prod — Mathlib

English

If each f_i is ContMDiff I' I n (f_i), then the finite product x ↦ ∏ i∈t f_i(x) is ContMDiff.

Русский

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

LaTeX

$$$\big( \forall i, \ ContMDiff I' I n (f_i) \big) \to \ ContMDiff I' I n (\lambda x, \prod_{i ∈ t} f_i(x))$$

Lean4

@[to_additive]
theorem prod (h : ∀ i ∈ t, ContMDiff I' I n (f i)) : ContMDiff I' I n fun x ↦ ∏ i ∈ t, f i x := fun x ↦
  ContMDiffAt.prod fun j hj ↦ h j hj x

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