projectiveSeminormAux_add_le — Mathlib

English

ProjectiveSeminormAux is subadditive: projectiveSeminormAux(p + q) ≤ projectiveSeminormAux(p) + projectiveSeminormAux(q).

Русский

Проективная семиномормa подсуммна: projectiveSeminormAux(p + q) ≤ projectiveSeminormAux(p) + projectiveSeminormAux(q).

LaTeX

$$$ \\mathrm{projectiveSeminormAux}(p + q) \\leq \\mathrm{projectiveSeminormAux}(p) + \\mathrm{projectiveSeminormAux}(q) $$$

Lean4

theorem projectiveSeminormAux_add_le (p q : FreeAddMonoid (𝕜 × Π i, E i)) :
    projectiveSeminormAux (p + q) ≤ projectiveSeminormAux p + projectiveSeminormAux q := by simp [projectiveSeminormAux]

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