absolutelyContinuous_of_le_smul

Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

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

← MathLib Explorer

English

If μ' ≤ c • μ for some c, then μ' is absolutely continuous with respect to μ.

Русский

Если μ' ≤ c • μ, то μ' ≪ μ.

LaTeX

$$$μ' \le c \cdot μ \Rightarrow μ' \ll μ$$$

Lean4

theorem absolutelyContinuous_of_le_smul {μ' : Measure α} {c : ℝ≥0∞} (hμ'_le : μ' ≤ c • μ) : μ' ≪ μ :=
  (Measure.absolutelyContinuous_of_le hμ'_le).trans smul_absolutelyContinuous

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

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

Разделы

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

Аффилиация

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