Table of ContentsTable of Contents Mathbox for Jeff Madsen < Previous   Next >
Related theorems
Unicode version

Definition df-ii 16530
Description: Define the unit interval with the Euclidean topology.
Assertion
Ref Expression
df-ii |- II = (MetOpen` ((abs o. - ) |` ((0[,]1) X. (0[,]1))))

Detailed syntax breakdown of Definition df-ii
StepHypRef Expression
1 cii 16529 . 2 class II
2 cabs 8925 . . . . 5 class abs
3 cmin 7328 . . . . 5 class -
42, 3ccom 4141 . . . 4 class (abs o. - )
5 cc0 7106 . . . . . 6 class 0
6 c1 7107 . . . . . 6 class 1
7 cicc 8401 . . . . . 6 class [,]
85, 6, 7co 5067 . . . . 5 class (0[,]1)
98, 8cxp 4135 . . . 4 class ((0[,]1) X. (0[,]1))
104, 9cres 4139 . . 3 class ((abs o. - ) |` ((0[,]1) X. (0[,]1)))
11 copn 10647 . . 3 class MetOpen
1210, 11cfv 4149 . 2 class (MetOpen` ((abs o. - ) |` ((0[,]1) X. (0[,]1))))
131, 12wceq 1592 1 wff II = (MetOpen` ((abs o. - ) |` ((0[,]1) X. (0[,]1))))
Colors of variables: wff set class
This definition is referenced by:  iitop 16531  iiuni 16532  dfii2 16533  dfii3 16534  iicmp 16663  phtpycom 16685  phtpycolem3 16688  phtpycolem4 16689  pcocn 16711  pcohtpylem3 16717  pcopt 16719  pcoass 16720  pcorev 16722  pi1gp 16730
Copyright terms: Public domain