English
If both s and t are well-ordered in the sense of IsPWO, then the smulAntidiagonal s t a is finite for any a.
Русский
Если s и t являются частями, удовлетворяющими IsPWO, тогда smulAntidiagonal s t a конечна для любого a.
LaTeX
$$$\text{(s.IsPWO)} \rightarrow (t.IsPWO) \rightarrow \forall a, (s.smulAntidiagonal t a).\Finite$$$
Lean4
@[to_additive VAddAntidiagonal.finite_of_isPWO]
theorem finite_of_isPWO (hs : s.IsPWO) (ht : t.IsPWO) (a) : (smulAntidiagonal s t a).Finite :=
by
refine Set.not_infinite.1 fun h => ?_
have h1 : (smulAntidiagonal s t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o (· ≤ ·)) := fun f ↦
hs fun n ↦ ⟨_, (mem_smulAntidiagonal.1 (f n).2).1⟩
have h2 : (smulAntidiagonal s t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o (· ≤ ·)) := fun f ↦
ht fun n ↦ ⟨_, (mem_smulAntidiagonal.1 (f n).2).2.1⟩
obtain ⟨g, hg⟩ := h1.exists_monotone_subseq fun n ↦ (h.natEmbedding _ n).2
obtain ⟨m, n, mn, h2'⟩ := h2 fun n ↦ h.natEmbedding _ _
refine mn.ne (g.injective <| (h.natEmbedding _).injective ?_)
exact eq_of_fst_le_fst_of_snd_le_snd (hg _ _ mn.le) h2'
