English
If a measure is finite on compact sets in a proper metric space, then every bounded subset has finite measure.
Русский
Если мера конечна на компактных множествах в корректном метрическом пространстве, то любое ограниченное множество имеет конечную меру.
LaTeX
$$$\text{If } s \subseteq X \text{ is bounded, then } \mu(s) < \infty,$ where $\mu$ is a measure finite on compact sets on a proper pseudo-metric space $X$.$$
Lean4
/-- A bounded subset has finite measure for a measure which is finite on compact sets, in a
proper space. -/
theorem _root_.Bornology.IsBounded.measure_lt_top [PseudoMetricSpace α] [ProperSpace α] {μ : Measure α}
[IsFiniteMeasureOnCompacts μ] ⦃s : Set α⦄ (hs : Bornology.IsBounded s) : μ s < ∞ :=
calc
μ s ≤ μ (closure s) := measure_mono subset_closure
_ < ∞ := (Metric.isCompact_of_isClosed_isBounded isClosed_closure hs.closure).measure_lt_top
