English
For a finite union of the form ⋃_{i≤n} s_i, the content is bounded by the finite sum of contents: projectiveFamilyContent hP (⋃ i ≤ n, s_i) ≤ ∑_{i=0}^n projectiveFamilyContent hP (s_i).
Русский
Для конечного объединения ⋃_{i≤n} s_i справедливо ограничение содержания: projectiveFamilyContent hP (⋃ i ≤ n, s_i) ≤ ∑_{i=0}^n projectiveFamilyContent hP (s_i).
LaTeX
$$$\operatorname{projectiveFamilyContent} hP (\bigcup_{i=0}^{n} s_i) \le \sum_{i=0}^{n} \operatorname{projectiveFamilyContent} hP (s_i)$$$
Lean4
theorem projectiveFamilyContent_iUnion_le (hP : IsProjectiveMeasureFamily P) {s : ℕ → Set (Π i : ι, α i)}
(hs : ∀ n, s n ∈ measurableCylinders α) (n : ℕ) :
projectiveFamilyContent hP (⋃ i ≤ n, s i) ≤ ∑ i ∈ range (n + 1), projectiveFamilyContent hP (s i) :=
calc
projectiveFamilyContent hP (⋃ i ≤ n, s i)
_ = projectiveFamilyContent hP (⋃ i ∈ range (n + 1), s i) := by simp only [mem_range_succ_iff]
_ ≤ ∑ i ∈ range (n + 1), projectiveFamilyContent hP (s i) :=
addContent_biUnion_le isSetRing_measurableCylinders (fun i _ ↦ hs i)
