instContMDiffMulOfNatWithTopENat — Mathlib

English

If there is C^∞ multiplication, then for any a with a ≤ ∞, there is C^a multiplication.

Русский

Если есть бесконечно гладкое умножение, то для любого a с a ≤ ∞ существует C^a гладкость умножения.

LaTeX

$$$$ (\text{ContMDiffMul } I \infty G) \land (ENat.LEInfty a) \Rightarrow \ContMDiffMul I a G $$$$

Lean4

@[to_additive]
instance [ContMDiffMul I 2 G] : ContMDiffMul I 1 G :=
  ContMDiffMul.of_le one_le_two

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