haarContent_self — Mathlib

English

For any positiveCompact K0, haarContent K0 evaluated on K0.toCompacts equals the unit 1.

Русский

Для любого K0 из положительных компактных множество K0.toCompacts отображает в единицу.

LaTeX

$$$\text{haarContent}_{K_0}(K_0^{\text{toCompacts}})=1$$$

Lean4

/-- The variant of `chaar_self` for `haarContent` -/
@[to_additive /-- The variant of `addCHaar_self` for `addHaarContent`. -/
    ]
theorem haarContent_self {K₀ : PositiveCompacts G} : haarContent K₀ K₀.toCompacts = 1 := by
  simp_rw [← ENNReal.coe_one, haarContent_apply, ENNReal.coe_inj, chaar_self]; rfl

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