English
If s is PWOn by r and f respects the order (monotone with respect to r → r'), then the image f[s] is PWOn by r'.
Русский
Если s частично хорошо упорядочено по r, и f сохраняет порядок так, что r a1 a2 ⇒ r'(f(a1)) (f(a2)) для a1,a2 ∈ s, то образ f[s] является PWOn по r'.
LaTeX
$$$(f''s).PartiallyWellOrderedOn r' \\leftarrow (\\forall a_1 \\in s)(\\forall a_2 \\in s)(r\\ a_1\\ a_2 \\Rightarrow r' (f a_1)(f a_2)\\right)$$$
Lean4
theorem image_of_monotone_on (hs : s.PartiallyWellOrderedOn r) (hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)) :
(f '' s).PartiallyWellOrderedOn r' :=
by
rw [partiallyWellOrderedOn_iff_exists_lt] at *
intro g' hg'
choose g hgs heq using hg'
obtain rfl : f ∘ g = g' := funext heq
obtain ⟨m, n, hlt, hmn⟩ := hs g hgs
exact
⟨m, n, hlt, hf _ (hgs m) _ (hgs n) hmn⟩
-- TODO: prove this in terms of `IsAntichain.finite_of_wellQuasiOrdered`
