zero_testAgainstNN — Mathlib

English

The zero finite measure yields zero when tested against any bounded nonnegative function.

Русский

Нулевая конечная мера даёт ноль при тестировании против любой ограниченной неотрицательной функции.

LaTeX

$$$ (0 : FiniteMeasure Ω).testAgainstNN = 0 $$$

Lean4

theorem zero_testAgainstNN : (0 : FiniteMeasure Ω).testAgainstNN = 0 :=
  by
  funext
  simp only [zero_testAgainstNN_apply, Pi.zero_apply]

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