smul — Mathlib

English

If ν ⟂ μ, then r · ν ⟂ μ for any scalar r ≥ 0∞.

Русский

Если ν ⟂ₘ μ, то для любого скалярa r ≥ 0∞ выполняется r · ν ⟂ₘ μ.

LaTeX

$$$$ \\nu \\perp_{m} \\mu \\;\Rightarrow\ \\, r \\cdot \\nu \\perp_{m} \\mu \\quad (r \\in \\mathbb{R}_{\\ge 0}^{\\infty}). $$$$

Lean4

theorem smul (r : ℝ≥0∞) (h : ν ⟂ₘ μ) : r • ν ⟂ₘ μ :=
  h.mono_ac (AbsolutelyContinuous.rfl.smul_left r) AbsolutelyContinuous.rfl

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