Description: The outer measure of a set is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | omexrcl.o | |- ( ph -> O e. OutMeas ) |
|
omexrcl.x | |- X = U. dom O |
||
omexrcl.a | |- ( ph -> A C_ X ) |
||
Assertion | omexrcl | |- ( ph -> ( O ` A ) e. RR* ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | omexrcl.o | |- ( ph -> O e. OutMeas ) |
|
2 | omexrcl.x | |- X = U. dom O |
|
3 | omexrcl.a | |- ( ph -> A C_ X ) |
|
4 | iccssxr | |- ( 0 [,] +oo ) C_ RR* |
|
5 | 1 2 3 | omecl | |- ( ph -> ( O ` A ) e. ( 0 [,] +oo ) ) |
6 | 4 5 | sseldi | |- ( ph -> ( O ` A ) e. RR* ) |