ae — Mathlib · SciLib

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

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