smul_nnreal

Mathlib.MeasureTheory.Measure.Regular

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

English

If μ is regular, then c • μ is regular for any c ∈ ℝ≥0.

Русский

Если μ регулярная, то c•μ регуларна для любого c∈ℝ≥0.

LaTeX

$$$c \\in \\mathbb{R}_{\\ge 0} \\implies (c \\cdot \\mu) \\text{ Regular}.$$$

Lean4

instance smul_nnreal [Regular μ] (c : ℝ≥0) : Regular (c • μ) :=
  Regular.smul coe_ne_top

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

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

Разделы

Аффилиация

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