maximal_mem_image_monotone — Mathlib

English

If f preserves order monotone on s, then maximal elements map to maximal elements of the image.

Русский

Если отображение сохраняет порядок на s, то максимальные элементы s переходят к максимальным элементам образа.

LaTeX

$$$\\forall x,\\; Maximal(\\cdot \\in s)\\, x \\Rightarrow Maximal(\\cdot \\in f''s)\\,(f(x)).$$$

Lean4

theorem maximal_mem_image_monotone (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) (hx : Maximal (· ∈ s) x) :
    Maximal (· ∈ f '' s) (f x) :=
  minimal_mem_image_monotone (α := αᵒᵈ) (β := βᵒᵈ) (s := s) (fun _ _ hx hy ↦ hf hy hx) hx

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