Description: The topology induced by a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tuslem.k | |- K = ( toUnifSp ` U ) |
|
tustopn.j | |- J = ( unifTop ` U ) |
||
Assertion | tustopn | |- ( U e. ( UnifOn ` X ) -> J = ( TopOpen ` K ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tuslem.k | |- K = ( toUnifSp ` U ) |
|
2 | tustopn.j | |- J = ( unifTop ` U ) |
|
3 | 1 | tuslem | |- ( U e. ( UnifOn ` X ) -> ( X = ( Base ` K ) /\ U = ( UnifSet ` K ) /\ ( unifTop ` U ) = ( TopOpen ` K ) ) ) |
4 | 3 | simp3d | |- ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) = ( TopOpen ` K ) ) |
5 | 2 4 | syl5eq | |- ( U e. ( UnifOn ` X ) -> J = ( TopOpen ` K ) ) |