Theorems · Definition · order theory

WithTop.subtypeOrderIso

{α : Type u_1} →
  [inst : PartialOrder α] → [inst_1 : OrderTop α] → [DecidablePred fun x => x = ⊤] → WithTop { a // a ≠ ⊤ } ≃o α

Any OrderTop is equivalent to WithTop of the subtype excluding ⊤. See also Equiv.optionSubtypeNe.

Defined in

Mathlib.Order.Hom.WithTopBot

Cited by

2 results in Mathlib

Foundations

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

Assumes

PartialOrderOrderTopDecidablePred