haarContent_outerMeasure_closure_pos

English

The outer measure of Haar content on the closure of K0 is positive.

Русский

Положительна внешняя мера содержания Хаара на замыкании K0.

LaTeX

$$$(\\text{haarContent}_{K_0}).\\text{outerMeasure}(\\overline{K_0})>0$$$

Lean4

@[to_additive]
theorem haarContent_outerMeasure_closure_pos (K₀ : PositiveCompacts G) :
    0 < (haarContent K₀).outerMeasure (closure K₀) :=
  (haarContent_outerMeasure_self_pos K₀).trans_le (OuterMeasure.mono _ subset_closure)

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