sigmaFinite_trim_bot_iff — Mathlib

English

The trimmed measure μ.trim bot is sigma-finite if and only if μ is finite.

Русский

Урезанная мера μ.trim bot является сигма-конечной тогда и только тогда, когда μ конечна.

LaTeX

$$$\\Sigma$-finite$(\\mu trim bot)$ ↔ IsFiniteMeasure$(\\mu)$$$

Lean4

theorem sigmaFinite_trim_bot_iff : SigmaFinite (μ.trim bot_le) ↔ IsFiniteMeasure μ :=
  by
  rw [sigmaFinite_bot_iff]
  refine ⟨fun h => ⟨?_⟩, fun h => ⟨?_⟩⟩ <;> have h_univ := h.measure_univ_lt_top
  · rwa [trim_measurableSet_eq bot_le MeasurableSet.univ] at h_univ
  · rwa [trim_measurableSet_eq bot_le MeasurableSet.univ]

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