English
Left invariance of haarContent under group action by g on K remains the same after mapping.
Русский
Лева invariанжированная haarContent сохраняется при действии группы по g на K.
LaTeX
$$haarContent K0 (K.map (continuous_mul_left g)) = haarContent K0 K$$
Lean4
/-- The Haar measure is a Haar measure, i.e., it is invariant and gives finite mass to compact
sets and positive mass to nonempty open sets. -/
@[to_additive /-- The additive Haar measure is an additive Haar measure, i.e., it is invariant and gives finite
mass to compact sets and positive mass to nonempty open sets. -/
]
instance isHaarMeasure_haarMeasure (K₀ : PositiveCompacts G) : IsHaarMeasure (haarMeasure K₀) :=
by
apply isHaarMeasure_of_isCompact_nonempty_interior (haarMeasure K₀) K₀ K₀.isCompact K₀.interior_nonempty
· simp only [haarMeasure_self]; exact one_ne_zero
· simp only [haarMeasure_self, ne_eq, ENNReal.one_ne_top, not_false_eq_true]
