Theorems · Definition · order theory

WithBot.toDualTopEquiv

{α : Type u_1} → [inst : LE α] → WithBot αᵒᵈ ≃o (WithTop α)ᵒᵈ

Taking the dual then adding ⊥ is the same as adding ⊤ then taking the dual. This is the order iso form of WithBot.ofDual, as proven by coe_toDualTopEquiv.

Defined in

Mathlib.Order.Hom.WithTopBot

Cited by

6 results in Mathlib

Foundations

Depth 17 from the axioms · uses Quot.sound

Assumes

LE