English
If I is finite and s_i(j) is monotone in i, then the union over j of the Pi-type of s_i(j) equals the Pi-type of unions: ⋃ j I.pi (s i j) = I.pi (⋃ j s i j).
Русский
Если I конечен, и s_i(j) монотонна по i, тогда объединение по j функционала Pi равно функционалу Pi от объединений.
LaTeX
$$$\text{finite}(I) \Rightarrow \bigcup_{j} \pi(I; s(i;j)) = \pi(I; \bigcup_{j} s(i;j)).$$$
Lean4
theorem iUnion_pi_of_monotone {ι ι' : Type*} [LinearOrder ι'] [Nonempty ι'] {α : ι → Type*} {I : Set ι}
{s : ∀ i, ι' → Set (α i)} (hI : I.Finite) (hs : ∀ i ∈ I, Monotone (s i)) :
⋃ j : ι', I.pi (fun i => s i j) = I.pi fun i => ⋃ j, s i j :=
by
simp only [pi_def, biInter_eq_iInter, preimage_iUnion]
haveI := hI.fintype.finite
refine iUnion_iInter_of_monotone (ι' := ι') (fun (i : I) j₁ j₂ h => ?_)
exact preimage_mono <| hs i i.2 h
