instContMDiffAddSelf — Mathlib

English

If every f_i is ContMDiff I n (f_i) then the product map x ↦ ∏ i∈t f_i(x) is ContMDiff.

Русский

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

LaTeX

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

Lean4

instance instContMDiffAddSelf : ContMDiffAdd 𝓘(𝕜, E) n E :=
  by
  constructor
  rw [← modelWithCornersSelf_prod, chartedSpaceSelf_prod]
  exact contDiff_add.contMDiff

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