null_iff_toMeasure_null — Mathlib

English

For ν and s, ν(s) = 0 iff (ν : Measure Ω) s = 0.

Русский

Для любых ν и s, ν(s) = 0 тогда и только тогда, когда (ν : Measure Ω) s = 0.

LaTeX

$$ν(s) = 0 \\Leftrightarrow (ν : Measure Ω) s = 0$$

Lean4

@[simp]
theorem null_iff_toMeasure_null (ν : ProbabilityMeasure Ω) (s : Set Ω) : ν s = 0 ↔ (ν : Measure Ω) s = 0 :=
  ⟨fun h ↦ by rw [← ennreal_coeFn_eq_coeFn_toMeasure, h, ENNReal.coe_zero], fun h ↦ congrArg ENNReal.toNNReal h⟩

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