English
For any K0, chaar(K0) belongs to HaarProduct(K0).
Русский
Для любых K0, chaar(K0) принадлежит HaarProduct(K0).
LaTeX
$$$\text{chaar}(K_0) \in \text{haarProduct}(K_0)$$$
Lean4
/-- This is the "limit" of `prehaar K₀ U K` as `U` becomes a smaller and smaller open
neighborhood of `(1 : G)`. More precisely, it is defined to be an arbitrary element
in the intersection of all the sets `clPrehaar K₀ V` in `haarProduct K₀`.
This is roughly equal to the Haar measure on compact sets,
but it can differ slightly. We do know that
`haarMeasure K₀ (interior K) ≤ chaar K₀ K ≤ haarMeasure K₀ K`. -/
@[to_additive addCHaar /-- additive version of `MeasureTheory.Measure.haar.chaar` -/
]
noncomputable def chaar (K₀ : PositiveCompacts G) (K : Compacts G) : ℝ :=
Classical.choose (nonempty_iInter_clPrehaar K₀) K
