ennreal_coeFn_eq_coeFn_toMeasure — Mathlib

English

Equality on sets between ν.toFiniteMeasure and ν holds for all s.

Русский

Равенство по всем множествам между ν.toFiniteMeasure и ν.

LaTeX

$$ ν.toFiniteMeasure(s) = ν(s) $$

Lean4

@[simp]
theorem ennreal_coeFn_eq_coeFn_toMeasure (ν : ProbabilityMeasure Ω) (s : Set Ω) : (ν s : ℝ≥0∞) = (ν : Measure Ω) s := by
  rw [← coeFn_comp_toFiniteMeasure_eq_coeFn, FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure,
    toMeasure_comp_toFiniteMeasure_eq_toMeasure]

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