Description: The outer measure of a set is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | omexrcl.o | ||
omexrcl.x | |||
omexrcl.a | |||
Assertion | omexrcl |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | omexrcl.o | ||
2 | omexrcl.x | ||
3 | omexrcl.a | ||
4 | iccssxr | ||
5 | 1 2 3 | omecl | |
6 | 4 5 | sseldi |