English
BiUnion is associative: combining πi and πi' in either order yields the same result as regrouping the BiUnions.
Русский
BiUnion обладает ассоциативностью: объединение πi и πi' в любом порядке эквивалентно переклассификации BiUnion.
LaTeX
$$$ \\left( π.biUnion f \\,\\right) \\!\\biUnion (πi' \\,+) = π.biUnion πi \\!\\biUnion (πi' ) \\\\ [text]$$
Lean4
theorem biUnion_assoc (πi : ∀ J, Prepartition J) (πi' : Box ι → ∀ J : Box ι, Prepartition J) :
(π.biUnion fun J => (πi J).biUnion (πi' J)) = (π.biUnion πi).biUnion fun J => πi' (π.biUnionIndex πi J) J :=
by
ext J
simp only [mem_biUnion]
constructor
· rintro ⟨J₁, hJ₁, J₂, hJ₂, hJ⟩
refine ⟨J₂, ⟨J₁, hJ₁, hJ₂⟩, ?_⟩
rwa [π.biUnionIndex_of_mem hJ₁ hJ₂]
· rintro ⟨J₁, ⟨J₂, hJ₂, hJ₁⟩, hJ⟩
refine ⟨J₂, hJ₂, J₁, hJ₁, ?_⟩
rwa [π.biUnionIndex_of_mem hJ₂ hJ₁] at hJ
