The abstract of the Mizar article:

Darboux's Theorem

by

Noboru Endou,

Katsumi Wasaki, and

Yasunari Shidama

Received December 7, 1999

MML identifier: INTEGRA3

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_1, ARYTM_1, INTEGRA1, MEASURE5, RELAT_1, ORDINAL2, BOOLE,
      FUNCT_1, CARD_1, FUNCT_3, SQUARE_1, ABSVALUE, RFUNCT_1, RLVECT_1, SEQ_2,
      LATTICES, JORDAN3, RCOMP_1, PARTFUN1, RFINSEQ, INTEGRA2, FDIFF_1, SEQ_1,
      ARYTM_3, PROB_1, FINSEQ_4, ARYTM;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, RELSET_1, SEQ_4, PARTFUN1,
      PSCOMP_1, FINSEQ_1, RFUNCT_1, RVSUM_1, INTEGRA1, SEQ_1, SEQ_2, JORDAN3,
      PRE_CIRC, SFMASTR3, RCOMP_1, FDIFF_1, ABSVALUE, GOBOARD1, CARD_1,
      SQUARE_1, FINSEQ_4, TOPREAL1, RFINSEQ, BINARITH, INTEGRA2;
 constructors REAL_1, REALSET1, PARTFUN1, RFUNCT_1, PRE_CIRC, SFMASTR3,
      FDIFF_1, SQUARE_1, FINSEQ_4, RFINSEQ, TOPREAL1, BINARITH, JORDAN3,
      INTEGRA2, ABSVALUE, PSCOMP_1, FINSOP_1;
 clusters XREAL_0, RELSET_1, FINSEQ_1, NAT_2, GOBOARD1, INTEGRA1, INTEGRA2,
      NAT_1, MEMBERED, NUMBERS, ORDINAL2;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Lemmas of Division

reserve a,b,d,e,x,y for Real,
        i,j,k,n,m for Nat,
        x1 for set,
        p,q for FinSequence of REAL;

theorem :: INTEGRA3:1
for A be closed-interval Subset of REAL, D be Element of divs A
st vol(A) <> 0 holds ex i st i in dom D & vol(divset(D,i)) > 0;

theorem :: INTEGRA3:2
for A be closed-interval Subset of REAL,
D be Element of divs A st x in A holds
ex j st j in dom D & x in divset(D,j);

theorem :: INTEGRA3:3
for A be closed-interval Subset of REAL,
                 D1,D2 be Element of divs A holds
ex D be Element of divs A st D1 <= D & D2 <= D & rng D = rng D1 \/ rng D2;

theorem :: INTEGRA3:4
for A be closed-interval Subset of REAL,
D,D1 be Element of divs A
st delta(D1)<min rng upper_volume(chi(A,A),D)
holds (for x,y,i st i in dom D1 & x in rng D /\ divset(D1,i)
& y in rng D /\ divset(D1,i) holds x=y);

theorem :: INTEGRA3:5
for p,q st rng p = rng q & p is increasing & q is increasing holds p = q;

theorem :: INTEGRA3:6
for A be closed-interval Subset of REAL, D,D1 be Element of divs A st
D <= D1 & i in dom D & j in dom D & i <= j holds
indx(D1,D,i) <= indx(D1,D,j) & indx(D1,D,i) in dom D1;

theorem :: INTEGRA3:7
for A be closed-interval Subset of REAL, D,D1 be Element of divs A
st D <= D1 & i in dom D & j in dom D & i < j holds
indx(D1,D,i) < indx(D1,D,j);

theorem :: INTEGRA3:8
for A be closed-interval Subset of REAL,
D be Element of divs A holds delta(D) >= 0;

theorem :: INTEGRA3:9
for A be closed-interval Subset of REAL, g be Function of A,REAL,
D1,D2 be Element of divs A st x in divset(D1,len D1) & len D1 >= 2
& D1<=D2 & rng D2 = rng D1 \/ {x} & g is_bounded_on A
holds Sum lower_volume(g,D2)-Sum
lower_volume(g,D1)<=(sup rng g-inf rng g)*delta(D1);

