theorem WithBot.coe_ne_coe {α : Type u_1} {a : α} {b : α} : ↑a ≠ ↑b ↔ a ≠ b

instance WithBot.instIsStrictTotalOrderLtOfIsWellOrder_conNF {α : Type u_1} [LT α] [IsWellOrder α fun (x x_1 : α) => x < x_1] : IsStrictTotalOrder (WithBot α) fun (x x_1 : WithBot α) => x < x_1

Equations

• ⋯ = ⋯

instance WithBot.instIsWellOrderLt_conNF {α : Type u_1} [Preorder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] : IsWellOrder (WithBot α) fun (x x_1 : WithBot α) => x < x_1

Equations

• ⋯ = ⋯