prod — Mathlib

English

Let s ⊆ α and t ⊆ β be subsets that are partially well-ordered under their respective orders. Then the Cartesian product s × t, ordered coordinatewise, is partially well-ordered.

Русский

Пусть s ⊆ α и t ⊆ β являются частично хорошо упорядоченными относительно соответствующих порядков. Тогда декартово произведение s × t, упорядоченное покоординатно, является частично хорошо упорядоченным.

LaTeX

$$$\\operatorname{IsPWO}(s) \\land \\operatorname{IsPWO}(t) \\Rightarrow \\operatorname{IsPWO}(s \\times t)$$$

Lean4

nonrec theorem prod {t : Set β} (hs : s.IsPWO) (ht : t.IsPWO) : IsPWO (s ×ˢ t) :=
  hs.prod ht

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