theorem :: INTEGRA3:10
for A be closed-interval Subset of REAL, g be Function of A,REAL,
D1,D2 be Element of divs A st x in divset(D1,len D1) & len D1 >= 2
& D1<=D2 & rng D2 = rng D1 \/ {x} & g is_bounded_on A
holds Sum upper_volume(g,D1)-Sum
upper_volume(g,D2)<=(sup rng g-inf rng g)*delta(D1);

theorem :: INTEGRA3:11
for A be closed-interval Subset of REAL, D be Element of divs A,
r be Real, i,j be Nat st i in dom D & j in dom D & i<=j & r < mid(D,i,j).1
holds ex B be closed-interval Subset of REAL
st r=inf B & sup B=mid(D,i,j).(len mid(D,i,j))
& len mid(D,i,j)=j-i+1 & mid(D,i,j) is DivisionPoint of B;

theorem :: INTEGRA3:12
for A be closed-interval Subset of REAL, f be Function of A,REAL,
D1,D2 be Element of divs A st x in divset(D1,len D1) & vol(A)<>0
& D1<=D2 & rng D2 = rng D1 \/ {x} & f is_bounded_on A & x > inf A
holds Sum lower_volume(f,D2)-Sum
lower_volume(f,D1)<=(sup rng f-inf rng f)*delta(D1);

theorem :: INTEGRA3:13
for A be closed-interval Subset of REAL, f be Function of A,REAL,
D1,D2 be Element of divs A st x in divset(D1,len D1) & vol(A)<>0
& D1<=D2 & rng D2 = rng D1 \/ {x} & f is_bounded_on A & x > inf A
holds Sum upper_volume(f,D1)-Sum
upper_volume(f,D2)<=(sup rng f-inf rng f)*delta(D1);

theorem :: INTEGRA3:14
for A be closed-interval Subset of REAL, D1,D2 be Element of divs A,
r be Real, i,j be Nat st i in dom D1 & j in dom D1 & i<=j & D1 <= D2
& r < mid(D2,indx(D2,D1,i),indx(D2,D1,j)).1
holds ex B be closed-interval Subset of REAL, MD1,MD2 be Element of divs B
st r=inf B & sup B=MD2.(len MD2) & sup B=MD1.(len MD1) & MD1 <= MD2
& MD1=mid(D1,i,j) & MD2=mid(D2,indx(D2,D1,i),indx(D2,D1,j));

theorem :: INTEGRA3:15
for A be closed-interval Subset of REAL, D be Element of divs A
st x in rng D holds D.1 <= x & x <= D.(len D);

theorem :: INTEGRA3:16
for p be FinSequence of REAL, i,j,k st p is increasing & i in dom p
& j in dom p & k in dom p & p.i <= p.k & p.k <= p.j holds
p.k in rng mid(p,i,j);

theorem :: INTEGRA3:17
for A be closed-interval Subset of REAL, f be Function of A,REAL,
D be Element of divs A st f is_bounded_on A & i in dom D
holds inf rng(f|divset(D,i)) <= sup rng f;

theorem :: INTEGRA3:18
for A be closed-interval Subset of REAL, f be Function of A,REAL,
D be Element of divs A st f is_bounded_on A & i in dom D
holds sup rng(f|divset(D,i)) >= inf rng f;

begin :: Darboux's Theorem

theorem :: INTEGRA3:19
  for A be closed-interval Subset of REAL, f be Function of A,REAL,
T be DivSequence of A
st f is_bounded_on A & delta(T) is convergent_to_0 & vol(A)<>0
holds lower_sum(f,T) is convergent & lim lower_sum(f,T) = lower_integral(f);

theorem :: INTEGRA3:20
  for A be closed-interval Subset of REAL, f be Function of A,REAL,
T be DivSequence of A
st f is_bounded_on A & delta(T) is convergent_to_0 & vol(A)<>0
holds upper_sum(f,T) is convergent & lim upper_sum(f,T) = upper_integral(f);