Description: The topology on the extended reals coincides with the standard topology on the reals, when restricted to RR . (Contributed by Glauco Siliprandi, 5-Feb-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | xrtgioo2 | |- ( topGen ` ran (,) ) = ( ( ordTop ` <_ ) |`t RR ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid | |- ( ( ordTop ` <_ ) |`t RR ) = ( ( ordTop ` <_ ) |`t RR ) |
|
| 2 | 1 | xrtgioo | |- ( topGen ` ran (,) ) = ( ( ordTop ` <_ ) |`t RR ) |