English
Under suitable monotonicity conditions, maximality is preserved under image and conversely.
Русский
При равнозначных монотонных условиях максимальность сохраняется под отображением образа и обратно эквивалентна.
LaTeX
$$$(\\forall x,\\; x\\in s \\Rightarrow \\text{...})\\;\\Longleftrightarrow\\; (\\text{Maximal}(\\cdot \\in f''s)\\,(f(a)) \\Leftrightarrow \\text{Maximal}(\\cdot \\in s)\\, a).$$$
Lean4
theorem minimal_mem_image_monotone_iff (ha : a ∈ s) (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) :
Minimal (· ∈ f '' s) (f a) ↔ Minimal (· ∈ s) a :=
by
refine ⟨fun h ↦ ⟨ha, fun y hys ↦ ?_⟩, minimal_mem_image_monotone hf⟩
rw [← hf ha hys, ← hf hys ha]
exact h.le_of_le (mem_image_of_mem f hys)
