minimal_mem_image_antitone — Mathlib

English

Using dual order, minimality in s corresponds to maximality in the dual order image, and vice versa.

Русский

Используя двойственный порядок, минимальность в s соответствует максимальности в образе в двойственном порядке и наоборот.

LaTeX

$$$(\\text{Minimal}(\\cdot \\in s)\\, x) \\iff (\\text{Maximal}(\\cdot \\in s)\\, x)\\text{ under dual order}.$$$

Lean4

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

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