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 ) |