Description: The measure of the intersection of any two preimages by simple functions is a real number. (Contributed by Thierry Arnoux, 21-Mar-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sitgval.b | |
|
sitgval.j | |
||
sitgval.s | |
||
sitgval.0 | |
||
sitgval.x | |
||
sitgval.h | |
||
sitgval.1 | |
||
sitgval.2 | |
||
sibfmbl.1 | |
||
sibfinima.g | |
||
sibfinima.w | |
||
sibfinima.j | |
||
Assertion | sibfinima | |