ae_le_iff_absolutelyContinuous

Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

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

← MathLib Explorer

English

ae μ ≤ ae ν if and only if μ ≪ ν.

Русский

ae μ ≤ ae ν тогда и только тогда, когда μ ≪ ν.

LaTeX

$$$ae(\mu) \le ae(\nu) \iff \mu \ll \nu$$$

Lean4

theorem ae_le_iff_absolutelyContinuous : ae μ ≤ ae ν ↔ μ ≪ ν :=
  ⟨fun h s => by
    rw [measure_eq_zero_iff_ae_notMem, measure_eq_zero_iff_ae_notMem]
    exact fun hs => h hs, fun h _ hs => h hs⟩

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

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

Разделы

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

Аффилиация

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