maximal_mem_image_antitone_iff — Mathlib

English

For an antitone f, the maximality of f(a) in the image corresponds to minimality of a in the domain under the dual order.

Русский

Для антитоничного f максимальность f(a) в образе соответствует минимальности a в области под двойственным порядком.

LaTeX

$$$(f '' s)\\;\\text{Maximal at } f(a) \\iff (s\\, Minimal at } a)$ under dual order.$$

Lean4

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

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