English
Let μ be a measure on a measurable space and g: α → ℝ. The set of real numbers t for which the two tail-measure values μ{a : t ≤ g(a)} and μ{a : t < g(a)} differ is countable.
Русский
Пусть μ — мерa на измеримом пространстве и g: α → ℝ. Множество вещественных t, для которых значения мер хвостовых множеств μ{a | t ≤ g(a)} и μ{a | t < g(a)} различны, счётно.
LaTeX
$$$${\\{t \\in \\mathbb{R} \\mid \\mu\\{a: t \\le g(a)\\} \\neq \\mu\\{a: t < g(a)\\}\\}} \\text{ is countable. }$$$$
Lean4
theorem countable_meas_le_ne_meas_lt (g : α → R) : {t : R | μ {a : α | t ≤ g a} ≠ μ {a : α | t < g a}}.Countable := by
-- the target set is contained in the set of points where the function `t ↦ μ {a : α | t ≤ g a}`
-- jumps down on the right of `t`. This jump set is countable for any function.
let F : R → ℝ≥0∞ := fun t ↦ μ {a : α | t ≤ g a}
apply (countable_image_gt_image_Ioi F).mono
intro t ht
have : μ {a | t < g a} < μ {a | t ≤ g a} := lt_of_le_of_ne (measure_mono (fun a ha ↦ le_of_lt ha)) (Ne.symm ht)
exact ⟨μ {a | t < g a}, this, fun s hs ↦ measure_mono (fun a ha ↦ hs.trans_le ha)⟩
