haarContent_apply — Mathlib

English

Applied to any K0 and compact K, haarContent K0 K equals the NNReal value with components chaar(K0,K) and its nonnegativity.

Русский

Для любых K0 и компактного K значение haarContent K0 K равно NNReal-значению с компонентами chaar(K0,K) и неотрицательностью.

LaTeX

$$$\text{haarContent}_{K_0}(K) = \langle \operatorname{chaar}(K_0,K),\; \operatorname{chaar\_nonneg}(K_0,K)\rangle$$$

Lean4

@[to_additive]
theorem haarContent_apply (K₀ : PositiveCompacts G) (K : Compacts G) :
    haarContent K₀ K = show NNReal from ⟨chaar K₀ K, chaar_nonneg _ _⟩ :=
  rfl

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