Theorems · Theorem · order theory

OrderIso.image_setOfPred_maximal

∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (P : α → Prop),
  ⇑f '' {x | Maximal P x} = {x | Maximal (fun x => P (f.symm x)) x}

Defined in

Mathlib.Order.Minimal

Cited by

1 results in Mathlib

Foundations

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

Assumes

PreorderPreorder