English
Let α be a distributive lattice. For finite s ⊆ ι, t ⊆ κ and f : ι → α, g : κ → α, we have\n\\[ s.sup' hs f ⊓ t.sup' ht g = (s ×ˢ t).sup' (hs.product ht) fun i => f i.1 ⊓ g i.2. \\]
Русский
Пусть α распределённая решётка. Тогда для конечных s ⊆ ι, t ⊆ κ и f,g: ι→α, κ→α выполняется\n\\[ s.sup' hs f ⊓ t.sup' ht g = (s ×ˢ t).sup' (hs.product ht) (λ i, f i.1 ⊓ g i.2). \\]
LaTeX
$$$$ s.sup' hs f \\wedge t.sup' ht g = (s \\times\\! t)^{\\sup'} (hs.product ht) (\\lambda i, f(i.1) \\wedge g(i.2)). $$$$
Lean4
theorem sup'_inf_sup' (f : ι → α) (g : κ → α) :
s.sup' hs f ⊓ t.sup' ht g = (s ×ˢ t).sup' (hs.product ht) fun i => f i.1 ⊓ g i.2 := by
simp_rw [Finset.sup'_inf_distrib_right, Finset.sup'_inf_distrib_left, sup'_product_left]
