measure_lt_top — Mathlib

English

A compact set has finite measure for a measure that is finite on compacts.

Русский

Компактное множество имеет конечную меру для меры, конечной на компактах.

LaTeX

$$$\text{IsFiniteMeasureOnCompacts}(\mu) \Rightarrow \forall K (\text{IsCompact } K \Rightarrow \mu(K) < \infty)$$$

Lean4

/-- A compact subset has finite measure for a measure which is finite on compacts. -/
theorem _root_.IsCompact.measure_lt_top [TopologicalSpace α] {μ : Measure α} [IsFiniteMeasureOnCompacts μ] ⦃K : Set α⦄
    (hK : IsCompact K) : μ K < ∞ :=
  IsFiniteMeasureOnCompacts.lt_top_of_isCompact hK

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