minimal_mem_image_antitone_iff — Mathlib

English

If f is antitone with respect to s, then the image of the minimal elements of s is exactly the minimal elements of the image set.

Русский

Если f антитонично относительно s, образ минимальных элементов s совпадает с минимальными элементами образа.

LaTeX

$$$f '' \\{x \\mid Minimal(\\cdot \\in s) x\\} = \\{x \\mid Minimal(\\cdot \\in f''s) x\\}$ under appropriate conditions.$$

Lean4

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

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