English
If f reverses the order on s (i.e., f x ≤ f y ↔ y ≤ x for x,y ∈ s), then the image of the set of maximal elements of s equals the set of minimal elements of f(s).
Русский
Если f обращает порядок на s (для x,y ∈ s выполняется f(x) ≤ f(y) ↔ y ≤ x), то образ максимальных элементов s совпадает с множеством минимальных элементов f''s.
LaTeX
$$$\\left( \\forall x,y \\in s,\\ f(x) \\le f(y) \\Leftrightarrow y \\le x \\right) \\Rightarrow f''\\{ x \\in α \\mid \\operatorname{Maximal}(\\cdot \\in s)\\ x \\} = \\{ x \\in β \\mid \\operatorname{Minimal}(\\cdot \\in f'' s)\\ x \\}$$$
Lean4
theorem image_antitone_setOf_maximal_mem (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ y ≤ x)) :
f '' {x | Maximal (· ∈ s) x} = {x | Minimal (· ∈ f '' s) x} :=
image_antitone_setOf_maximal hf
