haarScalarFactor_pos_of_isHaarMeasure

English

A Haar measure paired with itself gives scalar 1: Haar μ μ = 1.

Русский

Мера Хаара в паре с самой собой даёт коэффициент 1: Haar μ μ = 1.

LaTeX

$$$$\\mathrm{haarScalarFactor} (μ, μ) = 1.$$$$

Lean4

/-- The scalar factor between two left-invariant measures is non-zero when both measures are
positive on open sets. -/
@[to_additive]
theorem haarScalarFactor_pos_of_isHaarMeasure (μ' μ : Measure G) [IsHaarMeasure μ] [IsHaarMeasure μ'] :
    0 < haarScalarFactor μ' μ :=
  pos_iff_ne_zero.2 (fun H ↦ by simpa [H] using haarScalarFactor_eq_mul μ' μ μ')

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