minSmoothness_add — Mathlib

English

The operation of adding an integer m to the analysis variable translates into a corresponding shift on the smoothness: minSmoothness 𝕜 (n + m) = minSmoothness 𝕜 n + m.

Русский

При добавлении целого m к аргумента анализируемого параметра гладкость изменяется на то же количество: minSmoothness 𝕜 (n + m) = minSmoothness 𝕜 n + m.

LaTeX

$$$$ \\minSmoothness_{\\mathbb{k}}(n+m) = \\minSmoothness_{\\mathbb{k}}(n) + m. $$$$

Lean4

theorem minSmoothness_add {n m : WithTop ℕ∞} : minSmoothness 𝕜 (n + m) = minSmoothness 𝕜 n + m :=
  by
  simp only [minSmoothness]
  split_ifs <;> simp

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