mul — Mathlib

English

If S and T are well-founded subsets of a partially ordered commutative monoid, then the product set S·T is also well-founded under the induced order.

Русский

Если S и T — хорошо упорядоченные подмножества частично упорядоченного коммутативного мономиода, то произведение S·T также хорошо упорядовано под линейно-индуцированным порядком.

LaTeX

$$(IsWF(S) ∧ IsWF(T)) → IsWF(S T)$$

Lean4

@[to_additive]
theorem mul (hs : s.IsWF) (ht : t.IsWF) : IsWF (s * t) :=
  (hs.isPWO.mul ht.isPWO).isWF

Похожие утверждения