smul_finite

Mathlib.MeasureTheory.Measure.Typeclasses.Finite

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

← MathLib Explorer

English

If μ is locally finite and c ∈ ℝ≥0, then c • μ is locally finite.

Русский

Если μ локально конечна и c ∈ ℝ≥0, то c • μ локально конечна.

LaTeX

$$IsLocallyFiniteMeasure (c • μ)$$

Lean4

theorem smul_finite (μ : Measure α) [IsFiniteMeasure μ] {c : ℝ≥0∞} (hc : c ≠ ∞) : IsFiniteMeasure (c • μ) :=
  by
  lift c to ℝ≥0 using hc
  exact MeasureTheory.isFiniteMeasureSMulNNReal

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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