toFun_eq_toNNReal_apply — Mathlib

English

For any topological space G and any Content μ on G, and for every compact K, the value of μ on K via the inner function equals the NNReal part of μ(K); i.e., μ.toFun(K) = (μ(K)).toNNReal.

Русский

Для любой топологической группы G и содержания μ на G, для каждого компактного множества K выполняется равенство μ.toFun(K) = (μ(K)).toNNReal.

LaTeX

$$$\forall K \in \mathrm{Compacts}(G): \mu^{\mathrm{toFun}}(K) = (\mu(K))^{\mathrm{toNNReal}}$$$

Lean4

@[simp]
theorem toFun_eq_toNNReal_apply (K : Compacts G) : μ.toFun K = (μ K).toNNReal :=
  rfl

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