continuous_mass — Mathlib

English

The mass map μ ↦ μ.mass is continuous.

Русский

Масса меры является непрерывной функцией от μ.

LaTeX

$$$ \text{Continuous}(\lambda \mu : \text{FiniteMeasure } \Omega, \; \mu.mass). $$$

Lean4

/-- The total mass of a finite measure depends continuously on the measure. -/
theorem continuous_mass : Continuous fun μ : FiniteMeasure Ω ↦ μ.mass := by simp_rw [← testAgainstNN_one];
  exact continuous_testAgainstNN_eval 1

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