isLocallyFiniteMeasure_of_smulInvariant

English

If there exists a nonempty open set U with finite μ-measure and μ is SMulInvariant, then μ is locally finite.

Русский

Если существует непустое открытое множество U с конечной мерой μ и μ инвариантна относительно действия, тогда μ локально конечна.

LaTeX

$$$\\text{IsLocallyFiniteMeasure }\\mu$$$

Lean4

@[to_additive]
theorem isLocallyFiniteMeasure_of_smulInvariant (hU : IsOpen U) (hne : U.Nonempty) (hμU : μ U ≠ ∞) :
    IsLocallyFiniteMeasure μ :=
  ⟨fun x =>
    let ⟨g, hg⟩ := hU.exists_smul_mem G x hne
    ⟨(g • ·) ⁻¹' U, (hU.preimage (continuous_id.const_smul _)).mem_nhds hg,
      Ne.lt_top <| by rwa [measure_preimage_smul]⟩⟩

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