smul_sup — Mathlib

English

Scalar action distributes over sup: r • (p ⊔ q) = (r • p) ⊔ (r • q).

Русский

Скалярное действие распределяется по верхнему пределу: 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 : AddGroupSeminorm 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 _ _

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