English
If U is open and nonempty, and μ(U) ≠ ∞, then μ(K) < ∞ for every compact K.
Русский
Пусть U открытое и неабсолютно непустое, μ(U) не бесконечна, тогда для любого компактного K верно μ(K) < ∞.
LaTeX
$$$\text{IsOpen}(U) \land U \neq \emptyset \land μ(U) \neq ∞ \Rightarrow \forall K\ (\text{IsCompact}(K) \Rightarrow μ(K) < ∞)$$$
Lean4
/-- If a left-invariant measure gives finite mass to a nonempty open set, then it gives finite mass
to any compact set. -/
@[to_additive /-- If a left-invariant measure gives finite mass to a nonempty open set, then it gives finite mass
to any compact set. -/
]
theorem measure_lt_top_of_isCompact_of_isMulLeftInvariant (U : Set G) (hU : IsOpen U) (h'U : U.Nonempty) (h : μ U ≠ ∞)
{K : Set G} (hK : IsCompact K) : μ K < ∞ :=
by
rw [← hU.interior_eq] at h'U
obtain ⟨t, hKt⟩ : ∃ t : Finset G, K ⊆ ⋃ g ∈ t, (fun h : G => g * h) ⁻¹' U :=
compact_covered_by_mul_left_translates hK h'U
exact (measure_mono hKt).trans_lt <| measure_biUnion_lt_top t.finite_toSet <| by simp [h.lt_top]
