ae_eq_dirac' — Mathlib

English

If the base space α is nonempty, there exists at least one probability measure on α; in particular δ_a for some a ∈ α is a probability measure.

Русский

Если множество α непусто, то существует хотя бы одна вероятностная мера на α; в частности δ_a для некоторого a ∈ α является вероятностной мерой.

LaTeX

$$$ ∃ a ∈ α, IsProbabilityMeasure( dirac a ) $$$

Lean4

theorem ae_eq_dirac' [MeasurableSingletonClass β] {a : α} {f : α → β} (hf : Measurable f) :
    f =ᵐ[dirac a] const α (f a) :=
  (ae_dirac_iff <| show MeasurableSet (f ⁻¹' {f a}) from hf <| measurableSet_singleton _).2 rfl

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