Description: The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | tgioo2.1 | |- J = ( TopOpen ` CCfld ) |
|
| rerest.2 | |- R = ( topGen ` ran (,) ) |
||
| Assertion | rerest | |- ( A C_ RR -> ( J |`t A ) = ( R |`t A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | tgioo2.1 | |- J = ( TopOpen ` CCfld ) |
|
| 2 | rerest.2 | |- R = ( topGen ` ran (,) ) |
|
| 3 | 1 | tgioo2 | |- ( topGen ` ran (,) ) = ( J |`t RR ) |
| 4 | 2 3 | eqtri | |- R = ( J |`t RR ) |
| 5 | 4 | oveq1i | |- ( R |`t A ) = ( ( J |`t RR ) |`t A ) |
| 6 | 1 | cnfldtop | |- J e. Top |
| 7 | reex | |- RR e. _V |
|
| 8 | restabs | |- ( ( J e. Top /\ A C_ RR /\ RR e. _V ) -> ( ( J |`t RR ) |`t A ) = ( J |`t A ) ) |
|
| 9 | 6 7 8 | mp3an13 | |- ( A C_ RR -> ( ( J |`t RR ) |`t A ) = ( J |`t A ) ) |
| 10 | 5 9 | syl5req | |- ( A C_ RR -> ( J |`t A ) = ( R |`t A ) ) |