English
The SupIndep status of s.product t with respect to f is equivalent to the conjunction of SupIndep conditions on the two marginal families.
Русский
Статус SupIndep для s.product t относительно f эквивалентен сочетанию условий SupIndep по двум краям.
LaTeX
$$$(s.product t).SupIndep f \\iff (s.SupIndep (\\lambda i, t.sup (\\lambda i' => f (i,i')))) \\land (t.SupIndep (\\lambda i' => s.sup (\\lambda i => f (i,i'))))$$$
Lean4
theorem supIndep_product_iff {s : Finset ι} {t : Finset ι'} {f : ι × ι' → α} :
(s.product t).SupIndep f ↔
(s.SupIndep fun i => t.sup fun i' => f (i, i')) ∧ t.SupIndep fun i' => s.sup fun i => f (i, i') :=
by
refine ⟨?_, fun h => h.1.product h.2⟩
simp_rw [supIndep_iff_pairwiseDisjoint]
refine fun h => ⟨fun i hi j hj hij => ?_, fun i hi j hj hij => ?_⟩ <;>
simp_rw [Finset.disjoint_sup_left, Finset.disjoint_sup_right] <;>
intro i' hi' j' hj'
· exact h (mk_mem_product hi hi') (mk_mem_product hj hj') (ne_of_apply_ne Prod.fst hij)
· exact h (mk_mem_product hi' hi) (mk_mem_product hj' hj) (ne_of_apply_ne Prod.snd hij)
