:: The One-Dimensional Lebesgue Measure As an Example of aFormalization in the Mizar Language of the Classical Definitionof a Mathematical Object
:: by J\'ozef Bia{\l}as
::
:: Received February 4, 1995
:: Copyright (c) 1995 Association of Mizar Users
theorem Th1: :: MEASURE7:1
theorem Th2: :: MEASURE7:2
theorem Th3: :: MEASURE7:3
theorem Th4: :: MEASURE7:4
theorem :: MEASURE7:5
canceled;
theorem Th6: :: MEASURE7:6
theorem Th7: :: MEASURE7:7
:: deftheorem Def1 defines On MEASURE7:def 1 :
theorem Th8: :: MEASURE7:8
theorem Th9: :: MEASURE7:9
theorem Th10: :: MEASURE7:10
theorem Th11: :: MEASURE7:11
theorem Th12: :: MEASURE7:12
REAL in bool REAL
by ZFMISC_1:def 1;
then reconsider G0 = NAT --> REAL as Function of NAT , bool REAL by FUNCOP_1:57;
Lm2:
rng G0 = {REAL }
by FUNCOP_1:14;
Lm3:
REAL c= union (rng G0)
by Lm2, ZFMISC_1:31;
Lm4:
for n being Element of NAT holds G0 . n is Interval
:: deftheorem Def2 defines Interval_Covering MEASURE7:def 2 :
:: deftheorem Def3 defines Interval_Covering MEASURE7:def 3 :
:: deftheorem Def4 defines vol MEASURE7:def 4 :
theorem Th13: :: MEASURE7:13
:: deftheorem defines vol MEASURE7:def 5 :
:: deftheorem defines vol MEASURE7:def 6 :
:: deftheorem Def7 defines vol MEASURE7:def 7 :
theorem Th14: :: MEASURE7:14
:: deftheorem Def8 defines Svc MEASURE7:def 8 :
:: deftheorem defines COMPLEX MEASURE7:def 9 :
:: deftheorem Def10 defines OS_Meas MEASURE7:def 10 :
:: deftheorem defines pr1 MEASURE7:def 11 :
:: deftheorem Def12 defines pr2 MEASURE7:def 12 :
:: deftheorem Def13 defines On MEASURE7:def 13 :
reconsider D = NAT --> ({} REAL ) as Function of NAT , bool REAL ;
theorem Th15: :: MEASURE7:15
theorem Th16: :: MEASURE7:16
theorem Th17: :: MEASURE7:17
:: deftheorem defines Lmi_sigmaFIELD MEASURE7:def 14 :
:: deftheorem defines L_mi MEASURE7:def 15 :