of_le — Mathlib

English

If m ≤ n and multiplication is C^n, then it is C^m.

Русский

Если m ≤ n и операция умножения гладко дифференцируема класса C^n, то она гладко дифференцируема класса C^m.

LaTeX

$$$$ m \le n \Rightarrow \ContMDiffMul I m G $$$$

Lean4

@[to_additive]
protected theorem of_le {m n : WithTop ℕ∞} (hmn : m ≤ n) [h : ContMDiffMul I n G] : ContMDiffMul I m G :=
  by
  have : IsManifold I m G := IsManifold.of_le hmn
  exact ⟨h.contMDiff_mul.of_le hmn⟩

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