English
The product of maximal elements yields the maximal product: prod p q ⊔ prod p' q' = prod (p ⊔ p') (q ⊔ q').
Русский
Произведение максимальных элементов даёт максимальное произведение: p×q ⊔ p'×q' = (p⊔p')×(q⊔q').
LaTeX
$$$$ prod\\ p\\ q \\sqcup prod\\ p'\\ q' = prod\\ (p \\sqcup p')\\ (q \\sqcup q') $$$$
Lean4
@[simp]
theorem prod_sup_prod : prod p q₁ ⊔ prod p' q₁' = prod (p ⊔ p') (q₁ ⊔ q₁') :=
by
refine le_antisymm (sup_le (prod_mono le_sup_left le_sup_left) (prod_mono le_sup_right le_sup_right)) ?_
simp only [SetLike.le_def, mem_prod, and_imp, Prod.forall]; intro xx yy hxx hyy
rcases mem_sup.1 hxx with ⟨x, hx, x', hx', rfl⟩
rcases mem_sup.1 hyy with ⟨y, hy, y', hy', rfl⟩
exact mem_sup.2 ⟨(x, y), ⟨hx, hy⟩, (x', y'), ⟨hx', hy'⟩, rfl⟩
