image_antitone_setOf_minimal — Mathlib

English

With an antitone f, the image of the set of minimal elements of s equals the set of maximal elements of the image set, under the right duality.

Русский

С антитоничным f образ минимальных элементов s равен множеству максимальных элементов образа при правильной двойственности.

LaTeX

$$$\\text{Image}(f, \\{x \\mid Minimal P x\\}) = \\{x \\mid Maximal (\\exists x_0, P x_0 ∧ f x_0 = x)\\}$$$

Lean4

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

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