weightedSMul_nonneg — Mathlib

English

If μ s = μ t, then the weightedSMul converges to the same linear operator for s and t.

Русский

Если μ s = μ t, то weightedSMul μ s = weightedSMul μ t.

LaTeX

$$$$weightedSMul μ s = weightedSMul μ t \quad\text{iff } μ s = μ t.$$$$

Lean4

theorem weightedSMul_nonneg [PartialOrder F] [IsOrderedModule ℝ F] (s : Set α) (x : F) (hx : 0 ≤ x) :
    0 ≤ weightedSMul μ s x :=
  by
  simp only [weightedSMul, coe_smul', _root_.id, coe_id', Pi.smul_apply]
  exact smul_nonneg toReal_nonneg hx

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