English
If suprema over rows and columns are pairwise disjoint and satisfy completeness, then the entire index set yields pairwise disjoint blocks.
Русский
Если надстроки и столбцы попарно непересекаются и удовлетворяют условиям полноты, то вся совокупность индексов образует попарно непересекающиеся блоки.
LaTeX
$$$$\text{If } hs : s.PAIRWISE_DISJOINT (\lambda i, ⨆ i' ∈ t, f(i,i')) \text{ and } ht : t.PAIRWISE_DISJOINT (\lambda i', ⨆ i ∈ s, f(i,i')), \\ (s \timesˢ t).PAIRWISE_DISJOINT f.$$$$
Lean4
/-- If the suprema of columns are pairwise disjoint and suprema of rows as well, then everything is
pairwise disjoint. Not to be confused with `Set.PairwiseDisjoint.prod`. -/
theorem prod_left {f : ι × ι' → α} (hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i'))
(ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')) : (s ×ˢ t : Set (ι × ι')).PairwiseDisjoint f :=
by
rintro ⟨i, i'⟩ hi ⟨j, j'⟩ hj h
rw [mem_prod] at hi hj
obtain rfl | hij := eq_or_ne i j
· refine (ht hi.2 hj.2 <| (Prod.mk_right_injective _).ne_iff.1 h).mono ?_ ?_
· convert le_iSup₂ (α := α) i hi.1; rfl
· convert le_iSup₂ (α := α) i hj.1; rfl
· refine (hs hi.1 hj.1 hij).mono ?_ ?_
· convert le_iSup₂ (α := α) i' hi.2; rfl
· convert le_iSup₂ (α := α) j' hj.2; rfl
