Database
BASIC TOPOLOGY
Metric spaces
Topological definitions using the reals
iitop
Next ⟩
iiuni
Metamath Proof Explorer
Ascii
Structured
Theorem
iitop
Description:
The unit interval is a topological space.
(Contributed by
Jeff Madsen
, 2-Sep-2009)
Ref
Expression
Assertion
iitop
⊢
II ∈ Top
Proof
Step
Hyp
Ref
Expression
1
iitopon
⊢
II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
2
1
topontopi
⊢
II ∈ Top