English
For μ on the bottom measurable space, sigma-finite is equivalent to finite measure.
Русский
Для меры μ на нижнем пространство измеримости сигма-конечность эквивалентна конечной мере.
LaTeX
$$theorem sigmaFinite_bot_iff (μ : @Measure α ⊥) : SigmaFinite μ ↔ IsFiniteMeasure μ$$
Lean4
theorem sigmaFinite_bot_iff (μ : @Measure α ⊥) : SigmaFinite μ ↔ IsFiniteMeasure μ :=
by
refine ⟨fun h => ⟨?_⟩, fun h => by infer_instance⟩
haveI : SigmaFinite μ := h
let s := spanningSets μ
have hs_univ : ⋃ i, s i = Set.univ := iUnion_spanningSets μ
have hs_meas : ∀ i, MeasurableSet[⊥] (s i) := measurableSet_spanningSets μ
simp_rw [MeasurableSpace.measurableSet_bot_iff] at hs_meas
by_cases h_univ_empty : (Set.univ : Set α) = ∅
· rw [h_univ_empty, measure_empty]
exact ENNReal.zero_ne_top.lt_top
obtain ⟨i, hsi⟩ : ∃ i, s i = Set.univ := by
by_contra! h_not_univ
have h_empty : ∀ i, s i = ∅ := by simpa [h_not_univ] using hs_meas
simp only [h_empty, iUnion_empty] at hs_univ
exact h_univ_empty hs_univ.symm
rw [← hsi]
exact measure_spanningSets_lt_top μ i
