continuous_testAgainstNN_eval — Mathlib

English

For any f, the map μ ↦ μ.toFiniteMeasure.testAgainstNN f is continuous.

Русский

Для любого f отображение μ ↦ μ.toFiniteMeasure.testAgainstNN f непрерывно.

LaTeX

$$$\\text{continuous_testAgainstNN_eval}(f)$$$

Lean4

theorem continuous_testAgainstNN_eval (f : Ω →ᵇ ℝ≥0) :
    Continuous fun μ : ProbabilityMeasure Ω ↦ μ.toFiniteMeasure.testAgainstNN f :=
  (FiniteMeasure.continuous_testAgainstNN_eval f).comp toFiniteMeasure_continuous

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