smul_nnreal

Mathlib.MeasureTheory.Measure.MutuallySingular

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.MutuallySingular.smul_nnreal

English

If ν ⟂ μ, then r · ν ⟂ μ for any r ∈ ℝ≥0.

Русский

Если ν ⟂ₘ μ, то для любого r ∈ ℝ≥0 выполняется r · ν ⟂ₘ μ.

LaTeX

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

Lean4

theorem smul_nnreal (r : ℝ≥0) (h : ν ⟂ₘ μ) : r • ν ⟂ₘ μ :=
  h.smul r

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru