projectiveSeminormAux_nonneg — Mathlib

English

The values of projectiveSeminormAux are nonnegative: 0 ≤ projectiveSeminormAux p for all p.

Русский

Значения projectiveSeminormAux неотрицательны: 0 ≤ projectiveSeminormAux p для всех p.

LaTeX

$$$ 0 \\leq \\mathrm{projectiveSeminormAux}(p) $$$

Lean4

theorem projectiveSeminormAux_nonneg (p : FreeAddMonoid (𝕜 × Π i, E i)) : 0 ≤ projectiveSeminormAux p :=
  by
  simp only [projectiveSeminormAux]
  refine List.sum_nonneg ?_
  intro a
  simp only [List.mem_map, Prod.exists, forall_exists_index, and_imp]
  intro x m _ h
  rw [← h]
  exact mul_nonneg (norm_nonneg _) (Finset.prod_nonneg (fun _ _ ↦ norm_nonneg _))

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