haar — Mathlib

English

The outer measure of haarContent on closure is positive.

Русский

Внешняя мера haarContent на замыкании положительна.

LaTeX

$$(haarContent K0).outerMeasure(closure(K0))>0$$

Lean4

/-- `haar` is some choice of a Haar measure, on a locally compact group. -/
@[to_additive /-- `addHaar` is some choice of a Haar measure, on a locally compact additive group. -/
    ]
noncomputable abbrev haar [LocallyCompactSpace G] : Measure G :=
  haarMeasure <| Classical.arbitrary _

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