begin
theorem
theorem
theorem
:: deftheorem defines R_EAL MEASURE6:def 1 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem Th41:
theorem
canceled;
theorem
canceled;
theorem
theorem Th45:
theorem
theorem Th47:
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem MEASURE6:def 2 :
canceled;
:: deftheorem MEASURE6:def 3 :
canceled;
:: deftheorem MEASURE6:def 4 :
canceled;
:: deftheorem MEASURE6:def 5 :
canceled;
:: deftheorem Def6 defines ++ MEASURE6:def 6 :
theorem Th59:
theorem
theorem
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
theorem Th68:
theorem
begin
:: deftheorem Def1 defines without_zero MEASURE6:def 7 :
theorem Th1:
:: deftheorem Def2 defines " MEASURE6:def 8 :
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th6:
theorem Th7:
:: deftheorem Def3 defines with_max MEASURE6:def 9 :
:: deftheorem Def4 defines with_min MEASURE6:def 10 :
:: deftheorem Def5 defines open MEASURE6:def 11 :
:: deftheorem Def6X defines closed MEASURE6:def 12 :
:: deftheorem defines - MEASURE6:def 13 :
theorem Th14:
Lm1:
for X being Subset of REAL st X is bounded_above holds
- X is bounded_below
Lm2:
for X being Subset of REAL st X is bounded_below holds
- X is bounded_above
theorem Th15:
theorem
theorem Th17:
theorem Th18:
Lm3:
for X being Subset of REAL st X is closed holds
- X is closed
theorem Th19:
:: deftheorem defines ++ MEASURE6:def 14 :
theorem Th20:
theorem Th21:
theorem Th22:
Lm4:
for X being Subset of REAL
for s being Real st X is bounded_above holds
s ++ X is bounded_above
theorem
Lm5:
for X being Subset of REAL
for p being Real st X is bounded_below holds
p ++ X is bounded_below
theorem
theorem
theorem
Lm6:
for q3 being Real
for X being Subset of REAL st X is closed holds
q3 ++ X is closed
theorem Th27:
:: deftheorem defines Inv MEASURE6:def 15 :
theorem Th28:
theorem
theorem Th31:
:: deftheorem defines Cl MEASURE6:def 16 :
theorem Th32:
theorem Th33:
theorem Th34:
theorem
theorem
theorem
theorem Th38:
theorem Th39:
begin
:: deftheorem Def11 defines bounded_below MEASURE6:def 17 :
:: deftheorem Def12 defines bounded_above MEASURE6:def 18 :
:: deftheorem Def14 defines with_max MEASURE6:def 19 :
:: deftheorem Def15 defines with_min MEASURE6:def 20 :
theorem Th40:
Lm7:
for X being non empty set
for f being Function of X,REAL st f is with_max holds
- f is with_min
Lm8:
for X being non empty set
for f being Function of X,REAL st f is with_min holds
- f is with_max
theorem Th41:
theorem
theorem Th43:
theorem
theorem Th45:
theorem Th46: