instContMDiffMulOfSomeENatTopOfLEInfty

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
instance {a : WithTop ℕ∞} [ContMDiffMul I ∞ G] [h : ENat.LEInfty a] : ContMDiffMul I a G :=
  ContMDiffMul.of_le h.out

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