English
If f is monotone on s in the sense that x,y ∈ s implies f(x) ≤ f(y) iff x ≤ y, then the image of the minimal element in s is the minimal element of the image set.
Русский
Пусть отображение f монотонно на s, то есть x,y ∈ s => f(x) ≤ f(y) ⇔ x ≤ y; тогда образ минимального элемента в s есть минимальный элемент образа.
LaTeX
$$$\\forall s,\\; (\\forall x,y \\in s,\\; f(x) \\le f(y) \\iff x \\le y) \\Rightarrow (Minimal(\\cdot \\in s)\\; x) \\Rightarrow Minimal(\\cdot \\in f''s)\\; (f(x)).$$$
Lean4
theorem minimal_mem_image_monotone (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) (hx : Minimal (· ∈ s) x) :
Minimal (· ∈ f '' s) (f x) := by
refine ⟨mem_image_of_mem f hx.prop, ?_⟩
rintro _ ⟨y, hy, rfl⟩
rw [hf hx.prop hy, hf hy hx.prop]
exact hx.le_of_le hy
