English
A variant form stating the equivalence of maximality in the image and minimality in the domain for an antitone f.
Русский
Вариант формулировки эквивалентности для антитоничного отображения: максимальность образа ⇔ минимальность в области.
LaTeX
$$$(\\text{Maximal}(\\cdot \\in f''s)\\,(f(a))) \\iff (\\text{Minimal}(\\cdot \\in s)\\, a)$$$
Lean4
theorem image_monotone_setOf_minimal_mem (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) :
f '' {x | Minimal (· ∈ s) x} = {x | Minimal (· ∈ f '' s) x} :=
image_monotone_setOf_minimal hf