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 ) ⊆ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unitssre | ⊢ ( 0 [,] 1 ) ⊆ ℝ | |
2 | ax-resscn | ⊢ ℝ ⊆ ℂ | |
3 | 1 2 | sstri | ⊢ ( 0 [,] 1 ) ⊆ ℂ |