ae_eq_univ_iff_eq — Mathlib

English

Let F be closed. Then F equals the universe almost everywhere with respect to μ if and only if F equals the universe exactly, assuming OpensMeasurableSpace X and finite μ.

Русский

Пусть F замкнуто; тогда F равен всеобщности почти повсюду по отношению к μ тогда и только тогда, когда F равен всеобщности ровно, при условиях OpensMeasurableSpace X и сконечной меры μ.

LaTeX

$$$\\forall F,\\ IsClosed F \\rightarrow\\ (F =^{\\mu}_{ae} \\mathrm{univ}) \\iff F = \\mathrm{univ}.$$$

Lean4

theorem _root_.IsClosed.ae_eq_univ_iff_eq (hF : IsClosed F) : F =ᵐ[μ] univ ↔ F = univ :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩
  rwa [ae_eq_univ, hF.isOpen_compl.measure_eq_zero_iff μ, compl_empty_iff] at h

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