English
If s and t are IsPWO, then for any a, the set mulAntidiagonal s t a is finite.
Русский
Если s и t являются IsPWO, то для любого a множество mulAntidiagonal s t a конечное.
LaTeX
$$If s.IsPWO and t.IsPWO, then (mulAntidiagonal s t a).Finite.$$
Lean4
@[to_additive Set.AddAntidiagonal.finite_of_isPWO]
theorem finite_of_isPWO (hs : s.IsPWO) (ht : t.IsPWO) (a) : (mulAntidiagonal s t a).Finite :=
by
refine not_infinite.1 fun h => ?_
have h1 : (mulAntidiagonal s t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o (· ≤ ·)) := fun f ↦
hs fun n ↦ ⟨_, (mem_mulAntidiagonal.1 (f n).2).1⟩
have h2 : (mulAntidiagonal s t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o (· ≤ ·)) := fun f ↦
ht fun n ↦ ⟨_, (mem_mulAntidiagonal.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'
