English
Let f be an order-reversing (on s) mapping from α to β in a preorder setting, i.e., f x ≤ f y iff y ≤ x for x,y ∈ s. Then the image of the set of minimal elements of s equals the set of maximal 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{Minimal}(\\cdot \\in s)\\ x \\} = \\{ x \\in β \\mid \\operatorname{Maximal}(\\cdot \\in f'' s)\\ x \\}$$$
Lean4
theorem image_antitone_setOf_minimal_mem (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ y ≤ x)) :
f '' {x | Minimal (· ∈ s) x} = {x | Maximal (· ∈ f '' s) x} :=
image_antitone_setOf_minimal hf
