image_antitone_setOf_maximal — Mathlib

English

For an antitone f, maximality of f(a) in the image is equivalent to minimality of a in the domain.

Русский

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

LaTeX

$$$(\\text{Maximal}(\\cdot \\in f''s)\\,(f(a))) \\iff (\\text{Minimal}(\\cdot \\in s)\\, a)$$$

Lean4

theorem image_antitone_setOf_maximal (hf : ∀ ⦃x y⦄, P x → P y → (f x ≤ f y ↔ y ≤ x)) :
    f '' {x | Maximal P x} = {x | Minimal (∃ x₀, P x₀ ∧ f x₀ = ·) x} :=
  image_monotone_setOf_maximal (β := βᵒᵈ) (fun _ _ hx hy ↦ hf hy hx)

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