insert_ae_eq_self — Mathlib

English

Adding a point a to a set s changes it only on a μ-null set; thus insert a s equals s almost everywhere.

Русский

Добавление точки a к множеству s изменяет его только на нулевую меру; поэтому insert a s равняется s почти повсеместно.

LaTeX

$$(insert a s) =_{\mu-\text{a.e.}} s$$

Lean4

theorem insert_ae_eq_self (a : α) (s : Set α) : (insert a s : Set α) =ᵐ[μ] s :=
  union_ae_eq_right.2 <| measure_mono_null diff_subset (measure_singleton _)

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