smul_sup — Mathlib

English

For r ∈ R and p, q ∈ NonarchAddGroupSeminorm E, r • (p ⊔ q) = (r • p) ⊔ (r • q).

Русский

Для r ∈ R и p, q ∈ NonarchAddGroupSeminorm E, r • (p ⊔ q) = (r • p) ⊔ (r • q).

LaTeX

$$$ r \cdot (p \sqcup q) = (r \cdot p) \sqcup (r \cdot q) $$$

Lean4

theorem smul_sup (r : R) (p q : NonarchAddGroupSeminorm E) : r • (p ⊔ q) = r • p ⊔ r • q :=
  have Real.smul_max : ∀ x y : ℝ, r • max x y = max (r • x) (r • y) := fun x y => by
    simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
      mul_max_of_nonneg x y (r • (1 : ℝ≥0) : ℝ≥0).coe_nonneg
  ext fun _ => Real.smul_max _ _

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