outerMeasure_pos_of_is_mul_left_invariant

English

Under left-invariance hypotheses and a nonzero measure on a compact K, every nonempty open U has positive outer measure.

Русский

При условии инвариантности слева и ненулевой меры на компактном K любая непустая открытая U имеет положительную внешнюю меру.

LaTeX

$$$$0 < μ.outerMeasure(U)$$$$

Lean4

@[to_additive]
theorem outerMeasure_pos_of_is_mul_left_invariant [Group G] [IsTopologicalGroup G]
    (h3 : ∀ (g : G) {K : Compacts G}, μ (K.map _ <| continuous_mul_left g) = μ K) (K : Compacts G) (hK : μ K ≠ 0)
    {U : Set G} (h1U : IsOpen U) (h2U : U.Nonempty) : 0 < μ.outerMeasure U :=
  by
  convert μ.innerContent_pos_of_is_mul_left_invariant h3 K hK ⟨U, h1U⟩ h2U
  exact μ.outerMeasure_opens ⟨U, h1U⟩

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