Theorems · Theorem · order theory

minimal_mem_image_monotone_iff

∀ {α : Type u_2} {β : Type u_3} {a : α} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α → β},
  a ∈ s →
    (∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) →
      (Minimal (fun x => x ∈ f '' s) (f a) ↔ Minimal (fun x => x ∈ s) a)

Defined in

Mathlib.Order.Minimal

Cited by

3 results in Mathlib

Foundations

Depth 7 from the axioms · uses propext

Assumes

PreorderPreorder