null_iff_toMeasure_null — Mathlib

English

For a FiniteMeasure ν and a set s, ν s = 0 iff (ν.toMeasure) s = 0; a simp lemma.

Русский

Для конечной меры ν и множества s: ν(s) = 0 тогда и только тогда, когда ν.toMeasure(s) = 0; лемма для упрощения.

LaTeX

$$@[simp] theorem null_iff_toMeasure_null (ν : FiniteMeasure Ω) (s : Set Ω) : ν s = 0 ↔ (ν : Measure Ω) s = 0$$

Lean4

@[simp]
theorem null_iff_toMeasure_null (ν : FiniteMeasure Ω) (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⟩

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