coeFn_toFiniteMeasure — Mathlib

English

The evaluation of the finite-measure form equals the original evaluation: (ν.toFiniteMeasure : Set Ω → ℝ≥0) = (ν : Set Ω → ℝ≥0).

Русский

Оценка конечной меры равна исходной: (ν.toFiniteMeasure : Set Ω → ℝ≥0) = (ν : Set Ω → ℝ≥0).

LaTeX

$$(ν.toFiniteMeasure : Set Ω → ℝ≥0) = (ν : Set Ω → ℝ≥0)$$

Lean4

@[simp]
theorem coeFn_toFiniteMeasure (μ : ProbabilityMeasure Ω) : ⇑μ.toFiniteMeasure = μ :=
  rfl

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