measure_isOpen_pos_of_smulInvariant_of_compact_ne_zero

English

If μ ≠ 0 and U is open with U ≠ ∅, then μ(U) > 0 for a smul-invariant μ on a minimal action.

Русский

Если μ ≠ 0 и U открытое множество непусто, тогда μ(U) > 0 при минимальном действии группы.

LaTeX

$$$\\mu(U) > 0$ under the given conditions$$

Lean4

/-- If measure `μ` is invariant under a group action and is nonzero on a compact set `K`, then it is
positive on any nonempty open set. In case of a regular measure, one can assume `μ ≠ 0` instead of
`μ K ≠ 0`, see `MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_ne_zero`. -/
@[to_additive]
theorem measure_isOpen_pos_of_smulInvariant_of_compact_ne_zero (hK : IsCompact K) (hμK : μ K ≠ 0) (hU : IsOpen U)
    (hne : U.Nonempty) : 0 < μ U :=
  let ⟨t, ht⟩ := hK.exists_finite_cover_smul G hU hne
  pos_iff_ne_zero.2 fun hμU =>
    hμK <| measure_mono_null ht <| (measure_biUnion_null_iff t.countable_toSet).2 fun _ _ => by rwa [measure_smul]

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