Theorems · Theorem · order theory

WithTop.subtypeOrderIso_apply_coe

∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] [inst_2 : DecidablePred fun x => x = ⊤]
  (a : { a // a ≠ ⊤ }), WithTop.subtypeOrderIso ↑a = ↑a

Defined in

Mathlib.Order.Hom.WithTopBot

Cited by

2 results in Mathlib

Foundations

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

Assumes

PartialOrderOrderTopDecidablePred