English
If f is pairwise disjoint on its arguments, then the family of unions over decode₂ β i, i ↦ ⋃ b ∈ decode₂ β i, f b is pairwise disjoint.
Русский
Если множества f(b) для разных b попарно DISJOINT, то коллекции ⋃_{b ∈ decode₂ β i} f(b) по i попарно несоприкасаются.
LaTeX
$$$ \\text{Pairwise}(\\operatorname{Disjoint}\\ on\\ f) \\Rightarrow \\text{Pairwise}(\\operatorname{Disjoint}\\ on\\ (\\lambda i. \\bigcup_{b \\in decode_2(\\beta,i)} f(b))). $$$
Lean4
theorem iUnion_decode₂_disjoint_on {f : β → Set α} (hd : Pairwise (Disjoint on f)) :
Pairwise (Disjoint on fun i => ⋃ b ∈ decode₂ β i, f b) :=
by
rintro i j ij
refine disjoint_left.mpr fun x => ?_
suffices ∀ a, encode a = i → x ∈ f a → ∀ b, encode b = j → x ∉ f b by simpa [decode₂_eq_some]
rintro a rfl ha b rfl hb
exact (hd (mt (congr_arg encode) ij)).le_bot ⟨ha, hb⟩
