English
Under partial orders on α and β, if the projections of s onto α and β lie in PWOn, then s is PWOn under the ProdLex order.
Русский
При частичных порядках на α и β, если проекции s на α и β лежат в PWOn, тогда s является PWOn относительно порядка ProdLex.
LaTeX
$$∀ {α β}, [PartialOrder α] [Preorder β] {s : Set (Lex (Prod α β))}, (image fst s).IsPWO → (∀ a, {y | toLex (a, y) ∈ s}.IsPWO) → s.IsPWO$$
Lean4
theorem subsetProdLex [PartialOrder α] [Preorder β] {s : Set (α ×ₗ β)}
(hα : ((fun (x : α ×ₗ β) => (ofLex x).1) '' s).IsPWO) (hβ : ∀ a, {y | toLex (a, y) ∈ s}.IsPWO) : s.IsPWO :=
by
rw [IsPWO, partiallyWellOrderedOn_iff_exists_lt]
intro f hf
rw [isPWO_iff_exists_monotone_subseq] at hα
obtain ⟨g, hg⟩ : ∃ (g : (ℕ ↪o ℕ)), Monotone fun n => (ofLex f (g n)).1 :=
hα (fun n => (ofLex f n).1) (fun k => mem_image_of_mem (fun x => (ofLex x).1) (hf k))
have hhg : ∀ n, (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1 := fun n => hg n.zero_le
by_cases hc : ∃ n, (ofLex f (g 0)).1 < (ofLex f (g n)).1
· obtain ⟨n, hn⟩ := hc
use (g 0), (g n)
constructor
· by_contra hx
simp_all
· exact Prod.Lex.toLex_le_toLex.mpr <| .inl hn
· have hhc : ∀ n, (ofLex f (g 0)).1 = (ofLex f (g n)).1 :=
by
intro n
rw [not_exists] at hc
exact (hhg n).eq_of_not_lt (hc n)
obtain ⟨g', hg'⟩ : ∃ g' : ℕ ↪o ℕ, Monotone ((fun n ↦ (ofLex f (g (g' n))).2)) :=
by
simp_rw [isPWO_iff_exists_monotone_subseq] at hβ
apply hβ (ofLex f (g 0)).1 fun n ↦ (ofLex f (g n)).2
intro n
rw [hhc n]
simpa using hf _
use (g (g' 0)), (g (g' 1))
suffices (f (g (g' 0))) ≤ (f (g (g' 1))) by simpa
· refine Prod.Lex.toLex_le_toLex.mpr <| .inr ⟨?_, ?_⟩
· exact (hhc (g' 0)).symm.trans (hhc (g' 1))
· exact hg' (Nat.zero_le 1)
