ae_dirac_iff — Mathlib

English

For measurable p with MeasurableSet {x | p x}, (∀ᵐ x ∂dirac a, p x) holds if and only if p a.

Русский

Для измеримого p с MeasurableSet {x | p x} верно: (∀ᵐ x ∂dirac a, p x) тогда и только тогда, когда p a истинно.

LaTeX

$$$ (∀ᵐ x ∂dirac a, p x) \\iff p a $$$

Lean4

theorem ae_dirac_iff {a : α} {p : α → Prop} (hp : MeasurableSet {x | p x}) : (∀ᵐ x ∂dirac a, p x) ↔ p a :=
  mem_ae_dirac_iff hp

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