ae_eq_empty — Mathlib

English

A set s is almost everywhere empty exactly when its μ-measure is 0.

Русский

Множество s равно нулю почти всюду тогда и только тогда, когда μ(s) = 0.

LaTeX

$$$s =ᵐ[\mu] \emptyset \iff \mu(s) = 0$$$

Lean4

@[simp]
theorem ae_eq_empty : s =ᵐ[μ] (∅ : Set α) ↔ μ s = 0 :=
  eventuallyEq_empty.trans <| by
    simp only [ae_iff, Classical.not_not, setOf_mem_eq]
      -- The priority should be higher than `eventuallyEq_univ`.

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