product — Mathlib

English

If s and t are finite sets and f: ι × ι' → α, and the product-related SupIndep conditions hold for s and t, then their product s × t is SupIndep with respect to f.

Русский

Пусть s и t — конечные множества; если условия SupIndep, относящиеся к произведению, выполняются, то произведение s × t сохраняет SupIndep относительно f.

LaTeX

$$$(s \\times^\\, t).SupIndep f$ given $(hs : s.SupIndep (\\lambda i, t.sup (\\lambda i', f (i,i'))) )$ and $(ht : t.SupIndep (\\lambda i', s.sup (\\lambda i, f (i,i'))))$$$

Lean4

protected theorem product {s : Finset ι} {t : Finset ι'} {f : ι × ι' → α}
    (hs : s.SupIndep fun i => t.sup fun i' => f (i, i')) (ht : t.SupIndep fun i' => s.sup fun i => f (i, i')) :
    (s ×ˢ t).SupIndep f := by
  rintro u hu ⟨i, i'⟩ hi hiu
  rw [Finset.disjoint_sup_right]
  rintro ⟨j, j'⟩ hj
  have hij := (ne_of_mem_of_not_mem hj hiu).symm
  replace hj := hu hj
  rw [mem_product] at hi hj
  obtain rfl | hij := eq_or_ne i j
  · refine (ht.pairwiseDisjoint hi.2 hj.2 <| (Prod.mk_right_injective _).ne_iff.1 hij).mono ?_ ?_
    · convert le_sup (α := α) hi.1; simp
    · convert le_sup (α := α) hj.1; simp
  · refine (hs.pairwiseDisjoint hi.1 hj.1 hij).mono ?_ ?_
    · convert le_sup (α := α) hi.2; simp
    · convert le_sup (α := α) hj.2; simp

Похожие утверждения