maximal_mem_image_antitone — Mathlib

English

If f is antitone, maximality in s maps to minimality in the image in the opposite order, and vice versa.

Русский

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

LaTeX

$$$(\\text{Maximal}(\\cdot \\in s)\\, x) \\Rightarrow (\\text{Minimal}(\\cdot \\in f''s)\\, f(x))$ под антипорядком и наоборот.$$

Lean4

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

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