image_monotone_setOf_minimal_mem — Mathlib

English

A variant form stating the equivalence of maximality in the image and minimality in the domain for an antitone f.

Русский

Вариант формулировки эквивалентности для антитоничного отображения: максимальность образа ⇔ минимальность в области.

LaTeX

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

Lean4

theorem image_monotone_setOf_minimal_mem (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) :
    f '' {x | Minimal (· ∈ s) x} = {x | Minimal (· ∈ f '' s) x} :=
  image_monotone_setOf_minimal hf

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