coeFn_comp_toFiniteMeasure_eq_coeFn

English

The set-valued coeFn of ν.toFiniteMeasure equals the set-valued coeFn of ν.

Русский

Коэрцированная функция множества ν.toFiniteMeasure равна коэрированной функции ν.

LaTeX

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

Lean4

@[simp]
theorem coeFn_comp_toFiniteMeasure_eq_coeFn (ν : ProbabilityMeasure Ω) :
    (ν.toFiniteMeasure : Set Ω → ℝ≥0) = (ν : Set Ω → ℝ≥0) :=
  rfl

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