Description: If the metric D is "strongly finer" than C (meaning that there is a positive real constant R such that C ( x , y ) <_ R x. D ( x , y ) ), then D generates a finer topology. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they generate the same topology.) (Contributed by Mario Carneiro, 14-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | metequiv.3 | |
|
metequiv.4 | |
||
metss2.1 | |
||
metss2.2 | |
||
metss2.3 | |
||
metss2.4 | |
||
Assertion | metss2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | metequiv.3 | |
|
2 | metequiv.4 | |
|
3 | metss2.1 | |
|
4 | metss2.2 | |
|
5 | metss2.3 | |
|
6 | metss2.4 | |
|
7 | simpr | |
|
8 | rpdivcl | |
|
9 | 7 5 8 | syl2anr | |
10 | 1 2 3 4 5 6 | metss2lem | |
11 | oveq2 | |
|
12 | 11 | sseq1d | |
13 | 12 | rspcev | |
14 | 9 10 13 | syl2anc | |
15 | 14 | ralrimivva | |
16 | metxmet | |
|
17 | 3 16 | syl | |
18 | metxmet | |
|
19 | 4 18 | syl | |
20 | 1 2 | metss | |
21 | 17 19 20 | syl2anc | |
22 | 15 21 | mpbird | |