Description: The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014) (Revised by Thierry Arnoux, 3-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Hypothesis | tgioo3.1 | ⊢ 𝐽 = ( TopOpen ‘ ℝfld ) | |
Assertion | tgioo3 | ⊢ ( topGen ‘ ran (,) ) = 𝐽 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tgioo3.1 | ⊢ 𝐽 = ( TopOpen ‘ ℝfld ) | |
2 | eqid | ⊢ ( ℂfld ↾s ℝ ) = ( ℂfld ↾s ℝ ) | |
3 | eqid | ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) | |
4 | 2 3 | resstopn | ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) = ( TopOpen ‘ ( ℂfld ↾s ℝ ) ) |
5 | 3 | tgioo2 | ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) |
6 | df-refld | ⊢ ℝfld = ( ℂfld ↾s ℝ ) | |
7 | 6 | fveq2i | ⊢ ( TopOpen ‘ ℝfld ) = ( TopOpen ‘ ( ℂfld ↾s ℝ ) ) |
8 | 1 7 | eqtri | ⊢ 𝐽 = ( TopOpen ‘ ( ℂfld ↾s ℝ ) ) |
9 | 4 5 8 | 3eqtr4i | ⊢ ( topGen ‘ ran (,) ) = 𝐽 |