measure_ne_top — Mathlib

English

A compact set has finite measure for IsFiniteMeasureOnCompacts μ, i.e., μ(K) ≠ ∞.

Русский

Компактное множество имеет конечную меру (μ(K) ≠ ∞).

LaTeX

$$$\text{IsCompact } K \Rightarrow μ(K) \neq ∞$$$

Lean4

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

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