smul_sSup — Mathlib

English

For a scalar c and set s, c • sSup s = ⨆ a ∈ s, c • a.

Русский

Для скаляра c и множества s: c • sSup s = ⨆_{a ∈ s} (c • a).

LaTeX

$$$c \\cdot \\operatorname{sSup} s = \\displaystyle \\sup_{a \\in s} c \\cdot a$$$

Lean4

theorem smul_sSup {R} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (s : Set ℝ≥0∞) (c : R) : c • sSup s = ⨆ a ∈ s, c • a :=
  by simp_rw [← smul_one_mul c (sSup s), ENNReal.mul_sSup, smul_one_mul]

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