English
If s and t are monotone families of sets indexed by a semilattice, the iUnion of their Cartesian products equals the Cartesian product of their iUnions.
Русский
Если csal и t являются монотонными семействами множеств по полупринципу, то их iUnion произведений равен произведению их iUnions.
LaTeX
$$$\bigcup_{x} (s_x \times t_x) = (\bigcup_{x} s_x) \times (\bigcup_{x} t_x)$$$
Lean4
theorem iUnion_prod_of_monotone [SemilatticeSup α] {s : α → Set β} {t : α → Set γ} (hs : Monotone s) (ht : Monotone t) :
⋃ x, s x ×ˢ t x = (⋃ x, s x) ×ˢ ⋃ x, t x := by
ext ⟨z, w⟩; simp only [mem_prod, mem_iUnion, exists_imp, and_imp, iff_def]; constructor
· intro x hz hw
exact ⟨⟨x, hz⟩, x, hw⟩
· intro x hz x' hw
exact ⟨x ⊔ x', hs le_sup_left hz, ht le_sup_right hw⟩
