Description: This theorem's hypotheses define a pre-measure. A pre-measure is monotone. (Contributed by Thierry Arnoux, 19-Jul-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | caraext.1 | |
|
caraext.2 | |
||
caraext.3 | |
||
pmeasmono.1 | |
||
pmeasmono.2 | |
||
pmeasmono.3 | |
||
pmeasmono.4 | |
||
Assertion | pmeasmono | |