extend_iUnion_le_tsum_nat' — Mathlib

English

Reiterates that OuterMeasure α carries a canonical class structure consistent with the prior definition, ensuring the same properties hold.

Русский

Повторно устанавливается, что OuterMeasure α обладает канонической структурой класса, согласующейся с ранее заданной.\

LaTeX

$$$\\text{OuterMeasureClass}(\\mathrm{OuterMeasure}\\; \\alpha)\\; \\alpha$$$

Lean4

theorem extend_iUnion_le_tsum_nat' (s : ℕ → Set α) : extend m (⋃ i, s i) ≤ ∑' i, extend m (s i) :=
  by
  by_cases h : ∀ i, P (s i)
  · rw [extend_eq _ (PU h), congr_arg tsum _]
    · apply msU h
    funext i
    apply extend_eq _ (h i)
  · obtain ⟨i, hi⟩ := not_forall.1 h
    exact le_trans (le_iInf fun h => hi.elim h) (ENNReal.le_tsum i)

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