English
Let f be an order-embedding from α to β and x be minimal in s. Then f(x) is minimal in f''s.
Русский
Пусть f — вложение порядка из α в β, и x минимален в s. Тогда f(x) минимален в f''s.
LaTeX
$$$\\forall f:\\, \\alpha \\hookrightarrow\\beta,\; (\\text{Minimal}(\\cdot \\in s) x) \\Rightarrow (\\text{Minimal}(\\cdot \\in f'' s) f(x))$$$
Lean4
theorem minimal_mem_image (f : α ↪o β) (hx : Minimal (· ∈ s) x) : Minimal (· ∈ f '' s) (f x) :=
_root_.minimal_mem_image_monotone (by simp [f.le_iff_le]) hx