Description: The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Glauco Siliprandi, 5-Feb-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | tgioo4 | |- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld ) |
|
2 | 1 | tgioo2 | |- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR ) |