English
If a property p holds for all elements of the domain, then p holds almost everywhere with respect to any measure μ.
Русский
Если свойство p выполняется для всех элементов пространства, то оно выполняется почти всюду относительно любой меры μ.
LaTeX
$$$(\forall a, p(a)) \Rightarrow \forall^{\text{ae}} a\, (p(a)).$$$
Lean4
/-- The “almost everywhere” filter of co-null sets. -/
def ae (μ : F) : Filter α :=
.ofCountableUnion (μ · = 0) (fun _S hSc ↦ (measure_sUnion_null_iff hSc).2) fun _t ht _s hs ↦ measure_mono_null hs ht