English
With an antitone f, the image of the set of minimal elements of s equals the set of maximal elements of the image set, under the right duality.
Русский
С антитоничным f образ минимальных элементов s равен множеству максимальных элементов образа при правильной двойственности.
LaTeX
$$$\\text{Image}(f, \\{x \\mid Minimal P x\\}) = \\{x \\mid Maximal (\\exists x_0, P x_0 ∧ f x_0 = x)\\}$$$
Lean4
theorem image_antitone_setOf_minimal (hf : ∀ ⦃x y⦄, P x → P y → (f x ≤ f y ↔ y ≤ x)) :
f '' {x | Minimal P x} = {x | Maximal (∃ x₀, P x₀ ∧ f x₀ = ·) x} :=
image_monotone_setOf_minimal (β := βᵒᵈ) (fun _ _ hx hy ↦ hf hy hx)