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 _ _