Volume 6, 1994

University of Bialystok

Copyright (c) 1994 Association of Mizar Users

### The abstract of the Mizar article:

### Some Properties of the Intervals

**by****Jozef Bialas**- Received February 5, 1994
- MML identifier: MEASURE6

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, RELAT_1, SUPINF_1, SUPINF_2, RLVECT_1, ARYTM_3, ORDINAL2, ARYTM_1, FINSEQ_1, MEASURE5, RCOMP_1, BOOLE, MEASURE6, ARYTM; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, RELAT_1, FUNCT_1, FUNCT_2, REAL_1, NAT_1, SUPINF_1, SUPINF_2, MEASURE5; constructors DOMAIN_1, NAT_1, REAL_1, SUPINF_2, MEASURE5, WELLORD2, MEMBERED, XBOOLE_0; clusters SUBSET_1, SUPINF_1, XREAL_0, RELSET_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin :: :: Some theorems about R_eal numbers :: theorem :: MEASURE6:1 ex F being Function of NAT,[:NAT,NAT:] st F is one-to-one & dom F = NAT & rng F = [:NAT,NAT:]; theorem :: MEASURE6:2 for F being Function of NAT,ExtREAL holds F is nonnegative implies 0. <=' SUM(F); theorem :: MEASURE6:3 for F being Function of NAT,ExtREAL holds for x being R_eal holds ((ex n being Nat st x <=' F.n) & F is nonnegative) implies x <=' SUM(F); canceled 4; theorem :: MEASURE6:8 for x,y being R_eal holds x is Real implies y - x + x = y & y + x - x = y; canceled; theorem :: MEASURE6:10 for x,y,z being R_eal holds z in REAL & y <' x implies (z + x) - (z + y) = x - y; theorem :: MEASURE6:11 for x,y,z being R_eal holds z in REAL & x <=' y implies z + x <=' z + y & x + z <=' y + z & x - z <=' y - z; theorem :: MEASURE6:12 for x,y,z being R_eal holds z in REAL & x <' y implies z + x <' z + y & x + z <' y + z & x - z <' y - z; definition let x be real number; func R_EAL x -> R_eal equals :: MEASURE6:def 1 x; end; theorem :: MEASURE6:13 for x,y being real number holds x <= y iff R_EAL x <=' R_EAL y; theorem :: MEASURE6:14 for x,y being real number holds x < y iff R_EAL x <' R_EAL y; theorem :: MEASURE6:15 for x,y,z being R_eal holds x <' y & y <' z implies y is Real; theorem :: MEASURE6:16 for x,y,z being R_eal holds x is Real & z is Real & x <=' y & y <=' z implies y is Real; theorem :: MEASURE6:17 for x,y,z being R_eal st (x is Real & x <=' y & y <' z) holds y is Real; theorem :: MEASURE6:18 for x,y,z being R_eal st (x <' y & y <=' z & z is Real) holds y is Real; theorem :: MEASURE6:19 for x,y being R_eal st 0. <' x & x <' y holds 0. <' y - x; theorem :: MEASURE6:20 for x,y,z being R_eal holds (0. <=' x & 0. <=' z & z + x <' y) implies z <' y - x; theorem :: MEASURE6:21 for x being R_eal holds x - 0. = x; theorem :: MEASURE6:22 for x,y,z being R_eal holds 0. <=' x & 0. <=' z & z + x <' y implies z <=' y; theorem :: MEASURE6:23 for x being R_eal holds 0. <' x implies ex y being R_eal st 0. <' y & y <' x; theorem :: MEASURE6:24 for x,z being R_eal st (0. <' x & x <' z) holds ex y being R_eal st 0. <' y & x + y <' z & y in REAL; theorem :: MEASURE6:25 for x,z being R_eal holds 0. <=' x & x <' z implies ex y being R_eal st 0. <' y & x + y <' z & y in REAL; theorem :: MEASURE6:26 for x being R_eal st 0. <' x holds ex y being R_eal st 0. <' y & y + y <' x; definition let x be R_eal; assume 0. <' x; func Seg(x) -> non empty Subset of ExtREAL means :: MEASURE6:def 2 for y being R_eal holds y in it iff (0. <' y & y + y <' x); end; definition let x be R_eal; func len(x) -> R_eal equals :: MEASURE6:def 3 sup Seg(x); end; theorem :: MEASURE6:27 for x being R_eal st 0. <' x holds 0. <' len(x); theorem :: MEASURE6:28 for x being R_eal st 0. <' x holds len(x) <=' x; theorem :: MEASURE6:29 for x being R_eal st 0. <' x & x <' +infty holds len(x) is Real; theorem :: MEASURE6:30 for x being R_eal st 0. <' x holds len(x) + len(x) <=' x; theorem :: MEASURE6:31 for eps being R_eal st 0. <' eps ex F being Function of NAT,ExtREAL st (for n being Nat holds 0. <' F.n) & SUM(F) <' eps; theorem :: MEASURE6:32 for eps being R_eal holds for X being non empty Subset of ExtREAL holds 0. <' eps & inf X is Real implies ex x being R_eal st x in X & x <' inf X + eps; theorem :: MEASURE6:33 for eps being R_eal holds for X being non empty Subset of ExtREAL holds 0. <' eps & sup X is Real implies ex x being R_eal st x in X & sup X - eps <' x; theorem :: MEASURE6:34 for F being Function of NAT,ExtREAL holds F is nonnegative & SUM(F) <' +infty implies for n being Nat holds F.n in REAL; :: :: PROPERTIES OF THE INTERVALS :: definition redefine func -infty -> R_eal; redefine func +infty -> R_eal; end; theorem :: MEASURE6:35 REAL is Interval & REAL = ].-infty,+infty.[ & REAL = [.-infty,+infty.] & REAL = [.-infty,+infty.[ & REAL = ].-infty,+infty.]; theorem :: MEASURE6:36 for a,b being R_eal holds b = -infty implies ].a,b.[ = {} & [.a,b.] = {} & [.a,b.[ = {} & ].a,b.] = {}; theorem :: MEASURE6:37 for a,b being R_eal holds a = +infty implies ].a,b.[ = {} & [.a,b.] = {} & [.a,b.[ = {} & ].a,b.] = {}; theorem :: MEASURE6:38 for A being Interval, a, b being R_eal, c, d, e being Real st A = ].a,b.[ & c in A & d in A & c <= e & e <= d holds e in A; theorem :: MEASURE6:39 for A being Interval, a, b being R_eal, c, d, e being Real st A = [.a,b.] & c in A & d in A & c <= e & e <= d holds e in A; theorem :: MEASURE6:40 for A being Interval, a, b being R_eal, c, d, e being Real st A = ].a,b.] & c in A & d in A & c <= e & e <= d holds e in A; theorem :: MEASURE6:41 for A being Interval, a, b being R_eal, c, d, e being Real st A = [.a,b.[ & c in A & d in A & c <= e & e <= d holds e in A; theorem :: MEASURE6:42 for A being non empty Subset of ExtREAL holds for m,M being R_eal st m = inf A & M = sup A holds (((for c,d being Real st c in A & d in A holds for e being Real st c <= e & e <= d holds e in A) & not m in A & not M in A) implies A = ].m,M.[); theorem :: MEASURE6:43 for A being non empty Subset of ExtREAL holds for m,M being R_eal st m = inf A & M = sup A holds (((for c,d being Real st c in A & d in A holds for e being Real st c <= e & e <= d holds e in A) & m in A & M in A & A c= REAL) implies A = [.m,M.]); theorem :: MEASURE6:44 for A being non empty Subset of ExtREAL holds for m,M being R_eal st m = inf A & M = sup A holds (((for c,d being Real st c in A & d in A holds for e being Real st c <= e & e <= d holds e in A) & m in A & not M in A & A c= REAL) implies A = [.m,M.[); theorem :: MEASURE6:45 for A being non empty Subset of ExtREAL holds for m,M being R_eal st m = inf A & M = sup A holds (((for c,d being Real st c in A & d in A holds for e being Real st c <= e & e <= d holds e in A) & not m in A & M in A & A c= REAL) implies A = ].m,M.]); theorem :: MEASURE6:46 for A being Subset of REAL holds A is Interval iff for a,b being Real st a in A & b in A holds for c being Real st a <= c & c <= b holds c in A; theorem :: MEASURE6:47 for A,B being Interval st A meets B holds A \/ B is Interval; definition let A be Interval; assume A <> {}; func ^^A -> R_eal means :: MEASURE6:def 4 ex b being R_eal st it <=' b & (A = ].it,b.[ or A = ].it,b.] or A = [.it,b.] or A = [.it,b.[); end; definition let A be Interval; assume A <> {}; func A^^ -> R_eal means :: MEASURE6:def 5 ex a being R_eal st a <=' it & (A = ].a,it.[ or A = ].a,it.] or A = [.a,it.] or A = [.a,it.[); end; theorem :: MEASURE6:48 for A being Interval holds A is open_interval & A <> {} implies ^^A <=' A^^ & A = ].^^A,A^^.[; theorem :: MEASURE6:49 for A being Interval holds A is closed_interval & A <> {} implies ^^A <=' A^^ & A = [.^^A,A^^.]; theorem :: MEASURE6:50 for A being Interval holds A is right_open_interval & A <> {} implies ^^A <=' A^^ & A = [.^^A,A^^.[; theorem :: MEASURE6:51 for A being Interval holds A is left_open_interval & A <> {} implies ^^A <=' A^^ & A = ].^^A,A^^.]; theorem :: MEASURE6:52 for A being Interval holds A <> {} implies ^^A <=' A^^ & (A = ].^^A,A^^.[ or A = ].^^A,A^^.] or A = [.^^A,A^^.] or A = [.^^A,A^^.[); canceled; theorem :: MEASURE6:54 for A being Interval holds for a being real number holds a in A implies ^^A <=' R_EAL a & R_EAL a <=' A^^; theorem :: MEASURE6:55 for A,B being Interval holds for a,b being real number st a in A & b in B holds A^^ <=' ^^B implies a <= b; theorem :: MEASURE6:56 for A being Interval holds for a being R_eal st a in A holds ^^A <=' a & a <=' A^^; theorem :: MEASURE6:57 for A being Interval st A <> {} holds for a being R_eal st ^^A <' a & a <' A^^ holds a in A; theorem :: MEASURE6:58 for A,B being Interval holds A^^ = ^^B & (A^^ in A or ^^B in B) implies A \/ B is Interval; definition let A be Subset of REAL; let x be real number; func x + A -> Subset of REAL means :: MEASURE6:def 6 for y being Real holds y in it iff ex z being Real st z in A & y = x + z; end; theorem :: MEASURE6:59 for A being Subset of REAL holds for x being real number holds -x + (x + A) = A; theorem :: MEASURE6:60 for x being real number holds for A being Subset of REAL holds A = REAL implies x + A = A; theorem :: MEASURE6:61 for x being real number holds x + {} = {}; theorem :: MEASURE6:62 for A being Interval holds for x being real number holds A is open_interval iff x + A is open_interval; theorem :: MEASURE6:63 for A being Interval holds for x being real number holds A is closed_interval iff x + A is closed_interval; theorem :: MEASURE6:64 for A being Interval holds for x being real number holds A is right_open_interval iff x + A is right_open_interval; theorem :: MEASURE6:65 for A being Interval holds for x being real number holds A is left_open_interval iff x + A is left_open_interval; theorem :: MEASURE6:66 for A being Interval holds for x being real number holds x + A is Interval; definition let A be Interval; let x be real number; cluster x + A -> interval; end; theorem :: MEASURE6:67 for A being Interval holds for x being real number holds vol(A) = vol(x + A);

Back to top