Theorems · Definition · order theory

OrderIso.withTopCongr

{α : Type u_1} → {β : Type u_2} → [inst : PartialOrder α] → [inst_1 : PartialOrder β] → α ≃o β → WithTop α ≃o WithTop β

A version of Equiv.optionCongr for WithTop.

Defined in

Mathlib.Order.Hom.WithTopBot

Cited by

6 results in Mathlib

Foundations

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

Assumes

PartialOrderPartialOrder