Theorems · Theorem · order theory

OrderEmbedding.minimal_mem_image_iff

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

Defined in

Mathlib.Order.Minimal

Cited by

0 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext, Quot.sound

Assumes

PreorderPreorder