haarContent_outerMeasure_self_pos

English

The outer measure of Haar content on the base K0, evaluated at K0, is positive.

Русский

Внешняя мера содержания Хаара на базисе K0, примененная к K0, положительна.

LaTeX

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

Lean4

@[to_additive]
theorem haarContent_outerMeasure_self_pos (K₀ : PositiveCompacts G) : 0 < (haarContent K₀).outerMeasure K₀ :=
  by
  refine zero_lt_one.trans_le ?_
  rw [Content.outerMeasure_eq_iInf]
  refine le_iInf₂ fun U hU => le_iInf fun hK₀ => le_trans ?_ <| le_iSup₂ K₀.toCompacts hK₀
  exact haarContent_self.ge

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