English
Let f be an order-embedding on a subset s of a preorder α into a preorder β. If f preserves and reflects order on s (i.e., for all x,y in s, f(x) ≤ f(y) iff x ≤ y), then the image under f of the set of maximal elements of s equals the set of maximal elements of f(s).
Русский
Пусть f – координатное вложение (по порядку) на подмножестве s ⊆ α в упорядоченное множество β. Если f сохраняет и отражает порядок на s (для всех x,y ∈ s выполняется f(x) ≤ f(y) ↔ x ≤ y), то образ множества максимальных элементов s совпадает с множеством максимальных элементов f''s.
LaTeX
$$$\\left( \\forall x,y \\in s,\\; f(x) \\le f(y) \\Leftrightarrow x \\le y \\right) \\Rightarrow f''\\{ x \\in α \\mid \\operatorname{Maximal}(\\cdot \\in s)\\ x \\} = \\{ x \\in β \\mid \\operatorname{Maximal}(\\cdot \\in f''s)\\ x \\}$$$
Lean4
theorem image_monotone_setOf_maximal_mem (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) :
f '' {x | Maximal (· ∈ s) x} = {x | Maximal (· ∈ f '' s) x} :=
image_monotone_setOf_maximal hf
