Description: The topology of the extended nonnegative real numbers is Hausdorff. (Contributed by Thierry Arnoux, 26-Jul-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | xrge0haus | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xrge0topn | |
|
2 | xrhaus | |
|
3 | ovex | |
|
4 | resthaus | |
|
5 | 2 3 4 | mp2an | |
6 | 1 5 | eqeltri | |