smul_left — Mathlib

English

Let h be an AC relation μ ≪ ν. Then for any scalar c, c • μ ≪ c • ν.

Русский

Пусть μ ≪ ν. Тогда для любого скаляра c выполняется c • μ ≪ c • ν.

LaTeX

$$$\mu \ll \nu \rightarrow (c \cdot \mu) \ll (c \cdot \nu)$$$

Lean4

protected theorem smul_left [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (h : μ ≪ ν) (c : R) : c • μ ≪ ν := fun s hνs => by
  simp only [h hνs, smul_apply, smul_zero, ← smul_one_smul ℝ≥0∞ c (0 : ℝ≥0∞)]

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