testAgainstNN_mono — Mathlib

English

If f ≤ g as bounded nonnegative functions, then μ.testAgainstNN f ≤ μ.testAgainstNN g.

Русский

Если f ≤ g как ограниченные неотрицательные функции, то μ.testAgainstNN f ≤ μ.testAgainstNN g.

LaTeX

$$$\text{If } f \le g:\ (f,g) \text{ bounded nonnegative},\ \mu.testAgainstNN f \le \mu.testAgainstNN g$$$

Lean4

theorem testAgainstNN_mono (μ : FiniteMeasure Ω) {f g : Ω →ᵇ ℝ≥0} (f_le_g : (f : Ω → ℝ≥0) ≤ g) :
    μ.testAgainstNN f ≤ μ.testAgainstNN g :=
  by
  simp only [← ENNReal.coe_le_coe, testAgainstNN_coe_eq]
  gcongr
  apply f_le_g

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