Lemmas about images of intervals under order isomorphisms. #
Order isomorphism between Iic (⊤ : α)
and α
when α
has a top element
Equations
- OrderIso.IicTop = let __src := Equiv.subtypeUnivEquiv ⋯; { toEquiv := __src, map_rel_iff' := ⋯ }
Instances For
Order isomorphism between Ici (⊥ : α)
and α
when α
has a bottom element
Equations
- OrderIso.IciBot = let __src := Equiv.subtypeUnivEquiv ⋯; { toEquiv := __src, map_rel_iff' := ⋯ }