ae_restrict_le

Mathlib.MeasureTheory.Measure.Restrict

URI: https://scilib.ai/kg/mathlib#MeasureTheory.ae_restrict_le

English

The a.e. restriction is nonempty (nontrivial) iff μ(s) ≠ 0.

Русский

Aе-ограничение не тривиально тогда, когда μ(s) ≠ 0.

LaTeX

$$$\text{ae}(μ|_s) \text{ is nontrivial } \iff μ(s) \neq 0.$$$

Lean4

theorem ae_restrict_le : ae (μ.restrict s) ≤ ae μ :=
  ae_mono restrict_le_self

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

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

Разделы

Аффилиация

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