Description: A measure is continuous from below. Cf. volsup . (Contributed by Thierry Arnoux, 18-Jan-2017) (Revised by Thierry Arnoux, 11-Jul-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | meascnbl.0 | |
|
meascnbl.1 | |
||
meascnbl.2 | |
||
meascnbl.3 | |
||
Assertion | meascnbl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | meascnbl.0 | |
|
2 | meascnbl.1 | |
|
3 | meascnbl.2 | |
|
4 | meascnbl.3 | |
|
5 | 2 | adantr | |
6 | measbase | |
|
7 | 2 6 | syl | |
8 | 7 | adantr | |
9 | 3 | ffvelrnda | |
10 | simpll | |
|
11 | fzossnn | |
|
12 | simpr | |
|
13 | 11 12 | sselid | |
14 | 3 | ffvelrnda | |
15 | 10 13 14 | syl2anc | |
16 | 15 | ralrimiva | |
17 | sigaclfu2 | |
|
18 | 8 16 17 | syl2anc | |
19 | difelsiga | |
|
20 | 8 9 18 19 | syl3anc | |
21 | measvxrge0 | |
|
22 | 5 20 21 | syl2anc | |
23 | fveq2 | |
|
24 | oveq2 | |
|
25 | 24 | iuneq1d | |
26 | 23 25 | difeq12d | |
27 | 26 | fveq2d | |
28 | fveq2 | |
|
29 | oveq2 | |
|
30 | 29 | iuneq1d | |
31 | 28 30 | difeq12d | |
32 | 31 | fveq2d | |
33 | 1 22 27 32 | esumcvg2 | |
34 | measfrge0 | |
|
35 | 2 34 | syl | |
36 | fcompt | |
|
37 | 35 3 36 | syl2anc | |
38 | nfcv | |
|
39 | fveq2 | |
|
40 | simpr | |
|
41 | 40 | nnzd | |
42 | fzval3 | |
|
43 | 41 42 | syl | |
44 | 43 | olcd | |
45 | 2 | adantr | |
46 | simpll | |
|
47 | fzossnn | |
|
48 | 43 | eleq2d | |
49 | 48 | biimpa | |
50 | 47 49 | sselid | |
51 | 46 50 9 | syl2anc | |
52 | 38 39 44 45 51 | measiuns | |
53 | 3 | ffnd | |
54 | 53 4 | iuninc | |
55 | 54 | fveq2d | |
56 | 52 55 | eqtr3d | |
57 | 56 | mpteq2dva | |
58 | 37 57 | eqtr4d | |
59 | 9 | ralrimiva | |
60 | dfiun2g | |
|
61 | 59 60 | syl | |
62 | fnrnfv | |
|
63 | 53 62 | syl | |
64 | 63 | unieqd | |
65 | 61 64 | eqtr4d | |
66 | 65 | fveq2d | |
67 | eqidd | |
|
68 | 67 | orcd | |
69 | 38 39 68 2 9 | measiuns | |
70 | 66 69 | eqtr3d | |
71 | 33 58 70 | 3brtr4d | |