Description: The Lebesgue measure of a set is an extended real. (Contributed by Glauco Siliprandi, 8-Apr-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | vonxrcl.x | ||
vonxrcl.s | |||
vonxrcl.a | |||
Assertion | vonxrcl |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vonxrcl.x | ||
2 | vonxrcl.s | ||
3 | vonxrcl.a | ||
4 | iccssxr | ||
5 | 1 2 3 | voncl | |
6 | 4 5 | sseldi |