ae_le_set

Mathlib.MeasureTheory.OuterMeasure.AE

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

← MathLib Explorer

English

s ≤ᵐ t iff μ(s \ t) = 0

Русский

s ≤ᵐ t эквивалентно μ(s \ t) = 0

LaTeX

$$$s \leq_{\mathrm{a.e.}} t \iff \mu(s \setminus t) = 0$$$

Lean4

theorem ae_le_set : s ≤ᵐ[μ] t ↔ μ (s \ t) = 0 :=
  calc
    s ≤ᵐ[μ] t ↔ ∀ᵐ x ∂μ, x ∈ s → x ∈ t := Iff.rfl
    _ ↔ μ (s \ t) = 0 := by simp [ae_iff]; rfl

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

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

Разделы

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

Аффилиация

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