English
The join of a bi-index supremum with another supremum distributes to a bi-supimum over the product index: ((⨆ i ∈ s, f i) ⊓ (⨆ j ∈ t, g j)) = ⨆ p ∈ s×t, f p.fst ⊓ g p.snd.
Русский
Объединение двух супремумов по би-индексам распределяется по произведению индексов: (⨆ i∈s, f(i)) ∧ (⨆ j∈t, g(j)) = ⨆ p∈s×t, f(p.1) ∧ g(p.2).
LaTeX
$$$\\bigl( \\bigvee_{i\\in s} f(i) \\bigr) \\wedge \\bigl( \\bigvee_{j\\in t} g(j) \\bigr) = \\bigvee_{p\\in s\\times t} \\bigl( f(p)_1 \\wedge g(p)_2 \\bigr)$$$
Lean4
theorem biSup_inf_biSup {ι ι' : Type*} {f : ι → α} {g : ι' → α} {s : Set ι} {t : Set ι'} :
((⨆ i ∈ s, f i) ⊓ ⨆ j ∈ t, g j) = ⨆ p ∈ s ×ˢ t, f (p : ι × ι').1 ⊓ g p.2 :=
by
simp only [iSup_subtype', iSup_inf_iSup]
exact (Equiv.surjective _).iSup_congr (Equiv.Set.prod s t).symm fun x => rfl
