Description: A complete uniform space is an uniform space. (Contributed by Thierry Arnoux, 3-Dec-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | cuspusp | |- ( W e. CUnifSp -> W e. UnifSp ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iscusp | |- ( W e. CUnifSp <-> ( W e. UnifSp /\ A. c e. ( Fil ` ( Base ` W ) ) ( c e. ( CauFilU ` ( UnifSt ` W ) ) -> ( ( TopOpen ` W ) fLim c ) =/= (/) ) ) ) |
|
2 | 1 | simplbi | |- ( W e. CUnifSp -> W e. UnifSp ) |