English
Let s and t be subsets of a suitable ordered group that form a complete lattice under multiplication; the supremum of the pointwise product set s * t equals the product of the supremums: sSup(s * t) = sSup(s) * sSup(t).
Русский
Пусть s и t — подмножества подходящей упорядоченной группы, образующие полную решётку под умножением; супремум произведения равен произведению супремумов: sSup(s t) = sSup(s) sSup(t).
LaTeX
$$$$ \\operatorname{sSup}(s \\cdot t) = \\operatorname{sSup}(s) \\cdot \\operatorname{sSup}(t). $$$$
Lean4
@[to_additive]
theorem sSup_mul : sSup (s * t) = sSup s * sSup t :=
(sSup_image2_eq_sSup_sSup fun _ => (OrderIso.mulRight _).to_galoisConnection) fun _ =>
(OrderIso.mulLeft _).to_galoisConnection
