meas_le_ae_eq_meas_lt — Mathlib

English

For any ν with no atoms and any g: α → ℝ, the two tail maps t ↦ μ{a : t ≤ g(a)} and t ↦ μ{a : t < g(a)} are equal ν-almost everywhere.

Русский

Для всякой меры ν без атомов и любой функции g: α → ℝ, два хвостовых отображения t ↦ μ{a: t ≤ g(a)} и t ↦ μ{a: t < g(a)} совпадают почти наверняка по ν.

LaTeX

$$$$ (\\,t \\mapsto \\mu\\{a:\\, t \\le g(a)\\}~) =_{\\text{ae},\\nu} (\\,t \\mapsto \\mu\\{a:\\, t < g(a)\\}). $$$$

Lean4

theorem meas_le_ae_eq_meas_lt {R : Type*} [LinearOrder R] [MeasurableSpace R] (ν : Measure R) [NoAtoms ν] (g : α → R) :
    (fun t => μ {a : α | t ≤ g a}) =ᵐ[ν] fun t => μ {a : α | t < g a} :=
  Set.Countable.measure_zero (countable_meas_le_ne_meas_lt μ g) _

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