English
If s and t are partially well-ordered by r, then their union s ∪ t is also partially well-ordered by r.
Русский
Если s и t частично хорошо упорядочены по r, то их объединение s ∪ t тоже частично хорошо упорядочено по r.
LaTeX
$$$(s.PartiallyWellOrderedOn r) \\to (t.PartiallyWellOrderedOn r) \\to ((s \\cup t).PartiallyWellOrderedOn r)$$$
Lean4
theorem union (hs : s.PartiallyWellOrderedOn r) (ht : t.PartiallyWellOrderedOn r) : (s ∪ t).PartiallyWellOrderedOn r :=
by
intro f
obtain ⟨g, hgs | hgt⟩ := Nat.exists_subseq_of_forall_mem_union _ fun x ↦ (f x).2
· rcases hs.exists_lt hgs with ⟨m, n, hlt, hr⟩
exact ⟨g m, g n, g.strictMono hlt, hr⟩
· rcases ht.exists_lt hgt with ⟨m, n, hlt, hr⟩
exact ⟨g m, g n, g.strictMono hlt, hr⟩
