English
If s is pairwise disjoint with respect to f and t is pairwise disjoint with respect to g, then the product family (f i.1 × g i.2) over s × t is pairwise disjoint.
Русский
Если пары f и g по соответствующим индексам попарно непересекаются, то семейство произведений f i.1 × g i.2 над s × t попарно непересекается.
LaTeX
$$$$\text{If } s.PAIRWISE_DISJOINT f \text{ and } t.PAIRWISE_DISJOINT g, \ (s \timesˢ t).PairwiseDisjoint (\lambda i, f i.1 \timesˢ g i.2).$$$$
Lean4
theorem prod {f : ι → Set α} {g : ι' → Set β} (hs : s.PairwiseDisjoint f) (ht : t.PairwiseDisjoint g) :
(s ×ˢ t : Set (ι × ι')).PairwiseDisjoint fun i => f i.1 ×ˢ g i.2 := fun ⟨_, _⟩ ⟨hi, hi'⟩ ⟨_, _⟩ ⟨hj, hj'⟩ hij =>
disjoint_left.2 fun ⟨_, _⟩ ⟨hai, hbi⟩ ⟨haj, hbj⟩ =>
hij <| Prod.ext (hs.elim_set hi hj _ hai haj) <| ht.elim_set hi' hj' _ hbi hbj
