Description: The closed unit interval is a subset of the set of the complex numbers. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 12-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | unitsscn | |- ( 0 [,] 1 ) C_ CC |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unitssre | |- ( 0 [,] 1 ) C_ RR |
|
2 | ax-resscn | |- RR C_ CC |
|
3 | 1 2 | sstri | |- ( 0 [,] 1 ) C_ CC |