measure_inter_eq_of_ae — Mathlib

English

If almost every element of t belongs to the subset s, then μ(t∩s) = μ(s).

Русский

Если почти для всех x из t выполняется x ∈ s, тогда μ(t∩s) = μ(s).

LaTeX

$$$$ (\\text{ae } x \\in t) \\Rightarrow \\mu(t \\cap s) = \\mu(s). $$$$

Lean4

theorem measure_inter_eq_of_ae {s t : Set α} (h : ∀ᵐ a ∂μ, a ∈ t) : μ (t ∩ s) = μ s :=
  by
  refine le_antisymm (measure_mono inter_subset_right) ?_
  apply EventuallyLE.measure_le
  filter_upwards [h] with x hx h'x using ⟨hx, h'x⟩

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