Theorems · Theorem · order theory

minimal_mem_image_monotone

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

Defined in

Mathlib.Order.Minimal

Cited by

3 results in Mathlib

Foundations

Depth 6 from the axioms · uses propext

Assumes

PreorderPreorder