English
Let S and T be subsets of a partially ordered commutative monoid such that both are well-founded with respect to the order. Then the product set S·T = {st : s ∈ S, t ∈ T} is again well-founded.
Русский
Пусть S и T — подмножества частично упорядоченной коммутативной моноидной структуры, и оба множества хорошо упорядованы относительно данного порядка. Тогда произведение S·T = {st | s∈S, t∈T} также хорошо упорядовано.
LaTeX
$$$\big(\text{IsPWO}(S) \land \text{IsPWO}(T)\big) \Rightarrow \text{IsPWO}(S T)$$$
Lean4
@[to_additive]
theorem mul [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] (hs : s.IsPWO) (ht : t.IsPWO) : IsPWO (s * t) :=
by
rw [← image_mul_prod]
exact (hs.prod ht).image_of_monotone (monotone_fst.mul' monotone_snd)
