English
If s is PWOn by r and t is PWOn by r', then the product set s × t (with the product relation) is PWOn by the corresponding product relation.
Русский
Если s PWOn по r и t PWOn по r', то произведение s × t (с соответствующим произведением отношений) PWOn.
LaTeX
$$$\\forall {t : Set\\beta}, (hs : PartiallyWellOrderedOn s r) (ht : PartiallyWellOrderedOn t r') : PartiallyWellOrderedOn (s \\timesˢ t) (fun x y : \\alpha × \\beta => r x.1 y.1 ∧ r' x.2 y.2)$$$
Lean4
protected theorem prod {t : Set β} (hs : PartiallyWellOrderedOn s r) (ht : PartiallyWellOrderedOn t r') :
PartiallyWellOrderedOn (s ×ˢ t) fun x y : α × β => r x.1 y.1 ∧ r' x.2 y.2 :=
by
rw [partiallyWellOrderedOn_iff_exists_lt]
intro f hf
obtain ⟨g₁, h₁⟩ := hs.exists_monotone_subseq fun n => (hf n).1
obtain ⟨m, n, hlt, hle⟩ := ht.exists_lt fun n => (hf _).2
exact ⟨g₁ m, g₁ n, g₁.strictMono hlt, h₁ _ _ hlt.le, hle⟩
