Description: The bijection from [ -u 1 , 1 ] to the extended reals is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 9-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | xrhmeo.f | |
|
xrhmeo.g | |
||
xrhmeo.j | |
||
Assertion | xrhmeo | |