coe_toWeakDualBCNN — Mathlib

English

For every finite measure μ and bounded nonnegative test function f, the evaluation agrees: (μ.toWeakDualBCNN) f = μ.testAgainstNN f.

Русский

Для каждой конечной меры μ и тест-функции f выполняется совпадение: (μ.toWeakDualBCNN) f = μ.testAgainstNN f.

LaTeX

$$$ \forall \mu : \text{FiniteMeasure } \Omega, \; \forall f : \Omega \to^{} \mathbb{R}_{\ge 0}, (\mu.toWeakDualBCNN) f = \mu.testAgainstNN f. $$$

Lean4

@[simp]
theorem coe_toWeakDualBCNN (μ : FiniteMeasure Ω) : ⇑μ.toWeakDualBCNN = μ.testAgainstNN :=
  rfl

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