maximal_mem_image_monotone_iff — Mathlib

English

If x ∈ s and f preserves order, then maximality in s corresponds to maximality in the image, yielding an equivalence.

Русский

Если x ∈ s и f сохраняет порядок, то максимальность в s соответствует максимальности образа, образуя эквивалентность.

LaTeX

$$$(x \\in s) \\Rightarrow (\\text{Maximal}(\\cdot \\in s)\\, x \\iff \\text{Maximal}(\\cdot \\in f''s)\\, f(x)).$$$

Lean4

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

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