Lean4
/-- Given a prepartition `π` of a box `I` and a collection of prepartitions `πi J` of all boxes
`J ∈ π`, returns the prepartition of `I` into the union of the boxes of all `πi J`.
Though we only use the values of `πi` on the boxes of `π`, we require `πi` to be a globally defined
function. -/
@[simps]
def biUnion (πi : ∀ J : Box ι, Prepartition J) : Prepartition I
where
boxes := π.boxes.biUnion fun J => (πi J).boxes
le_of_mem' J
hJ := by
simp only [Finset.mem_biUnion, mem_boxes] at hJ
rcases hJ with ⟨J', hJ', hJ⟩
exact ((πi J').le_of_mem hJ).trans (π.le_of_mem hJ')
pairwiseDisjoint := by
simp only [Set.Pairwise, Finset.mem_coe, Finset.mem_biUnion]
rintro J₁' ⟨J₁, hJ₁, hJ₁'⟩ J₂' ⟨J₂, hJ₂, hJ₂'⟩ Hne
rw [Function.onFun, Set.disjoint_left]
rintro x hx₁ hx₂; apply Hne
obtain rfl : J₁ = J₂ := π.eq_of_mem_of_mem hJ₁ hJ₂ ((πi J₁).le_of_mem hJ₁' hx₁) ((πi J₂).le_of_mem hJ₂' hx₂)
exact (πi J₁).eq_of_mem_of_mem hJ₁' hJ₂' hx₁ hx₂
