English
If r on α and s on β are well-quasi-ordered, then the product relation on α × β, defined by (a,b) ≤ (a',b') iff r a.a' and s b.b', is a well-quasi-order.
Русский
Если на α отношение r образует хорошо-квазиупорядоченность, а на β — отношение s, то произведение α×β с попарным порядком является хорошо-квазиупорядоченным.
LaTeX
$$$\\mathrm{IsPreorder}(α, r) \\Rightarrow (\\mathrm{WellQuasiOrdered}(r) \\wedge \\mathrm{WellQuasiOrdered}(s) \\Rightarrow \\mathrm{WellQuasiOrdered}(\\lambda a b:=(r\\ a.1 b.1 \\wedge s\\ a.2 b.2)))$$$
Lean4
theorem prod [IsPreorder α r] (hr : WellQuasiOrdered r) (hs : WellQuasiOrdered s) :
WellQuasiOrdered fun a b : α × β ↦ r a.1 b.1 ∧ s a.2 b.2 :=
by
intro f
obtain ⟨g, h₁⟩ := hr.exists_monotone_subseq (Prod.fst ∘ f)
obtain ⟨m, n, h, hf⟩ := hs (Prod.snd ∘ f ∘ g)
exact ⟨g m, g n, g.strictMono h, h₁ _ _ h.le, hf⟩
