ae_eq_top — Mathlib

English

The almost-everywhere filter equals the top filter iff every singleton has nonzero measure.

Русский

Пусть ae μ равен верхнему фильтру тогда и только тогда, когда каждое синглтон имеет ненулевую меру.

LaTeX

$$$\operatorname{ae}(\mu) = \top \iff \forall a, \mu\{a\} \neq 0$$$

Lean4

@[simp]
theorem ae_eq_top : ae μ = ⊤ ↔ ∀ a, μ { a } ≠ 0 :=
  by
  simp only [Filter.ext_iff, mem_ae_iff, mem_top, ne_eq]
  refine ⟨fun h a ha ↦ by simpa [ha] using (h { a }ᶜ).1, fun h s ↦ ⟨fun hs ↦ ?_, ?_⟩⟩
  · rw [← compl_empty_iff, ← not_nonempty_iff_eq_empty]
    rintro ⟨a, ha⟩
    exact h _ <| measure_mono_null (singleton_subset_iff.2 ha) hs
  · rintro rfl
    simp

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