English
Summing over the boxes of the construction equals summing over the original boxes with Option.elim' 0.
Русский
Суммирование по коробкам конструирования равно суммированию по исходным коробкам с использованием Option.elim' 0.
LaTeX
$$$ \\sum_{J \\in (ofWithBot boxes \\; le\_of\_mem \\; pairwise\\_disjoint).boxes} f(J) = \\sum_{J \\in boxes} \\mathrm{Option.elim' } 0\\, f(J) $$$
Lean4
@[simp]
theorem iUnion_ofWithBot (boxes : Finset (WithBot (Box ι))) (le_of_mem : ∀ J ∈ boxes, (J : WithBot (Box ι)) ≤ I)
(pairwise_disjoint : Set.Pairwise (boxes : Set (WithBot (Box ι))) Disjoint) :
(ofWithBot boxes le_of_mem pairwise_disjoint).iUnion = ⋃ J ∈ boxes, ↑J :=
by
suffices ⋃ (J : Box ι) (_ : ↑J ∈ boxes), ↑J = ⋃ J ∈ boxes, (J : Set (ι → ℝ)) by simpa [ofWithBot, Prepartition.iUnion]
simp only [← Box.biUnion_coe_eq_coe, @iUnion_comm _ _ (Box ι), @iUnion_comm _ _ (@Eq _ _ _), iUnion_iUnion_eq_right]
