measure_lt_top_of_isCompact_of_isMulLeftInvariant'

English

If (interior U).Nonempty and μ(U) ≠ ∞, then μ(K) < ∞ for every compact K.

Русский

Если interior(U) непусто и μ(U) не бесконечна, то μ(K) < ∞ для любого компактного K.

LaTeX

$$$\text{(interior }U) .\text{Nonempty} \Rightarrow μ(U) \neq ∞ \Rightarrow \forall K \ (\text{IsCompact}(K) \Rightarrow μ(K) < ∞)$$$

Lean4

/-- If a left-invariant measure gives finite mass to a set with nonempty interior, then
it gives finite mass to any compact set. -/
@[to_additive /-- If a left-invariant measure gives finite mass to a set with nonempty interior, then it gives
    finite mass to any compact set. -/
    ]
theorem measure_lt_top_of_isCompact_of_isMulLeftInvariant' {U : Set G} (hU : (interior U).Nonempty) (h : μ U ≠ ∞)
    {K : Set G} (hK : IsCompact K) : μ K < ∞ :=
  measure_lt_top_of_isCompact_of_isMulLeftInvariant (interior U) isOpen_interior hU
    ((measure_mono interior_subset).trans_lt (lt_top_iff_ne_top.2 h)).ne hK

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