English
Under monotone conditions, the image of the set of minimal elements is characterized by a corresponding expression on the image.
Русский
При монотонных условиях образ множества минимальных элементов задаётся соответствующим образом в образе.
LaTeX
$$$\\text{Image}(f, \\{x \\mid Minimal P x\\}) = \\{x \\mid Minimal (\\exists x_0, P x_0 \\land f x_0 = x)\\}$$$
Lean4
theorem image_monotone_setOf_minimal (hf : ∀ ⦃x y⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)) :
f '' {x | Minimal P x} = {x | Minimal (∃ x₀, P x₀ ∧ f x₀ = ·) x} :=
by
refine Set.ext fun x ↦ ⟨?_, fun h ↦ ?_⟩
· rintro ⟨x, (hx : Minimal _ x), rfl⟩
exact (minimal_mem_image_monotone_iff hx.prop hf).2 hx
obtain ⟨y, hy, rfl⟩ := (mem_setOf_eq ▸ h).prop
exact mem_image_of_mem _ <| (minimal_mem_image_monotone_iff (s := setOf P) hy hf).1 h
