sfinite_sum_of_countable — Mathlib

English

If ι is countable and m: ι → Measure α with each m(n) finite, then sum m is s-finite (proof via injective nat and extend).

Русский

Пусть ι счётно, и каждая m(n) конечна; тогда сумма m является s-finite (доказано через инъективное отображение и расширение).

LaTeX

$$SFinite (Measure.sum m)$$

Lean4

/-- A countable sum of finite measures is s-finite.
This lemma is superseded by the instance below. -/
theorem sfinite_sum_of_countable [Countable ι] (m : ι → Measure α) [∀ n, IsFiniteMeasure (m n)] :
    SFinite (Measure.sum m) := by
  classical
  obtain ⟨f, hf⟩ : ∃ f : ι → ℕ, Function.Injective f := Countable.exists_injective_nat ι
  refine ⟨_, fun n ↦ ?_, (sum_extend_zero hf m).symm⟩
  rcases em (n ∈ range f) with ⟨i, rfl⟩ | hn
  · rw [hf.extend_apply]
    infer_instance
  · rw [Function.extend_apply' _ _ _ hn, Pi.zero_apply]
    infer_instance

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