image_monotone_setOf_maximal — Mathlib

English

Similarly for maximal elements under a monotone mapping, the image of maximal elements coincides with maximal elements of the image under dual order.

Русский

Аналогично для максимальных элементов при монотонном отображении: образ максимальных элементов совпадает с максимальными элементами образа в двойственном порядке.

LaTeX

$$$\\text{Image}(f, \\{x \\mid Maximal P x\\}) = \\{x \\mid Maximal (\\exists x_0, P x_0 \\land f x_0 = x)\\}$$$

Lean4

theorem image_monotone_setOf_maximal (hf : ∀ ⦃x y⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)) :
    f '' {x | Maximal P x} = {x | Maximal (∃ x₀, P x₀ ∧ f x₀ = ·) x} :=
  image_monotone_setOf_minimal (α := αᵒᵈ) (β := βᵒᵈ) (fun _ _ hx hy ↦ hf hy hx)

Похожие утверждения