smul_sup — Mathlib

English

For r ∈ R, p, q seminorms on E, we have r • (p ⊔ q) = (r • p) ⊔ (r • q).

Русский

Для r ∈ R и полунорм p, q на 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 [SMul R ℝ] [SMul R ℝ≥0] [IsScalarTower R ℝ≥0 ℝ] (r : R) (p q : Seminorm 𝕜 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 _ _

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