Copyright (c) 2003 Association of Mizar Users
environ
vocabulary BOOLE, ARYTM_1, PRE_TOPC, COMPTS_1, SEQ_1, RELAT_2, BORSUK_1,
SUBSET_1, RCOMP_1, TOPMETR, CONNSP_1, ARYTM_3, SQUARE_1, RELAT_1,
ORDINAL2, LATTICES, SEQ_2, INTEGRA1, FUNCT_1, TREAL_1, ARYTM, LIMFUNC1,
BORSUK_2, PCOMPS_1, GRAPH_1, INCPROJ, CARD_1, SETFAM_1, RAT_1, METRIC_1,
FINSET_1, ABSVALUE, IRRAT_1, POWER, INT_1, BORSUK_5, XREAL_0;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, ENUMSET1, SQUARE_1, RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, INT_1,
PRE_TOPC, COMPTS_1, RCOMP_1, SEQ_4, TREAL_1, RCOMP_2, CONNSP_1, BORSUK_2,
CARD_1, TOPMETR, PSCOMP_1, INTEGRA1, LIMFUNC1, IRRAT_1, FINSET_1,
ABSVALUE, INCPROJ, RAT_1, METRIC_1, PCOMPS_1, NECKLACE;
constructors TOPS_2, CONNSP_1, RCOMP_2, PSCOMP_1, INTEGRA1, BORSUK_3,
COMPTS_1, YELLOW_8, PARTFUN1, LIMFUNC1, TREAL_1, POWER, PROB_1, BORSUK_2,
ENUMSET1, NAT_1, INCPROJ, URYSOHN1, RAT_1, NECKLACE, MEMBERED;
clusters XREAL_0, RELSET_1, TOPREAL6, STRUCT_0, PRE_TOPC, BORSUK_2, INTEGRA1,
YELLOW13, TOPS_1, JORDAN6, BORSUK_4, FINSET_1, RAT_1, METRIC_1, INT_1,
MEMBERED, ZFMISC_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions XBOOLE_0, TARSKI;
theorems TOPS_2, BORSUK_1, RCOMP_2, PRE_TOPC, COMPTS_1, TARSKI, TOPREAL5,
TOPMETR, RCOMP_1, CONNSP_1, ZFMISC_1, JORDAN5A, AXIOMS, XREAL_0,
SQUARE_1, REAL_1, TOPREAL6, TREAL_1, XBOOLE_0, XBOOLE_1, JORDAN6, SEQ_4,
JGRAPH_5, INTEGRA1, FUNCT_2, FUNCT_1, TOPS_1, XCMPLX_0, BORSUK_4,
LIMFUNC1, PROB_1, BORSUK_2, MEASURE1, ENUMSET1, RAT_1, METRIC_1,
HAUSDORF, ABSVALUE, XCMPLX_1, TOPREAL3, INCPROJ, CARD_2, NECKLACE,
REAL_2, INT_1, YELLOW_8, FCONT_3, SETWISEO, IRRAT_1;
begin :: Preliminaries
canceled;
theorem Th2:
for A, B, a being set st
A c= B & B c= A \/ {a} holds
A \/ {a} = B or A = B
proof
let A, B, a be set;
assume
A1: A c= B & B c= A \/ {a};
assume A \/ {a} <> B & A <> B;
then A2: not A \/ {a} c= B & not B c= A by A1,XBOOLE_0:def 10;
not a in B
proof
assume a in B;
then {a} c= B by ZFMISC_1:37;
hence thesis by A1,A2,XBOOLE_1:8;
end;
hence thesis by A1,A2,SETWISEO:5;
end;
theorem
for x1, x2, x3, x4, x5, x6 being set holds
{ x1, x2, x3, x4, x5, x6 } = { x1, x3, x6 } \/ { x2, x4, x5 }
proof
let x1, x2, x3, x4, x5, x6 be set;
thus { x1, x2, x3, x4, x5, x6 } c= { x1, x3, x6 } \/ { x2, x4, x5 }
proof
let x be set;
assume x in { x1, x2, x3, x4, x5, x6 };
then x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6
by ENUMSET1:28;
then x in { x1, x3, x6 } or x in { x2, x4, x5 } by ENUMSET1:14;
hence thesis by XBOOLE_0:def 2;
end;
let x be set;
assume x in { x1, x3, x6 } \/ { x2, x4, x5 };
then x in { x1, x3, x6 } or x in { x2, x4, x5 } by XBOOLE_0:def 2;
then x = x1 or x = x3 or x = x6 or x = x2 or x = x4 or x = x5
by ENUMSET1:13;
hence thesis by ENUMSET1:29;
end;
reserve x1, x2, x3, x4, x5, x6, x7 for set;
definition let x1, x2, x3, x4, x5, x6 be set;
pred x1, x2, x3, x4, x5, x6 are_mutually_different means :Def1:
x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 &
x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 &
x3 <> x4 & x3 <> x5 & x3 <> x6 &
x4 <> x5 & x4 <> x6 &
x5 <> x6;
end;
definition let x1, x2, x3, x4, x5, x6, x7 be set;
pred x1, x2, x3, x4, x5, x6, x7 are_mutually_different means :Def2:
x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x1 <> x7 &
x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x2 <> x7 &
x3 <> x4 & x3 <> x5 & x3 <> x6 & x3 <> x7 &
x4 <> x5 & x4 <> x6 & x4 <> x7 &
x5 <> x6 & x5 <> x7 &
x6 <> x7;
end;
theorem Th4:
for x1, x2, x3, x4, x5, x6 being set st
x1, x2, x3, x4, x5, x6 are_mutually_different holds
card {x1, x2, x3, x4, x5, x6} = 6
proof
let x1, x2, x3, x4, x5, x6 be set;
assume x1, x2, x3, x4, x5, x6 are_mutually_different;
then A1: x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 &
x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 &
x3 <> x4 & x3 <> x5 & x3 <> x6 &
x4 <> x5 & x4 <> x6 &
x5 <> x6 by Def1;
then x1, x2, x3, x4, x5 are_mutually_different by NECKLACE:def 1;
then A2: card {x1,x2,x3,x4,x5} = 5 by NECKLACE:1;
not x6 in {x1,x2,x3,x4,x5} & {x1,x2,x3,x4,x5} is finite &
{x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5} \/ {x6} by A1,ENUMSET1:23,55;
hence card {x1,x2,x3,x4,x5,x6} = 5+1 by A2,CARD_2:54 .= 6;
end;
theorem
for x1, x2, x3, x4, x5, x6, x7 being set st
x1, x2, x3, x4, x5, x6, x7 are_mutually_different holds
card {x1, x2, x3, x4, x5, x6, x7} = 7
proof
let x1, x2, x3, x4, x5, x6, x7 be set;
assume x1, x2, x3, x4, x5, x6, x7 are_mutually_different;
then A1: x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x1 <> x7 &
x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x2 <> x7 &
x3 <> x4 & x3 <> x5 & x3 <> x6 & x3 <> x7 &
x4 <> x5 & x4 <> x6 & x4 <> x7 &
x5 <> x6 & x5 <> x7 &
x6 <> x7 by Def2;
then x1, x2, x3, x4, x5, x6 are_mutually_different by Def1;
then A2: card {x1,x2,x3,x4,x5,x6} = 6 by Th4;
not x7 in {x1,x2,x3,x4,x5,x6} & {x1,x2,x3,x4,x5,x6} is finite &
{x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5,x6} \/ {x7}
by A1,ENUMSET1:28,61;
hence card {x1,x2,x3,x4,x5,x6,x7} = 6+1 by A2,CARD_2:54 .= 7;
end;
theorem Th6:
{ x1, x2, x3 } misses { x4, x5, x6 } implies
x1 <> x4 & x1 <> x5 & x1 <> x6 &
x2 <> x4 & x2 <> x5 & x2 <> x6 &
x3 <> x4 & x3 <> x5 & x3 <> x6
proof
assume
A1: { x1, x2, x3 } misses { x4, x5, x6 };
assume x1 = x4 or x1 = x5 or x1 = x6 or
x2 = x4 or x2 = x5 or x2 = x6 or
x3 = x4 or x3 = x5 or x3 = x6;
then A2: x4 in { x1, x2, x3 } or x5 in { x1, x2, x3 } or x6 in { x1, x2, x3 }
by ENUMSET1:14;
x4 in { x4, x5, x6 } & x5 in { x4, x5, x6 } & x6 in { x4, x5, x6 }
by ENUMSET1:14;
hence thesis by A1,A2,XBOOLE_0:3;
end;
theorem
x1, x2, x3 are_mutually_different &
x4, x5, x6 are_mutually_different &
{ x1, x2, x3 } misses { x4, x5, x6 } implies
x1, x2, x3, x4, x5, x6 are_mutually_different
proof
assume that
A1: x1, x2, x3 are_mutually_different and
A2: x4, x5, x6 are_mutually_different and
A3: { x1, x2, x3 } misses { x4, x5, x6 };
A4: x1 <> x2 & x2 <> x3 & x1 <> x3 by A1,INCPROJ:def 5;
A5: x4 <> x5 & x5 <> x6 & x4 <> x6 by A2,INCPROJ:def 5;
x1 <> x4 & x1 <> x5 & x1 <> x6 &
x2 <> x4 & x2 <> x5 & x2 <> x6 &
x3 <> x4 & x3 <> x5 & x3 <> x6 by A3,Th6;
hence thesis by A4,A5,Def1;
end;
theorem
x1, x2, x3, x4, x5, x6 are_mutually_different &
{ x1, x2, x3, x4, x5, x6 } misses { x7 } implies
x1, x2, x3, x4, x5, x6, x7 are_mutually_different
proof
assume that
A1: x1, x2, x3, x4, x5, x6 are_mutually_different and
A2: { x1, x2, x3, x4, x5, x6 } misses { x7 };
A3: x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 &
x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 &
x3 <> x4 & x3 <> x5 & x3 <> x6 &
x4 <> x5 & x4 <> x6 & x5 <> x6 by A1,Def1;
not x7 in { x1, x2, x3, x4, x5, x6 } by A2,ZFMISC_1:54;
then x7 <> x1 & x7 <> x2 & x7 <> x3 & x7 <> x4 & x7 <> x5 & x7 <> x6
by ENUMSET1:29;
hence thesis by A3,Def2;
end;
theorem
x1, x2, x3, x4, x5, x6, x7 are_mutually_different implies
x7, x1, x2, x3, x4, x5, x6 are_mutually_different
proof
assume x1, x2, x3, x4, x5, x6, x7 are_mutually_different;
then x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x1 <> x7 &
x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x2 <> x7 &
x3 <> x4 & x3 <> x5 & x3 <> x6 & x3 <> x7 &
x4 <> x5 & x4 <> x6 & x4 <> x7 &
x5 <> x6 & x5 <> x7 & x6 <> x7 by Def2;
hence thesis by Def2;
end;
theorem
x1, x2, x3, x4, x5, x6, x7 are_mutually_different implies
x1, x2, x5, x3, x6, x7, x4 are_mutually_different
proof
assume x1, x2, x3, x4, x5, x6, x7 are_mutually_different;
then x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x1 <> x7 &
x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x2 <> x7 &
x3 <> x4 & x3 <> x5 & x3 <> x6 & x3 <> x7 &
x4 <> x5 & x4 <> x6 & x4 <> x7 &
x5 <> x6 & x5 <> x7 &
x6 <> x7 by Def2;
hence thesis by Def2;
end;
theorem Th11:
for T being non empty TopSpace,
a, b being Point of T st
(ex f being map of I[01], T st f is continuous & f.0 = a & f.1 = b) holds
ex g being map of I[01], T st g is continuous & g.0 = b & g.1 = a
proof
let T be non empty TopSpace,
a, b be Point of T;
given P being map of I[01], T such that
A1: P is continuous & P.0 = a & P.1 = b;
set e = L[01]((0,1)(#),(#)(0,1));
A2: e.0 = e.(#)(0,1) by TREAL_1:def 1
.= (0,1)(#) by TREAL_1:12
.= 1 by TREAL_1:def 2;
A3: e.1 = e.(0,1)(#) by TREAL_1:def 2
.= (#)(0,1) by TREAL_1:12
.= 0 by TREAL_1:def 1;
set f = P * e;
f is Function of the carrier of Closed-Interval-TSpace (0,1),
the carrier of T by FUNCT_2:19,TOPMETR:27;
then reconsider f as map of I[01], T by TOPMETR:27;
0 in [. 0,1 .] by TOPREAL5:1;
then 0 in the carrier of Closed-Interval-TSpace (0,1) by TOPMETR:25;
then A4: 0 in dom e by FUNCT_2:def 1;
1 in [. 0,1 .] by TOPREAL5:1;
then 1 in the carrier of Closed-Interval-TSpace (0,1) by TOPMETR:25;
then A5: 1 in dom e by FUNCT_2:def 1;
take f;
e is continuous map of
Closed-Interval-TSpace(0,1),Closed-Interval-TSpace(0,1) by TREAL_1:11;
hence f is continuous by A1,TOPMETR:27,TOPS_2:58;
thus thesis by A1,A2,A3,A4,A5,FUNCT_1:23;
end;
Lm1: R^1 is arcwise_connected
proof
for a, b being Point of R^1 ex f being map of I[01], R^1 st
f is continuous & f.0 = a & f.1 = b
proof
let a, b be Point of R^1;
per cases;
suppose
A1: a <= b;
reconsider B = [. a, b .] as Subset of R^1
by TOPMETR:24;
reconsider B as non empty Subset of R^1 by A1,TOPREAL5:1;
A2: Closed-Interval-TSpace(a,b) = R^1|B by A1,TOPMETR:26;
then A3: L[01]((#)(a,b),(a,b)(#)) is continuous map of
I[01], R^1|B by A1,TOPMETR:27,TREAL_1:11;
the carrier of R^1|B c= the carrier of R^1 by BORSUK_1:35;
then reconsider g = L[01]((#)(a,b),(a,b)(#)) as Function of
the carrier of I[01], the carrier of R^1
by A2,FUNCT_2:9,TOPMETR:27;
reconsider g as map of I[01], R^1;
take g;
thus g is continuous by A3,TOPMETR:7;
0 = (#)(0,1) by TREAL_1:def 1;
hence g.0 = (#)(a,b) by A1,TREAL_1:12 .= a by A1,TREAL_1:def 1;
1 = (0,1)(#) by TREAL_1:def 2;
hence g.1 = (a,b)(#) by A1,TREAL_1:12 .= b by A1,TREAL_1:def 2;
suppose
A4: b <= a;
reconsider B = [. b, a .] as Subset of R^1
by TOPMETR:24;
b in B by A4,TOPREAL5:1;
then reconsider B = [. b, a .] as non empty Subset of R^1;
A5: Closed-Interval-TSpace(b,a) = R^1|B by A4,TOPMETR:26;
then A6: L[01]((#)(b,a),(b,a)(#)) is continuous map of
I[01], R^1|B by A4,TOPMETR:27,TREAL_1:11;
the carrier of R^1|B c= the carrier of R^1 by BORSUK_1:35;
then reconsider g = L[01]((#)(b,a),(b,a)(#)) as Function of
the carrier of I[01], the carrier of R^1
by A5,FUNCT_2:9,TOPMETR:27;
reconsider g as map of I[01], R^1;
A7: g is continuous by A6,TOPMETR:7;
0 = (#)(0,1) by TREAL_1:def 1;
then A8: g.0 = (#)(b,a) by A4,TREAL_1:12 .= b by A4,TREAL_1:def 1;
1 = (0,1)(#) by TREAL_1:def 2;
then A9: g.1 = (b,a)(#) by A4,TREAL_1:12 .= a by A4,TREAL_1:def 2;
then reconsider P = g as Path of b, a by A7,A8,BORSUK_2:def 1;
take h = -P;
ex t being map of I[01], R^1 st
t is continuous & t.0 = a & t.1 = b by A7,A8,A9,Th11;
hence thesis by BORSUK_2:def 1;
end;
hence thesis by BORSUK_2:def 2;
end;
definition
cluster R^1 -> arcwise_connected;
coherence by Lm1;
end;
definition
cluster connected non empty TopSpace;
existence
proof
take R^1;
thus thesis;
end;
end;
begin :: Intervals
theorem
for A being Subset of REAL holds
A is Subset of R^1 by TOPMETR:24;
theorem Th13:
[#]R^1 = REAL by PRE_TOPC:def 3,TOPMETR:24;
Lm2:
for A being Subset of REAL, B being Subset of R^1 st
A = B holds Cl A = Cl B by TOPREAL6:80;
definition let a be real number;
redefine func left_closed_halfline a; :: LIMFUNC1
synonym ].-infty, a .];
redefine func left_open_halfline a;
synonym ].-infty, a .[;
redefine func right_closed_halfline a;
synonym [. a,+infty.[;
redefine func right_open_halfline a;
synonym ]. a,+infty.[;
end;
theorem Th14:
for a, b being real number holds
a in ]. b,+infty.[ iff a > b
proof
let a, b be real number;
A1: a is Element of REAL by XREAL_0:def 1;
hereby assume a in ]. b,+infty.[;
then a in { g where g is Element of REAL : b < g } by LIMFUNC1:def 3;
then consider h being Element of REAL such that
A2: h = a & b < h;
thus b < a by A2;
end;
assume b < a;
then a in { g where g is Element of REAL : b < g } by A1;
hence thesis by LIMFUNC1:def 3;
end;
theorem Th15:
for a, b being real number holds
a in [. b,+infty.[ iff a >= b
proof
let a, b be real number;
A1: a is Element of REAL by XREAL_0:def 1;
hereby assume a in [. b,+infty.[;
then a in { g where g is Element of REAL : b <= g } by LIMFUNC1:def 2;
then consider h being Element of REAL such that
A2: h = a & b <= h;
thus b <= a by A2;
end;
assume b <= a;
then a in { g where g is Element of REAL : b <= g } by A1;
hence thesis by LIMFUNC1:def 2;
end;
theorem Th16:
for a, b being real number holds
a in ].-infty, b .] iff a <= b
proof
let a, b be real number;
A1: a is Element of REAL by XREAL_0:def 1;
hereby assume a in ].-infty,b .];
then a in { g where g is Element of REAL : g <= b } by LIMFUNC1:def 1;
then consider h being Element of REAL such that
A2: h = a & b >= h;
thus b >= a by A2;
end;
assume b >= a;
then a in { g where g is Element of REAL : b >= g } by A1;
hence thesis by LIMFUNC1:def 1;
end;
theorem Th17:
for a, b being real number holds
a in ].-infty, b .[ iff a < b
proof
let a, b be real number;
A1: a is Element of REAL by XREAL_0:def 1;
hereby assume a in ].-infty,b .[;
then a in { g where g is Element of REAL : g < b } by PROB_1:def 15;
then consider h being Element of REAL such that
A2: h = a & b > h;
thus b > a by A2;
end;
assume a < b;
then a in { g where g is Element of REAL : b > g } by A1;
hence thesis by PROB_1:def 15;
end;
theorem Th18:
for a being real number holds
REAL \ {a} = ].-infty, a .[ \/ ]. a,+infty.[
proof
let a be real number;
A1: a is Real by XREAL_0:def 1;
[. a,a .] = {a} by RCOMP_1:14;
hence thesis by A1,LIMFUNC1:25;
end;
theorem Th19:
for a, b, c, d being real number st a < b & b <= c holds
[. a, b .] misses ]. c, d .]
proof
let a, b, c, d be real number;
assume
A1: a < b & b <= c;
assume [. a, b .] meets ]. c, d .];
then consider x being set such that
A2: x in [. a, b .] & x in ]. c, d .] by XBOOLE_0:3;
reconsider x as real number by A2,XREAL_0:def 1;
x <= b & x > c by A2,RCOMP_2:4,TOPREAL5:1;
hence thesis by A1,AXIOMS:22;
end;
theorem Th20:
for a, b, c, d being real number st a < b & b <= c holds
[. a, b .[ misses [. c, d .]
proof
let a, b, c, d be real number;
assume
A1: a < b & b <= c;
assume [. a, b .[ meets [. c, d .];
then consider x being set such that
A2: x in [. a, b .[ & x in [. c, d .] by XBOOLE_0:3;
reconsider x as real number by A2,XREAL_0:def 1;
x < b & x >= c by A2,RCOMP_2:3,TOPREAL5:1;
hence thesis by A1,AXIOMS:22;
end;
theorem
for A, B being Subset of R^1,
a, b, c, d being real number st a < b & b <= c & c < d &
A = [. a, b .[ & B = ]. c, d .] holds
A, B are_separated
proof
let A, B be Subset of R^1,
a, b, c, d be real number;
assume that
A1: a < b & b <= c & c < d and
A2: A = [. a, b .[ and
A3: B = ]. c, d .];
Cl [. a, b .[ = [. a, b .] by A1,BORSUK_4:21;
then Cl A = [. a, b .] by A2,Lm2;
then A4: Cl A misses B by A1,A3,Th19;
Cl ]. c, d .] = [. c, d .] by A1,BORSUK_4:20;
then Cl B = [. c, d .] by A3,Lm2;
then Cl B misses A by A1,A2,Th20;
hence thesis by A4,CONNSP_1:def 1;
end;
theorem Th22:
for a being real number holds
REAL \ ].-infty, a .[ = [. a,+infty.[
proof
let a be real number;
a is Real by XREAL_0:def 1;
hence thesis by LIMFUNC1:24;
end;
theorem Th23:
for a being real number holds
REAL \ ].-infty, a .] = ]. a,+infty.[
proof
let a be real number;
a is Real by XREAL_0:def 1;
hence thesis by LIMFUNC1:24;
end;
theorem
for a being real number holds
REAL \ ]. a,+infty.[ = ].-infty, a .]
proof
let a be real number;
a is Real by XREAL_0:def 1;
hence thesis by LIMFUNC1:24;
end;
theorem Th25:
for a being real number holds
REAL \ [. a,+infty.[ = ].-infty, a .[
proof
let a be real number;
a is Real by XREAL_0:def 1;
hence thesis by LIMFUNC1:24;
end;
theorem Th26:
for a being real number holds
].-infty, a .] misses ]. a,+infty.[
proof
let a be real number;
REAL \ ].-infty, a .] = ]. a,+infty.[ by Th23;
hence thesis by XBOOLE_1:79;
end;
theorem Th27:
for a being real number holds
].-infty, a .[ misses [. a,+infty.[
proof
let a be real number;
REAL \ ].-infty, a .[ = [. a,+infty.[ by Th22;
hence thesis by XBOOLE_1:79;
end;
theorem Th28:
for a, b, c being real number st
a <= c & c <= b holds [.a,b.] \/ [.c,+infty.[ = [.a,+infty.[
proof
let a, b, c be real number;
assume
A1: a <= c & c <= b;
A2: [.a,+infty.[ c= [.a,b.] \/ [.c,+infty.[
proof
let r be set;
assume
A3: r in [.a,+infty.[;
then reconsider s = r as Real;
A4: a <= s by A3,Th15;
per cases;
suppose s <= b;
then s in [.a,b.] by A4,TOPREAL5:1;
hence thesis by XBOOLE_0:def 2;
suppose not s <= b;
then c <= s by A1,AXIOMS:22;
then s in [.c,+infty.[ by Th15;
hence thesis by XBOOLE_0:def 2;
end;
A5: a is Real by XREAL_0:def 1;
A6: b is Real by XREAL_0:def 1;
A7: c is Real by XREAL_0:def 1;
[.a,b.] \/ [.c,+infty.[ c= [.a,+infty.[
proof
A8: [.a,b.] c= [.a,+infty.[ by A5,A6,LIMFUNC1:12;
[.c,+infty.[ c= [.a,+infty.[ by A1,A5,A7,LIMFUNC1:9;
hence thesis by A8,XBOOLE_1:8;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
theorem Th29:
for a, b, c being real number st
a <= c & c <= b holds ].-infty, c .] \/ [. a, b .] = ].-infty, b .]
proof
let a, b, c be real number;
assume
A1: a <= c & c <= b;
thus ].-infty, c .] \/ [. a, b .] c= ].-infty, b .]
proof
let x be set;
assume
A2: x in ].-infty, c .] \/ [. a, b .];
then reconsider x as real number by XREAL_0:def 1;
per cases by A2,XBOOLE_0:def 2;
suppose x in ].-infty, c .];
then x <= c by Th16;
then x <= b by A1,AXIOMS:22;
hence thesis by Th16;
suppose x in [. a, b .];
then x <= b by TOPREAL5:1;
hence thesis by Th16;
end;
let x be set;
assume
A3: x in ].-infty, b .];
then reconsider x as real number by XREAL_0:def 1;
per cases;
suppose x <= c;
then x in ].-infty, c .] by Th16;
hence thesis by XBOOLE_0:def 2;
suppose x > c;
then A4: x > a by A1,AXIOMS:22;
x <= b by A3,Th16;
then x in [. a, b .] by A4,TOPREAL5:1;
hence thesis by XBOOLE_0:def 2;
end;
theorem Th30:
for T being 1-sorted,
A being Subset of T holds
{ A } is Subset-Family of T by MEASURE1:6;
theorem
for T being 1-sorted,
A, B being Subset of T holds
{ A, B } is Subset-Family of T by MEASURE1:7;
theorem
for T being 1-sorted,
A, B, C being Subset of T holds
{ A, B, C } is Subset-Family of T by MEASURE1:8;
definition
cluster -> real Element of RAT;
coherence;
end;
definition
cluster -> real Element of RealSpace;
coherence by METRIC_1:def 14,XREAL_0:def 1;
end;
theorem Th33:
for A being Subset of R^1,
p being Point of RealSpace holds
p in Cl A iff
for r being real number st r > 0 holds Ball (p, r) meets A
by HAUSDORF:7,TOPMETR:def 7;
theorem Th34:
for p, q being Element of RealSpace st q >= p holds
dist (p, q) = q - p
proof
let p, q be Element of RealSpace;
assume p <= q;
then A1: q - p >= 0 by SQUARE_1:12;
dist (p, q) = abs (q - p) by TOPMETR:15
.= q - p by A1,ABSVALUE:def 1;
hence thesis;
end;
Lm3: for r being real number holds r is Element of RealSpace by METRIC_1:def 14
,XREAL_0:def 1;
theorem Th35:
for A being Subset of R^1 st A = RAT holds
Cl A = the carrier of R^1
proof
let A be Subset of R^1;
assume
A1: A = RAT;
Cl A = the carrier of R^1
proof
thus Cl A c= the carrier of R^1;
thus the carrier of R^1 c= Cl A
proof
let x be set;
assume x in the carrier of R^1;
then reconsider p = x as Element of RealSpace
by METRIC_1:def 14,TOPMETR:24;
now let r be real number;
assume
A2: r > 0;
reconsider pr = p + r as Element of RealSpace by Lm3;
p < pr by A2,REAL_1:69;
then consider Q being rational number such that
A3: p < Q & Q < pr by RAT_1:22;
A4: Q in A by A1,RAT_1:def 2;
reconsider P = Q as Element of RealSpace by Lm3;
P - p < pr - p by A3,REAL_1:54;
then P - p < r by XCMPLX_1:26;
then dist (p, P) < r by A3,Th34;
then P in Ball (p, r) by METRIC_1:12;
hence Ball (p, r) meets A by A4,XBOOLE_0:3;
end;
hence thesis by Th33;
end;
end;
hence thesis;
end;
theorem Th36:
for A being Subset of R^1,
a, b being real number st
A = ]. a, b .[ & a <> b holds
Cl A = [. a, b .]
proof
let A be Subset of R^1,
a, b be real number;
assume
A1: A = ]. a, b .[ & a <> b;
then Cl ]. a, b .[ = [. a, b .] by TOPREAL6:82;
hence thesis by A1,Lm2;
end;
begin :: Rational and Irrational Numbers
definition
cluster number_e -> irrational;
coherence by IRRAT_1:42;
end;
definition
func IRRAT -> Subset of REAL equals :Def3:
REAL \ RAT;
coherence by XBOOLE_1:36;
end;
definition let a, b be real number;
func RAT (a, b) -> Subset of REAL equals :Def4:
RAT /\ ]. a, b .[;
coherence
proof
RAT /\ ]. a, b .[ c= ]. a, b .[ by XBOOLE_1:17;
hence thesis by XBOOLE_1:1;
end;
func IRRAT (a, b) -> Subset of REAL equals :Def5:
IRRAT /\ ]. a, b .[;
coherence;
end;
theorem Th37:
for x being real number holds
x is irrational iff x in IRRAT
proof
let x be real number;
A1: x in REAL by XREAL_0:def 1;
hereby assume x is irrational;
then not x in RAT by RAT_1:def 2;
hence x in IRRAT by A1,Def3,XBOOLE_0:def 4;
end;
assume x in IRRAT;
then not x in RAT by Def3,XBOOLE_0:def 4;
hence thesis by RAT_1:def 2;
end;
definition
cluster irrational (real number);
existence by IRRAT_1:42;
end;
definition
cluster IRRAT -> non empty;
coherence by Th37,IRRAT_1:42;
end;
theorem Th38:
for a being rational number, b being irrational (real number) holds
a + b is irrational
proof
let a be rational number, b be irrational (real number);
assume a + b is rational;
then consider m, n being Integer such that
A1: n <> 0 & a + b = m / n by RAT_1:3;
consider m1, n1 being Integer such that
A2: n1 <> 0 & a = m1 / n1 by RAT_1:3;
A3: a + b - a = b by XCMPLX_1:26;
a + b - a = (m*n1 - m1*n) / (n1*n) by A1,A2,XCMPLX_1:131;
then b in RAT by A3;
hence thesis by RAT_1:def 2;
end;
theorem Th39:
for a being irrational (real number) holds -a is irrational
proof
let a be irrational (real number);
assume -a is rational;
then reconsider b = -a as rational number;
-b is rational;
hence thesis;
end;
theorem Th40:
for a being rational number, b being irrational (real number) holds
a - b is irrational
proof
let a be rational number, b be irrational (real number);
-b is irrational by Th39;
then a + -b is irrational by Th38;
hence thesis by XCMPLX_0:def 8;
end;
theorem Th41:
for a being rational number, b being irrational (real number) holds
b - a is irrational
proof
let a be rational number, b be irrational (real number);
b + -a is irrational by Th38;
hence thesis by XCMPLX_0:def 8;
end;
theorem Th42:
for a being rational number, b being irrational (real number) st
a <> 0 holds a * b is irrational
proof
let a be rational number, b be irrational (real number);
assume
A1: a <> 0;
assume a * b is rational;
then consider m, n being Integer such that
A2: n <> 0 & a * b = m / n by RAT_1:3;
consider m1, n1 being Integer such that
A3: n1 <> 0 & a = m1 / n1 by RAT_1:3;
A4: a * b / a = b by A1,XCMPLX_1:90;
a * b / a = (m * n1) / (n * m1) by A2,A3,XCMPLX_1:85;
then b in RAT by A4;
hence thesis by RAT_1:def 2;
end;
theorem Th43:
for a being rational number, b being irrational (real number)
st a <> 0 holds b / a is irrational
proof
let a be rational number, b be irrational (real number);
assume
A1: a <> 0;
assume b / a is rational;
then reconsider c = b / a as rational number;
c * a is rational;
hence thesis by A1,XCMPLX_1:88;
end;
definition
cluster irrational -> non zero (real number);
coherence
proof
let a be real number;
assume
A1: a is irrational;
assume a is zero;
then a = 0 / 1;
hence thesis by A1;
end;
end;
theorem Th44:
for a being rational number, b being irrational (real number)
st a <> 0 holds a / b is irrational
proof
let a be rational number, b be irrational (real number);
assume
A1: a <> 0;
assume a / b is rational;
then reconsider c = a / b as rational number;
b <> 0 & c <> 0 by A1,XCMPLX_1:50;
then c * b is irrational by Th42;
hence thesis by XCMPLX_1:88;
end;
theorem Th45:
for r being irrational (real number) holds frac r is irrational
proof
let r be irrational (real number);
frac r = r - [\ r /] by INT_1:def 6;
hence thesis by Th41;
end;
definition let r be irrational (real number);
cluster frac r -> irrational;
coherence by Th45;
end;
definition let a be irrational (real number);
cluster -a -> irrational;
coherence by Th39;
end;
definition let a be rational number, b be irrational (real number);
cluster a + b -> irrational;
coherence by Th38;
cluster b + a -> irrational;
coherence by Th38;
cluster a - b -> irrational;
coherence by Th40;
cluster b - a -> irrational;
coherence by Th41;
end;
definition
cluster non zero (rational number);
existence
proof
reconsider a = 1 as rational number;
a <> 0;
hence thesis;
end;
end;
definition let a be non zero (rational number), b be irrational (real number);
cluster a * b -> irrational;
coherence by Th42;
cluster b * a -> irrational;
coherence by Th42;
cluster a / b -> irrational;
coherence by Th44;
cluster b / a -> irrational;
coherence by Th43;
end;
theorem
for r being irrational (real number) holds 0 < frac r by INT_1:69;
theorem Th47:
for a, b being real number st a < b
ex p1, p2 being rational number st
a < p1 & p1 < p2 & p2 < b
proof
let a, b be real number;
assume a < b;
then consider p1 being rational number such that
A1: a < p1 & p1 < b by RAT_1:22;
consider p2 being rational number such that
A2: p1 < p2 & p2 < b by A1,RAT_1:22;
thus thesis by A1,A2;
end;
Lm4:
for p1, p2, x being real number holds
(1 - x) * p1 + x * p2 = p1 + x * (p2 - p1)
proof
let p1, p2, x be real number;
thus (1 - x) * p1 + x * p2 = 1 * p1 - x * p1 + x * p2 by XCMPLX_1:40
.= 1 * p1 + - x * p1 + x * p2 by XCMPLX_0:def 8
.= 1 * p1 + (- x * p1 + x * p2) by XCMPLX_1:1
.= 1 * p1 + (x * p2 - x * p1) by XCMPLX_0:def 8
.= p1 + x * (p2 - p1) by XCMPLX_1:40;
end;
theorem Th48:
for s1, s3, s4, l being real number holds
s1 <= s3 & s1 < s4 & 0 < l & l < 1 implies s1 < (1-l)*s3+l*s4
proof
let s1, s3, s4, l be real number;
assume
A1: s1 <= s3 & s1 < s4 & 0 < l & l < 1;
then A2: l*s1 < l*s4 by REAL_1:70;
1-l > 0 by A1,SQUARE_1:11;
then A3: (1-l)*s1 <= (1-l)*s3 by A1,AXIOMS:25;
(1-l)*s1+l*s1 = (1-l+l)*s1 by XCMPLX_1:8
.= 1 * s1 by XCMPLX_1:27
.= s1;
hence thesis by A2,A3,REAL_1:67;
end;
theorem Th49:
for s1, s3, s4, l being real number holds
s3 < s1 & s4 <= s1 & 0 < l & l < 1 implies (1-l)*s3+l*s4 < s1
proof
let s1, s3, s4, l be real number;
assume
A1: s1 > s3 & s1 >= s4 & 0 < l & l < 1;
then A2: l*s1 >= l*s4 by AXIOMS:25;
1-l > 0 by A1,SQUARE_1:11;
then A3: (1-l)*s1 > (1-l)*s3 by A1,REAL_1:70;
(1-l)*s1+l*s1 = (1-l+l)*s1 by XCMPLX_1:8
.= 1 * s1 by XCMPLX_1:27
.= s1;
hence thesis by A2,A3,REAL_1:67;
end;
theorem Th50:
for a, b being real number st a < b
ex p being irrational (real number) st a < p & p < b
proof
let a, b be real number;
assume a < b;
then consider p1, p2 being rational number such that
A1: a < p1 & p1 < p2 & p2 < b by Th47;
A2: p2 - p1 <> 0 by A1,XCMPLX_1:15;
set x = frac number_e;
set y = (1 - x) * p1 + x * p2;
A3: y = p1 + x * (p2 - p1) by Lm4;
x * (p2 - p1) is irrational by A2,Th42;
then A4: y is irrational by A3,Th38;
A5: 0 < x & x < 1 by INT_1:69;
then y < p2 by A1,Th49;
then A6: y < b by A1,AXIOMS:22;
y > p1 by A1,A5,Th48;
then y > a by A1,AXIOMS:22;
hence thesis by A4,A6;
end;
theorem Th51:
for A being Subset of R^1 st A = IRRAT holds
Cl A = the carrier of R^1
proof
let A be Subset of R^1;
assume
A1: A = IRRAT;
Cl A = the carrier of R^1
proof
thus Cl A c= the carrier of R^1;
thus the carrier of R^1 c= Cl A
proof
let x be set;
assume x in the carrier of R^1;
then reconsider p = x as Element of RealSpace
by METRIC_1:def 14,TOPMETR:24;
now let r be real number;
assume
A2: r > 0;
reconsider pr = p + r as Element of RealSpace by Lm3;
p < pr by A2,REAL_1:69;
then consider Q being irrational (real number) such that
A3: p < Q & Q < pr by Th50;
A4: Q in A by A1,Th37;
reconsider P = Q as Element of RealSpace by Lm3;
P - p < pr - p by A3,REAL_1:54;
then P - p < r by XCMPLX_1:26;
then dist (p, P) < r by A3,Th34;
then P in Ball (p, r) by METRIC_1:12;
hence Ball (p, r) meets A by A4,XBOOLE_0:3;
end;
hence thesis by Th33;
end;
end;
hence thesis;
end;
Lm5:
for A being Subset of R^1,
a, b being real number st a < b & A = RAT (a, b) holds
a in Cl A & b in Cl A
proof
let A be Subset of R^1,
a, b be real number;
assume that
A1: a < b and
A2: A = RAT (a, b);
thus a in Cl A
proof
reconsider a' = a as Element of RealSpace by Lm3;
for r being real number st r > 0 holds Ball (a', r) meets A
proof
let r be real number;
assume
A3: r > 0;
set p = a;
reconsider pp = a + r as Element of RealSpace by Lm3;
set pr = min (pp, (p + b)/2);
A4: pr <= (p + b)/2 by SQUARE_1:35;
A5: (p + b)/2 < b by A1,TOPREAL3:3;
p < pr
proof
per cases by SQUARE_1:38;
suppose pr = pp;
hence thesis by A3,REAL_1:69;
suppose pr = (p + b)/2;
hence thesis by A1,TOPREAL3:3;
end;
then consider Q being rational number such that
A6: p < Q & Q < pr by RAT_1:22;
A7: Q in RAT by RAT_1:def 2;
pr < b by A4,A5,AXIOMS:22;
then a < Q & Q < b by A6,AXIOMS:22;
then Q in ]. a, b .[ by JORDAN6:45;
then Q in RAT /\ ]. a, b .[ by A7,XBOOLE_0:def 3;
then A8: Q in A by A2,Def4;
reconsider P = Q as Element of RealSpace by Lm3;
A9: P - p < pr - p by A6,REAL_1:54;
pr - p <= r
proof
per cases by SQUARE_1:38;
suppose pr = pp;
hence thesis by XCMPLX_1:26;
suppose pr = (p + b)/2;
pr <= pp by SQUARE_1:35;
then pr - p <= pp - p by REAL_1:49;
hence thesis by XCMPLX_1:26;
end;
then P - p < r by A9,AXIOMS:22;
then dist (a', P) < r by A6,Th34;
then P in Ball (a', r) by METRIC_1:12;
hence thesis by A8,XBOOLE_0:3;
end;
hence thesis by Th33;
end;
b in Cl A
proof
reconsider a' = b as Element of RealSpace by Lm3;
for r being real number st r > 0 holds Ball (a', r) meets A
proof
let r be real number;
assume
A10: r > 0;
set p = b;
reconsider pp = b - r as Element of RealSpace by Lm3;
set pr = max (pp, (p + a)/2);
A11: b < b + r by A10,REAL_1:69;
A12: pr >= (p + a)/2 by SQUARE_1:46;
A13: (p + a)/2 > a by A1,TOPREAL3:3;
p > pr
proof
per cases by SQUARE_1:49;
suppose pr = pp;
hence thesis by A11,REAL_1:84;
suppose pr = (p + a)/2;
hence thesis by A1,TOPREAL3:3;
end;
then consider Q being rational number such that
A14: pr < Q & Q < p by RAT_1:22;
A15: Q in RAT by RAT_1:def 2;
a < pr by A12,A13,AXIOMS:22;
then a < Q & Q < b by A14,AXIOMS:22;
then Q in ]. a, b .[ by JORDAN6:45;
then Q in RAT /\ ]. a, b .[ by A15,XBOOLE_0:def 3;
then A16: Q in A by A2,Def4;
reconsider P = Q as Element of RealSpace by Lm3;
A17: p - P < p - pr by A14,REAL_2:105;
p - pr <= r
proof
per cases by SQUARE_1:49;
suppose pr = pp;
hence thesis by XCMPLX_1:18;
suppose pr = (p + a)/2;
pr >= pp by SQUARE_1:46;
then p - pr <= p - pp by REAL_1:92;
hence thesis by XCMPLX_1:18;
end;
then p - P < r by A17,AXIOMS:22;
then dist (a', P) < r by A14,Th34;
then P in Ball (a', r) by METRIC_1:12;
hence thesis by A16,XBOOLE_0:3;
end;
hence thesis by Th33;
end;
hence thesis;
end;
Lm6:
for A being Subset of R^1,
a, b being real number st a < b & A = IRRAT (a, b) holds
a in Cl A & b in Cl A
proof
let A be Subset of R^1,
a, b be real number;
assume that
A1: a < b and
A2: A = IRRAT (a, b);
thus a in Cl A
proof
reconsider a' = a as Element of RealSpace by Lm3;
for r being real number st r > 0 holds Ball (a', r) meets A
proof
let r be real number;
assume
A3: r > 0;
set p = a;
reconsider pp = a + r as Element of RealSpace by Lm3;
set pr = min (pp, (p + b)/2);
A4: pr <= (p + b)/2 by SQUARE_1:35;
A5: (p + b)/2 < b by A1,TOPREAL3:3;
p < pr
proof
per cases by SQUARE_1:38;
suppose pr = pp;
hence thesis by A3,REAL_1:69;
suppose pr = (p + b)/2;
hence thesis by A1,TOPREAL3:3;
end;
then consider Q being irrational (real number) such that
A6: p < Q & Q < pr by Th50;
A7: Q in IRRAT by Th37;
pr < b by A4,A5,AXIOMS:22;
then a < Q & Q < b by A6,AXIOMS:22;
then Q in ]. a, b .[ by JORDAN6:45;
then Q in IRRAT /\ ]. a, b .[ by A7,XBOOLE_0:def 3;
then A8: Q in A by A2,Def5;
reconsider P = Q as Element of RealSpace by Lm3;
A9: P - p < pr - p by A6,REAL_1:54;
pr - p <= r
proof
per cases by SQUARE_1:38;
suppose pr = pp;
hence thesis by XCMPLX_1:26;
suppose pr = (p + b)/2;
pr <= pp by SQUARE_1:35;
then pr - p <= pp - p by REAL_1:49;
hence thesis by XCMPLX_1:26;
end;
then P - p < r by A9,AXIOMS:22;
then dist (a', P) < r by A6,Th34;
then P in Ball (a', r) by METRIC_1:12;
hence thesis by A8,XBOOLE_0:3;
end;
hence thesis by Th33;
end;
b in Cl A
proof
reconsider a' = b as Element of RealSpace by Lm3;
for r being real number st r > 0 holds Ball (a', r) meets A
proof
let r be real number;
assume
A10: r > 0;
set p = b;
reconsider pp = b - r as Element of RealSpace by Lm3;
set pr = max (pp, (p + a)/2);
A11: b < b + r by A10,REAL_1:69;
A12: pr >= (p + a)/2 by SQUARE_1:46;
A13: (p + a)/2 > a by A1,TOPREAL3:3;
p > pr
proof
per cases by SQUARE_1:49;
suppose pr = pp;
hence thesis by A11,REAL_1:84;
suppose pr = (p + a)/2;
hence thesis by A1,TOPREAL3:3;
end;
then consider Q being irrational (real number) such that
A14: pr < Q & Q < p by Th50;
A15: Q in IRRAT by Th37;
a < pr by A12,A13,AXIOMS:22;
then a < Q & Q < b by A14,AXIOMS:22;
then Q in ]. a, b .[ by JORDAN6:45;
then Q in IRRAT /\ ]. a, b .[ by A15,XBOOLE_0:def 3;
then A16: Q in A by A2,Def5;
reconsider P = Q as Element of RealSpace by Lm3;
A17: p - P < p - pr by A14,REAL_2:105;
p - pr <= r
proof
per cases by SQUARE_1:49;
suppose pr = pp;
hence thesis by XCMPLX_1:18;
suppose pr = (p + a)/2;
pr >= pp by SQUARE_1:46;
then p - pr <= p - pp by REAL_1:92;
hence thesis by XCMPLX_1:18;
end;
then p - P < r by A17,AXIOMS:22;
then dist (a', P) < r by A14,Th34;
then P in Ball (a', r) by METRIC_1:12;
hence thesis by A16,XBOOLE_0:3;
end;
hence thesis by Th33;
end;
hence thesis;
end;
theorem Th52:
for a, b, c being real number st a < b holds
c in RAT (a,b) iff c is rational & a < c & c < b
proof
let a, b, c be real number;
assume a < b;
hereby assume c in RAT (a,b);
then c in RAT /\ ]. a, b .[ by Def4;
then c in RAT & c in ]. a, b .[ by XBOOLE_0:def 3;
hence c is rational & a < c & c < b by JORDAN6:45,RAT_1:def 2;
end;
assume c is rational & a < c & c < b;
then c in RAT & c in ]. a, b .[ by JORDAN6:45,RAT_1:def 2;
then c in RAT /\ ]. a, b .[ by XBOOLE_0:def 3;
hence thesis by Def4;
end;
theorem Th53:
for a, b, c being real number st a < b holds
c in IRRAT (a,b) iff c is irrational & a < c & c < b
proof
let a, b, c be real number;
assume a < b;
hereby assume c in IRRAT (a,b);
then c in IRRAT /\ ]. a, b .[ by Def5;
then c in IRRAT & c in ]. a, b .[ by XBOOLE_0:def 3;
hence c is irrational & a < c & c < b by Th37,JORDAN6:45;
end;
assume c is irrational & a < c & c < b;
then c in IRRAT & c in ]. a, b .[ by Th37,JORDAN6:45;
then c in IRRAT /\ ]. a, b .[ by XBOOLE_0:def 3;
hence thesis by Def5;
end;
theorem Th54:
for A being Subset of R^1,
a, b being real number st a < b & A = RAT (a, b) holds
Cl A = [. a, b .]
proof
let A be Subset of R^1,
a, b be real number;
assume that
A1: a < b and
A2: A = RAT (a, b);
RAT /\ ]. a, b .[ c= ]. a, b .[ by XBOOLE_1:17;
then RAT /\ ]. a, b .[ c= the carrier of R^1
by TOPMETR:24,XBOOLE_1:1;
then reconsider RR = RAT /\ ]. a, b .[ as Subset of R^1;
reconsider ab = ]. a, b .[, RT = RAT as Subset of R^1
by RAT_1:4,TOPMETR:24;
A3: Cl RR c= (Cl RT) /\ Cl ab by PRE_TOPC:51;
A4: (the carrier of R^1) /\ Cl ab = Cl ab by XBOOLE_1:28;
thus Cl A c= [. a, b .]
proof
let x be set;
assume x in Cl A;
then x in Cl RR by A2,Def4;
then x in (Cl RT) /\ Cl ab by A3;
then x in (the carrier of R^1) /\ Cl ab by Th35;
hence thesis by A1,A4,Th36;
end;
thus [. a, b .] c= Cl A
proof
let x be set;
assume A5: x in [. a, b .];
then x is real number by XREAL_0:def 1;
then reconsider p = x as Element of RealSpace by Lm3;
A6: a <= p by A5,TOPREAL5:1;
A7: p <= b by A5,TOPREAL5:1;
per cases by A7,REAL_1:def 5;
suppose
A8: p < b;
now let r be real number;
assume
A9: r > 0;
reconsider pp = p + r as Element of RealSpace by Lm3;
set pr = min (pp, (p + b)/2);
A10: pr <= (p + b)/2 by SQUARE_1:35;
A11: (p + b)/2 < b by A8,TOPREAL3:3;
p < pr
proof
per cases by SQUARE_1:38;
suppose pr = pp;
hence thesis by A9,REAL_1:69;
suppose pr = (p + b)/2;
hence thesis by A8,TOPREAL3:3;
end;
then consider Q being rational number such that
A12: p < Q & Q < pr by RAT_1:22;
A13: Q in RAT by RAT_1:def 2;
pr < b by A10,A11,AXIOMS:22;
then a < Q & Q < b by A6,A12,AXIOMS:22;
then Q in ]. a, b .[ by JORDAN6:45;
then Q in RAT /\ ]. a, b .[ by A13,XBOOLE_0:def 3;
then A14: Q in A by A2,Def4;
reconsider P = Q as Element of RealSpace by Lm3;
A15: P - p < pr - p by A12,REAL_1:54;
pr - p <= r
proof
per cases by SQUARE_1:38;
suppose pr = pp;
hence thesis by XCMPLX_1:26;
suppose pr = (p + b)/2;
pr <= pp by SQUARE_1:35;
then pr - p <= pp - p by REAL_1:49;
hence thesis by XCMPLX_1:26;
end;
then P - p < r by A15,AXIOMS:22;
then dist (p, P) < r by A12,Th34;
then P in Ball (p, r) by METRIC_1:12;
hence Ball (p, r) meets A by A14,XBOOLE_0:3;
end;
hence thesis by Th33;
suppose p = b;
hence thesis by A1,A2,Lm5;
end;
end;
theorem Th55:
for A being Subset of R^1,
a, b being real number st a < b & A = IRRAT (a, b) holds
Cl A = [. a, b .]
proof
let A be Subset of R^1,
a, b be real number;
assume that
A1: a < b and
A2: A = IRRAT (a, b);
reconsider RR = IRRAT /\ ]. a, b .[ as Subset of R^1
by TOPMETR:24;
reconsider ab = ]. a, b .[, RT = IRRAT as Subset of R^1
by TOPMETR:24;
A3: Cl RR c= (Cl RT) /\ Cl ab by PRE_TOPC:51;
A4: (the carrier of R^1) /\ Cl ab = Cl ab by XBOOLE_1:28;
thus Cl A c= [. a, b .]
proof
let x be set;
assume x in Cl A;
then x in Cl RR by A2,Def5;
then x in (Cl RT) /\ Cl ab by A3;
then x in (the carrier of R^1) /\ Cl ab by Th51;
hence thesis by A1,A4,Th36;
end;
thus [. a, b .] c= Cl A
proof
let x be set;
assume A5: x in [. a, b .];
then x is real number by XREAL_0:def 1;
then reconsider p = x as Element of RealSpace by Lm3;
A6: a <= p by A5,TOPREAL5:1;
A7: p <= b by A5,TOPREAL5:1;
per cases by A7,REAL_1:def 5;
suppose
A8: p < b;
now let r be real number;
assume
A9: r > 0;
reconsider pp = p + r as Element of RealSpace by Lm3;
set pr = min (pp, (p + b)/2);
A10: pr <= (p + b)/2 by SQUARE_1:35;
A11: (p + b)/2 < b by A8,TOPREAL3:3;
p < pr
proof
per cases by SQUARE_1:38;
suppose pr = pp;
hence thesis by A9,REAL_1:69;
suppose pr = (p + b)/2;
hence thesis by A8,TOPREAL3:3;
end;
then consider Q being irrational (real number) such that
A12: p < Q & Q < pr by Th50;
A13: Q in IRRAT by Th37;
pr < b by A10,A11,AXIOMS:22;
then a < Q & Q < b by A6,A12,AXIOMS:22;
then Q in ]. a, b .[ by JORDAN6:45;
then Q in IRRAT /\ ]. a, b .[ by A13,XBOOLE_0:def 3;
then A14: Q in A by A2,Def5;
reconsider P = Q as Element of RealSpace by Lm3;
A15: P - p < pr - p by A12,REAL_1:54;
pr - p <= r
proof
per cases by SQUARE_1:38;
suppose pr = pp;
hence thesis by XCMPLX_1:26;
suppose pr = (p + b)/2;
pr <= pp by SQUARE_1:35;
then pr - p <= pp - p by REAL_1:49;
hence thesis by XCMPLX_1:26;
end;
then P - p < r by A15,AXIOMS:22;
then dist (p, P) < r by A12,Th34;
then P in Ball (p, r) by METRIC_1:12;
hence Ball (p, r) meets A by A14,XBOOLE_0:3;
end;
hence thesis by Th33;
suppose p = b;
hence thesis by A1,A2,Lm6;
end;
end;
theorem Th56:
for T being connected TopSpace,
A being closed open Subset of T holds
A = {} or A = [#]T
proof
let T be connected TopSpace,
A be closed open Subset of T;
assume that
A1: A <> {} and
A2: A <> [#]T;
A3: A <> {}T by A1;
A4: [#]T = A \/ A` by PRE_TOPC:18;
A misses A` by TOPS_1:20;
then A5: A, A` are_separated by A4,CONNSP_1:3;
[#]T \ A <> {} by A2,PRE_TOPC:23;
then A` <> {} by PRE_TOPC:17;
then not [#]T is connected by A3,A4,A5,CONNSP_1:16;
hence thesis by CONNSP_1:28;
end;
theorem Th57:
for A being Subset of R^1 st A is closed open holds
A = {} or A = REAL
proof
let A be Subset of R^1;
assume A is closed open;
then reconsider A as closed open Subset of R^1;
A = {} or A = [#]R^1 by Th56;
hence thesis by PRE_TOPC:def 3,TOPMETR:24;
end;
begin :: Topological Properties of Intervals
theorem Th58:
for A being Subset of R^1,
a, b being real number st
A = [. a, b .[ & a <> b holds
Cl A = [. a, b .]
proof
let A be Subset of R^1,
a, b be real number;
assume
A1: A = [. a, b .[ & a <> b;
then Cl [. a, b .[ = [. a, b .] by BORSUK_4:21;
hence thesis by A1,Lm2;
end;
theorem Th59:
for A being Subset of R^1,
a, b being real number st
A = ]. a, b .] & a <> b holds
Cl A = [. a, b .]
proof
let A be Subset of R^1,
a, b be real number;
assume
A1: A = ]. a, b .] & a <> b;
then Cl ]. a, b .] = [. a, b .] by BORSUK_4:20;
hence thesis by A1,Lm2;
end;
theorem
for A being Subset of R^1,
a, b, c being real number st
A = [. a, b .[ \/ ]. b, c .] & a < b & b < c holds
Cl A = [. a, c .]
proof
let A be Subset of R^1,
a, b, c be real number;
assume that
A1: A = [. a, b .[ \/ ]. b, c .] and
A2: a < b & b < c;
reconsider B = [. a, b .[, C = ]. b, c .] as Subset of R^1
by TOPMETR:24;
Cl A = Cl B \/ Cl C by A1,PRE_TOPC:50
.= [. a, b .] \/ Cl C by A2,Th58
.= [. a, b .] \/ [. b, c .] by A2,Th59
.= [. a, c .] by A2,TREAL_1:2;
hence thesis;
end;
theorem Th61:
for A being Subset of R^1,
a being real number st A = {a} holds Cl A = {a}
proof
let A be Subset of R^1,
a be real number;
assume
A1: A = {a};
a is Point of R^1 by TOPMETR:24,XREAL_0:def 1;
hence thesis by A1,YELLOW_8:35;
end;
theorem Th62:
for A being Subset of REAL, B being Subset of R^1 st A = B holds
A is open iff B is open
proof
let A be Subset of REAL,
B be Subset of R^1;
assume
A1: A = B;
hereby assume A is open;
then A in Family_open_set RealSpace by JORDAN5A:6;
then A in the topology of TopSpaceMetr RealSpace by TOPMETR:16;
hence B is open by A1,PRE_TOPC:def 5,TOPMETR:def 7;
end;
assume B is open;
then B in the topology of R^1 by PRE_TOPC:def 5;
then A in Family_open_set RealSpace by A1,TOPMETR:16,def 7;
hence thesis by JORDAN5A:6;
end;
Lm7:
for a being real number holds ]. a,+infty.[ is open
proof
let a be real number;
a is Real by XREAL_0:def 1;
hence thesis by FCONT_3:7;
end;
Lm8:
for a being real number holds ].-infty,a.] is closed
proof
let a be real number;
a is Real by XREAL_0:def 1;
hence thesis by FCONT_3:6;
end;
Lm9:
for a being real number holds ].-infty,a.[ is open
proof
let a be real number;
a is Real by XREAL_0:def 1;
hence thesis by FCONT_3:8;
end;
Lm10:
for a being real number holds [.a,+infty.[ is closed
proof
let a be real number;
a is Real by XREAL_0:def 1;
hence thesis by FCONT_3:5;
end;
theorem Th63:
for A being Subset of R^1,
a being real number st
A = ]. a,+infty.[ holds A is open
proof
let A be Subset of R^1,
a be real number;
assume
A1: A = ]. a,+infty.[;
]. a,+infty.[ is open by Lm7;
hence thesis by A1,Th62;
end;
theorem Th64:
for A being Subset of R^1,
a being real number st
A = ].-infty,a .[ holds A is open
proof
let A be Subset of R^1,
a be real number;
assume
A1: A = ].-infty,a .[;
].-infty,a .[ is open by Lm9;
hence thesis by A1,Th62;
end;
theorem Th65:
for A being Subset of R^1,
a being real number st
A = ].-infty,a.] holds A is closed
proof
let A be Subset of R^1,
a be real number;
assume
A1: A = ].-infty,a.];
].-infty,a.] is closed by Lm8;
hence thesis by A1,TOPREAL6:79;
end;
theorem Th66:
for A being Subset of R^1,
a being real number st
A = [. a,+infty.[ holds A is closed
proof
let A be Subset of R^1,
a be real number;
assume
A1: A = [. a,+infty.[;
[. a,+infty.[ is closed by Lm10;
hence thesis by A1,TOPREAL6:79;
end;
theorem Th67:
for a being real number holds
[. a,+infty.[ = {a} \/ ]. a,+infty.[
proof
let a be real number;
thus [. a,+infty.[ c= {a} \/ ]. a,+infty.[
proof
let x be set;
assume
A1: x in [. a,+infty.[;
then reconsider x as real number by XREAL_0:def 1;
A2: x >= a by A1,Th15;
per cases by A2,REAL_1:def 5;
suppose x = a;
then x in {a} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 2;
suppose x > a;
then x in ]. a,+infty.[ by Th14;
hence thesis by XBOOLE_0:def 2;
end;
let x be set;
assume
A3: x in {a} \/ ]. a,+infty.[;
then reconsider x as real number by XREAL_0:def 1;
x in {a} or x in ]. a,+infty.[ by A3,XBOOLE_0:def 2;
then x = a or x > a by Th14,TARSKI:def 1;
hence thesis by Th15;
end;
theorem Th68:
for a being real number holds
].-infty,a.] = {a} \/ ].-infty,a.[
proof
let a be real number;
thus ].-infty,a.] c= {a} \/ ].-infty,a.[
proof
let x be set;
assume
A1: x in ].-infty,a.];
then reconsider x as real number by XREAL_0:def 1;
A2: x <= a by A1,Th16;
per cases by A2,REAL_1:def 5;
suppose x = a;
then x in {a} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 2;
suppose x < a;
then x in ].-infty,a.[ by Th17;
hence thesis by XBOOLE_0:def 2;
end;
let x be set;
assume
A3: x in {a} \/ ].-infty,a.[;
then reconsider x as real number by XREAL_0:def 1;
x in {a} or x in ].-infty,a.[ by A3,XBOOLE_0:def 2;
then x = a or x < a by Th17,TARSKI:def 1;
hence thesis by Th16;
end;
theorem Th69:
for a being real number holds
]. a,+infty.[ c= [. a,+infty.[
proof
let a be real number;
a is Real by XREAL_0:def 1;
hence thesis by LIMFUNC1:10;
end;
theorem Th70:
for a being real number holds
].-infty,a .[ c= ].-infty,a .]
proof
let a be real number;
a is Real by XREAL_0:def 1;
hence thesis by LIMFUNC1:15;
end;
definition let a be real number;
cluster ]. a,+infty.[ -> non empty;
coherence
proof
a < a + 1 by REAL_1:69;
hence thesis by Th14;
end;
cluster ].-infty,a .] -> non empty;
coherence by Th16;
cluster ].-infty,a .[ -> non empty;
coherence
proof
a - 1 < a by INT_1:26;
hence thesis by Th17;
end;
cluster [. a,+infty.[ -> non empty;
coherence by Th15;
end;
theorem Th71:
for a being real number holds
]. a,+infty.[ <> REAL
proof
let a be real number;
a in REAL by XREAL_0:def 1;
hence thesis by Th14;
end;
theorem
for a being real number holds
[. a,+infty.[ <> REAL
proof
let a be real number;
A1: a - 1 in REAL by XREAL_0:def 1;
a - 1 < a by INT_1:26;
hence thesis by A1,Th15;
end;
theorem
for a being real number holds
].-infty, a .] <> REAL
proof
let a be real number;
A1: a + 1 in REAL by XREAL_0:def 1;
a + 1 > a by REAL_1:69;
hence thesis by A1,Th16;
end;
theorem Th74:
for a being real number holds
].-infty, a .[ <> REAL
proof
let a be real number;
A1: a + 1 in REAL by XREAL_0:def 1;
a + 1 > a by REAL_1:69;
hence thesis by A1,Th17;
end;
theorem Th75:
for A being Subset of R^1,
a being real number st
A = ]. a,+infty.[ holds Cl A = [. a,+infty.[
proof
let A be Subset of R^1,
a be real number;
reconsider A' = A as Subset of R^1;
assume
A1: A = ]. a,+infty.[;
then A2: A' is open by Th63;
reconsider C = [. a,+infty.[ as Subset of R^1
by TOPMETR:24;
A3: C is closed by Th66;
A4: C = A' \/ {a} by A1,Th67;
A5: A' c= Cl A' by PRE_TOPC:48;
A' c= C by A1,Th69;
then A6: Cl A' c= C by A3,TOPS_1:31;
per cases by A4,A5,A6,Th2;
suppose Cl A' = C;
hence thesis;
suppose Cl A' = A';
then A' = {} or A' = REAL by A2,Th57;
hence thesis by A1,Th71;
end;
theorem
for a being real number holds
Cl ]. a,+infty.[ = [. a,+infty.[
proof
let a be real number;
reconsider A = ]. a,+infty.[ as Subset of R^1
by TOPMETR:24;
Cl A = [. a,+infty.[ by Th75;
hence thesis by TOPREAL6:80;
end;
theorem Th77:
for A being Subset of R^1,
a being real number st
A = ].-infty, a .[ holds Cl A = ].-infty, a .]
proof
let A be Subset of R^1,
a be real number;
reconsider A' = A as Subset of R^1;
assume
A1: A = ].-infty, a .[;
then A2: A' is open by Th64;
reconsider C = ].-infty, a .] as Subset of R^1
by TOPMETR:24;
A3: C is closed by Th65;
A4: C = A' \/ {a} by A1,Th68;
A5: A' c= Cl A' by PRE_TOPC:48;
A' c= C by A1,Th70;
then A6: Cl A' c= C by A3,TOPS_1:31;
per cases by A4,A5,A6,Th2;
suppose Cl A' = C;
hence thesis;
suppose Cl A' = A';
then A' = {} or A' = REAL by A2,Th57;
hence thesis by A1,Th74;
end;
theorem
for a being real number holds
Cl ].-infty, a .[ = ].-infty, a .]
proof
let a be real number;
reconsider A = ].-infty, a .[ as Subset of R^1
by TOPMETR:24;
Cl A = ].-infty, a .] by Th77;
hence thesis by TOPREAL6:80;
end;
theorem Th79:
for A, B being Subset of R^1,
b being real number st
A = ].-infty, b .[ & B = ]. b,+infty.[ holds A, B are_separated
proof
let A, B be Subset of R^1,
b be real number;
assume that
A1: A = ].-infty, b .[ and
A2: B = ]. b,+infty.[;
Cl A = ].-infty, b .] by A1,Th77;
then A3: Cl A misses B by A2,Th26;
Cl B = [. b,+infty.[ by A2,Th75;
then Cl B misses A by A1,Th27;
hence thesis by A3,CONNSP_1:def 1;
end;
theorem
for A being Subset of R^1,
a, b being real number st a < b &
A = [. a, b .[ \/ ]. b,+infty.[ holds Cl A = [. a,+infty.[
proof
let A be Subset of R^1,
a, b be real number;
assume
A1: a < b & A = [. a, b .[ \/ ]. b,+infty.[;
reconsider B = [. a, b .[, C = ]. b,+infty.[ as Subset of R^1
by TOPMETR:24;
A2: Cl B = [. a, b .] by A1,Th58;
A3: Cl C = [. b,+infty.[ by Th75;
Cl A = Cl B \/ Cl C by A1,PRE_TOPC:50;
hence thesis by A1,A2,A3,Th28;
end;
theorem Th81:
for A being Subset of R^1,
a, b being real number st a < b &
A = ]. a, b .[ \/ ]. b,+infty.[ holds Cl A = [. a,+infty.[
proof
let A be Subset of R^1,
a, b be real number;
assume
A1: a < b & A = ]. a, b .[ \/ ]. b,+infty.[;
reconsider B = ]. a, b .[, C = ]. b,+infty.[ as Subset of R^1
by TOPMETR:24;
A2: Cl A = Cl B \/ Cl C by A1,PRE_TOPC:50;
A3: Cl B = [. a, b .] by A1,Th36;
Cl C = [. b,+infty.[ by Th75;
hence thesis by A1,A2,A3,Th28;
end;
theorem
for A being Subset of R^1,
a, b, c being real number st a < b & b < c &
A = RAT (a,b) \/ ]. b, c .[ \/ ]. c,+infty.[ holds
Cl A = [. a,+infty.[
proof
let A be Subset of R^1;
let a, b, c be real number;
assume
A1: a < b & b < c;
reconsider C = ]. b, c .[ \/ ]. c,+infty.[ as Subset of R^1
by TOPMETR:24;
reconsider B = RAT (a,b) as Subset of R^1 by TOPMETR:24;
assume A = RAT (a,b) \/ ]. b, c .[ \/ ]. c,+infty.[;
then A = RAT (a,b) \/ C by XBOOLE_1:4;
then Cl A = Cl B \/ Cl C by PRE_TOPC:50;
then Cl A = Cl B \/ [. b,+infty.[ by A1,Th81;
then Cl A = [. a, b .] \/ [. b,+infty.[ by A1,Th54;
hence Cl A = [. a,+infty.[ by A1,Th28;
end;
theorem
for A being Subset of R^1 holds
A` = REAL \ A by Th13,PRE_TOPC:17;
theorem Th84:
for a, b being real number st a < b holds
IRRAT (a, b) misses RAT (a, b)
proof
let a, b be real number;
assume
A1: a < b;
assume IRRAT (a, b) meets RAT (a, b);
then consider x being set such that
A2: x in IRRAT (a, b) & x in RAT (a, b) by XBOOLE_0:3;
reconsider x as real number by A2,XREAL_0:def 1;
x is rational & x is irrational by A1,A2,Th52,Th53;
hence thesis;
end;
theorem Th85:
for a, b being real number st a < b holds
REAL \ RAT (a, b) = ].-infty,a.] \/ IRRAT (a, b) \/ [.b,+infty.[
proof
let a, b be real number;
assume
A1: a < b;
thus REAL \ RAT (a, b) c= ].-infty,a.] \/ IRRAT (a, b) \/ [.b,+infty.[
proof
let x be set;
assume x in REAL \ RAT (a, b);
then A2: x in REAL & not x in RAT (a, b) by XBOOLE_0:def 4;
then reconsider x as real number by XREAL_0:def 1;
per cases;
suppose x <= a & x < b;
then x in ].-infty,a.] by Th16;
then x in ].-infty,a.] \/ IRRAT (a, b) by XBOOLE_0:def 2;
hence thesis by XBOOLE_0:def 2;
suppose x <= a & x >= b;
then x in ].-infty,a.] by Th16;
then x in ].-infty,a.] \/ IRRAT (a, b) by XBOOLE_0:def 2;
hence thesis by XBOOLE_0:def 2;
suppose
A3: x > a & x < b;
x in IRRAT (a, b)
proof
per cases;
suppose x is rational;
hence thesis by A1,A2,A3,Th52;
suppose x is irrational;
hence thesis by A1,A3,Th53;
end;
then x in ].-infty,a.] \/ IRRAT (a, b) by XBOOLE_0:def 2;
hence thesis by XBOOLE_0:def 2;
suppose x > a & x >= b;
then x in [.b,+infty.[ by Th15;
hence thesis by XBOOLE_0:def 2;
end;
let x be set;
assume
A4: x in ].-infty,a.] \/ IRRAT (a, b) \/ [.b,+infty.[;
then reconsider x as real number by XREAL_0:def 1;
A5: x in ].-infty,a.] \/ IRRAT (a, b) or x in [.b,+infty.[
by A4,XBOOLE_0:def 2;
per cases by A5,XBOOLE_0:def 2;
suppose x in ].-infty,a.];
then x <= a by Th16;
then x in REAL & not x in RAT (a, b) by A1,Th52,XREAL_0:def 1;
hence thesis by XBOOLE_0:def 4;
suppose
A6: x in IRRAT (a, b);
A7: x in REAL by XREAL_0:def 1;
IRRAT (a, b) misses RAT (a, b) by A1,Th84;
then not x in RAT (a,b) by A6,XBOOLE_0:3;
hence thesis by A7,XBOOLE_0:def 4;
suppose x in [.b,+infty.[;
then x >= b by Th15;
then x in REAL & not x in RAT (a, b) by A1,Th52,XREAL_0:def 1;
hence thesis by XBOOLE_0:def 4;
end;
theorem Th86:
for a, b, c being real number st a <= b & b < c holds
not a in ]. b, c .[ \/ ]. c,+infty.[
proof
let a, b, c be real number;
assume
A1: a <= b & b < c;
then a < c by AXIOMS:22;
then not a in ]. b, c .[ & not a in ]. c,+infty.[ by A1,Th14,JORDAN6:45;
hence thesis by XBOOLE_0:def 2;
end;
theorem Th87:
for a, b being real number st a < b holds
not b in ]. a, b .[ \/ ]. b,+infty.[
proof
let a, b be real number;
assume a < b;
not b in ]. a, b .[ & not b in ]. b,+infty.[ by Th14,JORDAN6:45;
hence thesis by XBOOLE_0:def 2;
end;
theorem Th88:
for a, b being real number st a < b holds
[.a,+infty.[ \ (]. a, b .[ \/ ]. b,+infty.[) = {a} \/ {b}
proof
let a, b be real number;
assume
A1: a < b;
then A2: not a in ]. a,b .[ \/ ]. b,+infty.[ by Th86;
not b in ]. a,b .[ \/ ]. b,+infty.[ by A1,Th87;
then A3: {a, b} misses ]. a,b .[ \/ ]. b,+infty.[ by A2,ZFMISC_1:57;
[. a,+infty.[ = [. a,b .] \/ [. b,+infty.[ by A1,Th28
.= {a, b} \/ ]. a,b .[ \/ [. b,+infty.[ by A1,RCOMP_1:11
.= {a, b} \/ ]. a,b .[ \/ ({b} \/ ]. b,+infty.[) by Th67
.= {a, b} \/ ]. a,b .[ \/ {b} \/ ]. b,+infty.[ by XBOOLE_1:4
.= {a, b} \/ {b} \/ ]. a,b .[ \/ ]. b,+infty.[ by XBOOLE_1:4
.= {a, b} \/ ]. a,b .[ \/ ]. b,+infty.[ by ZFMISC_1:14
.= {a, b} \/ (]. a,b .[ \/ ]. b,+infty.[) by XBOOLE_1:4;
then [.a,+infty.[ \ (]. a, b .[ \/ ]. b,+infty.[) = {a, b}
by A3,XBOOLE_1:88;
hence thesis by ENUMSET1:41;
end;
theorem
for A being Subset of R^1 st
A = RAT (2,3) \/ ]. 3, 4 .[ \/ ]. 4,+infty.[ holds
A` = ].-infty,2 .] \/ IRRAT(2,3) \/ {3} \/ {4}
proof
let A be Subset of R^1;
assume A = RAT (2,3) \/ ]. 3, 4 .[ \/ ]. 4,+infty.[;
then A1: A` = REAL \ (RAT (2,3) \/ ]. 3, 4 .[ \/ ]. 4,+infty.[)
by Th13,PRE_TOPC:17
.= REAL \ (RAT (2,3) \/ (]. 3, 4 .[ \/ ]. 4,+infty.[)) by XBOOLE_1:4
.= REAL \ RAT (2,3) \ (]. 3, 4 .[ \/ ]. 4,+infty.[) by XBOOLE_1:41
.= (].-infty,2.] \/ IRRAT (2, 3) \/ [.3,+infty.[) \
(]. 3, 4 .[ \/ ]. 4,+infty.[) by Th85;
A2: ].-infty,3.] misses ]. 3,+infty.[ by Th26;
A3: ].-infty,2.] \/ IRRAT (2, 3) c= ].-infty,3.]
proof
let x be set;
assume
A4: x in ].-infty,2.] \/ IRRAT (2, 3);
then reconsider x as real number by XREAL_0:def 1;
per cases by A4,XBOOLE_0:def 2;
suppose x in ].-infty,2.];
then x <= 2 by Th16;
then x <= 3 by AXIOMS:22;
hence thesis by Th16;
suppose x in IRRAT (2, 3);
then x < 3 by Th53;
hence thesis by Th16;
end;
]. 3, 4 .[ \/ ]. 4,+infty.[ c= ]. 3,+infty.[
proof
let x be set;
assume
A5: x in ]. 3, 4 .[ \/ ]. 4,+infty.[;
then reconsider x as real number by XREAL_0:def 1;
per cases by A5,XBOOLE_0:def 2;
suppose x in ]. 3, 4 .[;
then x > 3 by JORDAN6:45;
hence thesis by Th14;
suppose x in ]. 4,+infty.[;
then x > 4 by Th14;
then x > 3 by AXIOMS:22;
hence thesis by Th14;
end;
then ].-infty,2.] \/ IRRAT (2, 3) misses ]. 3, 4 .[ \/ ]. 4,+infty.[
by A2,A3,XBOOLE_1:64;
then A` = ([.3,+infty.[ \
(]. 3, 4 .[ \/ ]. 4,+infty.[)) \/ (].-infty,2.] \/ IRRAT (2, 3))
by A1,XBOOLE_1:87
.= (].-infty,2.] \/ IRRAT (2, 3)) \/ ({3} \/ {4}) by Th88
.= ].-infty,2 .] \/ IRRAT(2,3) \/ {3} \/ {4} by XBOOLE_1:4;
hence thesis;
end;
theorem
for A being Subset of R^1,
a being real number st A = {a} holds
A` = ].-infty, a .[ \/ ]. a,+infty.[
proof
let A be Subset of R^1,
a be real number;
assume A = {a};
then A` = REAL \ {a} by Th13,PRE_TOPC:17;
hence thesis by Th18;
end;
Lm11: IRRAT(2,3) \/ {3} \/ {4} c= ]. 1,+infty.[
proof
let x be set;
assume
A1: x in IRRAT(2,3) \/ {3} \/ {4};
then reconsider x as real number by XREAL_0:def 1;
A2: x in IRRAT(2,3) \/ {3} or x in {4} by A1,XBOOLE_0:def 2;
per cases by A2,XBOOLE_0:def 2;
suppose x in IRRAT(2,3);
then x > 2 by Th53;
then x > 1 by AXIOMS:22;
hence thesis by Th14;
suppose x in {3};
then x = 3 by TARSKI:def 1;
hence thesis by Th14;
suppose x in {4};
then x = 4 by TARSKI:def 1;
hence thesis by Th14;
end;
]. 1,+infty.[ c= [. 1,+infty.[ by Th69;
then Lm12: IRRAT(2,3) \/ {3} \/ {4} c= [. 1,+infty.[ by Lm11,XBOOLE_1:1;
Lm13: ].-infty, 1 .[ /\ (].-infty, 2 .] \/ IRRAT(2,3) \/ {3} \/ {4}) =
].-infty, 1 .[
proof
[. 1,+infty.[ misses ].-infty, 1 .[ by Th27;
then A1: IRRAT(2,3) \/ {3} \/ {4} misses ].-infty, 1 .[ by Lm12,XBOOLE_1:63;
A2: ].-infty, 1 .[ c= ].-infty, 2 .]
proof
let x be set;
assume
A3: x in ].-infty, 1 .[;
then reconsider x as real number by XREAL_0:def 1;
x < 1 by A3,Th17;
then x < 2 by AXIOMS:22;
hence thesis by Th16;
end;
].-infty, 1 .[ /\ (].-infty, 2 .] \/ IRRAT(2,3) \/ {3} \/ {4}) =
].-infty, 1 .[ /\ (].-infty, 2 .] \/ (IRRAT(2,3) \/ {3} \/ {4}))
by XBOOLE_1:113
.= ].-infty, 1 .[ /\ ].-infty, 2 .] by A1,XBOOLE_1:78
.= ].-infty, 1 .[ by A2,XBOOLE_1:28;
hence thesis;
end;
theorem Th91:
for a, b being real number st a < b holds
]. a,+infty.[ /\ ].-infty, b .] = ]. a, b .]
proof
let a, b be real number;
assume a < b;
thus ]. a,+infty.[ /\ ].-infty, b .] c= ]. a, b .]
proof
let x be set;
assume
A1: x in ]. a,+infty.[ /\ ].-infty, b .];
then reconsider x as real number by XREAL_0:def 1;
x in ]. a,+infty.[ & x in ].-infty, b .] by A1,XBOOLE_0:def 3;
then x > a & x <= b by Th14,Th16;
hence thesis by RCOMP_2:4;
end;
let x be set;
assume
A2: x in ]. a, b .];
then reconsider x as real number by XREAL_0:def 1;
a < x & x <= b by A2,RCOMP_2:4;
then x in ]. a,+infty.[ & x in ].-infty, b .] by Th14,Th16;
hence thesis by XBOOLE_0:def 3;
end;
Lm14: ]. 1,+infty.[ /\ (].-infty, 2 .] \/ IRRAT(2,3) \/ {3} \/ {4}) =
]. 1, 2 .] \/ IRRAT(2,3) \/ {3} \/ {4}
proof
]. 1,+infty.[ /\ (].-infty, 2 .] \/ IRRAT(2,3) \/ {3} \/ {4}) =
]. 1,+infty.[ /\ (].-infty, 2 .] \/ (IRRAT(2,3) \/ {3} \/ {4}))
by XBOOLE_1:113
.= (]. 1,+infty.[ /\ ].-infty, 2 .]) \/
(]. 1,+infty.[ /\ (IRRAT(2,3) \/ {3} \/ {4})) by XBOOLE_1:23
.= (]. 1,+infty.[ /\ ].-infty, 2 .]) \/
(IRRAT(2,3) \/ {3} \/ {4}) by Lm11,XBOOLE_1:28
.= ]. 1,2 .] \/ (IRRAT(2,3) \/ {3} \/ {4}) by Th91
.= ]. 1,2 .] \/ IRRAT(2,3) \/ {3} \/ {4} by XBOOLE_1:113;
hence thesis;
end;
theorem
(].-infty, 1 .[ \/ ]. 1,+infty.[) /\
(].-infty, 2 .] \/ IRRAT(2,3) \/ {3} \/ {4}) =
].-infty, 1 .[ \/ ]. 1, 2 .] \/ IRRAT(2,3) \/ {3} \/ {4}
proof
(].-infty, 1 .[ \/ ]. 1,+infty.[) /\
(].-infty, 2 .] \/ IRRAT(2,3) \/ {3} \/ {4}) = ].-infty, 1 .[ \/
(]. 1,+infty.[ /\ (].-infty, 2 .] \/ IRRAT(2,3) \/ {3} \/ {4}))
by Lm13,XBOOLE_1:23
.= ].-infty, 1 .[ \/ (]. 1, 2 .] \/ IRRAT(2,3) \/ ({3} \/ {4}))
by Lm14,XBOOLE_1:4
.= ].-infty, 1 .[ \/ ]. 1, 2 .] \/ IRRAT(2,3) \/ ({3} \/ {4})
by XBOOLE_1:113;
hence thesis by XBOOLE_1:4;
end;
theorem Th93:
for a, b being real number st a <= b holds
].-infty,b.[ \ {a} = ].-infty, a .[ \/ ]. a, b .[
proof
let a, b be real number;
assume
A1: a <= b;
thus ].-infty,b.[ \ {a} c= ].-infty, a .[ \/ ]. a, b .[
proof
let x be set;
assume
A2: x in ].-infty,b .[ \ {a};
then reconsider x as real number by XREAL_0:def 1;
A3: x in ].-infty,b.[ & x <> a by A2,ZFMISC_1:64;
then A4: x < b by Th17;
per cases by A3,REAL_1:def 5;
suppose x < a;
then x in ].-infty, a .[ by Th17;
hence thesis by XBOOLE_0:def 2;
suppose x > a;
then x in ]. a, b .[ by A4,JORDAN6:45;
hence thesis by XBOOLE_0:def 2;
end;
let x be set;
assume
A5: x in ].-infty, a .[ \/ ]. a, b .[;
then reconsider x as real number by XREAL_0:def 1;
per cases by A5,XBOOLE_0:def 2;
suppose
A6: x in ].-infty, a .[;
then x < a by Th17;
then x < b by A1,AXIOMS:22;
then x in ].-infty,b.[ & x <> a by A6,Th17;
hence thesis by ZFMISC_1:64;
suppose x in ]. a, b .[;
then a < x & x < b by JORDAN6:45;
then x in ].-infty,b.[ & x <> a by Th17;
hence thesis by ZFMISC_1:64;
end;
theorem Th94:
for a, b being real number st a <= b holds
]. a,+infty.[ \ {b} = ]. a, b .[ \/ ]. b,+infty.[
proof
let a, b be real number;
assume
A1: a <= b;
thus ]. a,+infty.[ \ {b} c= ]. a, b .[ \/ ]. b,+infty.[
proof
let x be set;
assume
A2: x in ]. a,+infty.[ \ {b};
then reconsider x as real number by XREAL_0:def 1;
A3: x in ]. a,+infty.[ & x <> b by A2,ZFMISC_1:64;
then A4: x > a by Th14;
per cases by A3,REAL_1:def 5;
suppose x > b;
then x in ]. b,+infty.[ by Th14;
hence thesis by XBOOLE_0:def 2;
suppose x < b;
then x in ]. a, b .[ by A4,JORDAN6:45;
hence thesis by XBOOLE_0:def 2;
end;
let x be set;
assume
A5: x in ]. a, b .[ \/ ]. b,+infty.[;
then reconsider x as real number by XREAL_0:def 1;
per cases by A5,XBOOLE_0:def 2;
suppose
A6: x in ]. b,+infty.[;
then x > b by Th14;
then x > a by A1,AXIOMS:22;
then x in ]. a,+infty.[ & x <> b by A6,Th14;
hence thesis by ZFMISC_1:64;
suppose x in ]. a, b .[;
then a < x & x < b by JORDAN6:45;
then x in ]. a,+infty.[ & x <> b by Th14;
hence thesis by ZFMISC_1:64;
end;
theorem
for A being Subset of R^1,
a, b being real number st a <= b &
A = {a} \/ [. b,+infty.[ holds
A` = ].-infty, a .[ \/ ]. a, b .[
proof
let A be Subset of R^1,
a, b be real number;
assume
A1: a <= b & A = {a} \/ [. b,+infty.[;
then A` = REAL \ ({a} \/ [. b,+infty.[) by Th13,PRE_TOPC:17
.= (REAL \ [. b,+infty.[) \ {a} by XBOOLE_1:41
.= ].-infty,b.[ \ {a} by Th25;
hence thesis by A1,Th93;
end;
theorem
for A being Subset of R^1,
a, b being real number st a < b &
A = ].-infty, a .[ \/ ]. a, b .[ holds Cl A = ].-infty, b .]
proof
let A be Subset of R^1,
a, b be real number;
assume
A1: a < b & A = ].-infty, a .[ \/ ]. a, b .[;
reconsider B = ].-infty, a .[, C = ]. a, b .[ as Subset of R^1
by TOPMETR:24;
A2: Cl C = [. a, b .] by A1,Th36;
Cl A = Cl B \/ Cl C by A1,PRE_TOPC:50
.= ].-infty, a .] \/ [. a, b .] by A2,Th77
.= ].-infty, b .] by A1,Th29;
hence thesis;
end;
theorem Th97:
for A being Subset of R^1,
a, b being real number st a < b &
A = ].-infty, a .[ \/ ]. a, b .] holds Cl A = ].-infty, b .]
proof
let A be Subset of R^1,
a, b be real number;
assume
A1: a < b & A = ].-infty, a .[ \/ ]. a, b .];
reconsider B = ].-infty, a .[, C = ]. a, b .] as Subset of R^1
by TOPMETR:24;
A2: Cl C = [. a, b .] by A1,Th59;
Cl A = Cl B \/ Cl C by A1,PRE_TOPC:50
.= ].-infty, a .] \/ [. a, b .] by A2,Th77
.= ].-infty, b .] by A1,Th29;
hence thesis;
end;
theorem
for A being Subset of R^1,
a being real number st
A = ].-infty, a .] holds A` = ]. a ,+infty.[
proof
let A be Subset of R^1,
a be real number;
assume
A1: A = ].-infty, a .];
A` = REAL \ A by Th13,PRE_TOPC:17
.= ]. a ,+infty.[ by A1,Th23;
hence thesis;
end;
theorem
for A being Subset of R^1,
a being real number st
A = [. a ,+infty.[ holds A` = ].-infty, a .[
proof
let A be Subset of R^1,
a be real number;
assume
A1: A = [. a ,+infty.[;
A` = REAL \ A by Th13,PRE_TOPC:17
.= ].-infty, a .[ by A1,Th25;
hence thesis;
end;
theorem Th100:
for A being Subset of R^1,
a, b, c being real number st a < b & b < c &
A = ].-infty, a .[ \/ ]. a, b .] \/ IRRAT(b,c) \/ {c} holds
Cl A = ].-infty, c .]
proof
let A be Subset of R^1,
a, b, c be real number;
assume
A1: a < b & b < c &
A = ].-infty, a .[ \/ ]. a, b .] \/ IRRAT(b,c) \/ {c};
reconsider B = ].-infty, a .[, C = ]. a, b .], D = IRRAT(b,c), E = {c}
as Subset of R^1 by TOPMETR:24;
A2: c in E & c in ].-infty, c .] by Th16,TARSKI:def 1;
Cl A = Cl (B \/ C \/ D) \/ Cl E by A1,PRE_TOPC:50
.= Cl (B \/ C \/ D) \/ E by Th61
.= Cl (B \/ C) \/ Cl D \/ E by PRE_TOPC:50
.= ].-infty, b .] \/ Cl D \/ E by A1,Th97
.= ].-infty, b .] \/ [. b,c .] \/ E by A1,Th55
.= ].-infty, c .] \/ E by A1,Th29
.= ].-infty, c .] by A2,ZFMISC_1:46;
hence thesis;
end;
theorem
for A being Subset of R^1,
a, b, c, d being real number st a < b & b < c &
A = ].-infty, a .[ \/ ]. a, b .] \/ IRRAT(b,c) \/ {c} \/ {d} holds
Cl A = ].-infty, c .] \/ {d}
proof
let A be Subset of R^1,
a, b, c, d be real number;
assume
A1: a < b & b < c &
A = ].-infty, a .[ \/ ]. a, b .] \/ IRRAT(b,c) \/ {c} \/ {d};
reconsider B = ].-infty, a .[, C = ]. a, b .], D = IRRAT(b,c),
E = {c}, F = {d} as Subset of R^1 by TOPMETR:24;
Cl A = Cl (B \/ C \/ D \/ E) \/ Cl F by A1,PRE_TOPC:50
.= Cl (B \/ C \/ D \/ E) \/ {d} by Th61;
hence thesis by A1,Th100;
end;
theorem
for A being Subset of R^1,
a, b being real number st a <= b &
A = ].-infty, a .] \/ {b} holds
A` = ]. a, b .[ \/ ]. b,+infty.[
proof
let A be Subset of R^1,
a, b be real number;
assume
A1: a <= b & A = ].-infty, a .] \/ {b};
A` = REAL \ A by Th13,PRE_TOPC:17
.= (REAL \ ].-infty, a .]) \ {b} by A1,XBOOLE_1:41
.= ]. a,+infty.[ \ {b} by Th23
.= ]. a, b .[ \/ ]. b,+infty.[ by A1,Th94;
hence thesis;
end;
theorem
for a, b being real number holds
[. a,+infty.[ \/ {b} <> REAL
proof
let a, b be real number;
set ab = min (a,b) - 1;
A1: ab in REAL by XREAL_0:def 1;
A2: min (a,b) <= a & min (a,b) <= b by SQUARE_1:35;
A3: ab < min (a,b) by INT_1:26;
then ab < a & ab < b by A2,AXIOMS:22;
then A4: not ab in [. a,+infty.[ by Th15;
not ab in {b} by A2,A3,TARSKI:def 1;
hence thesis by A1,A4,XBOOLE_0:def 2;
end;
theorem
for a, b being real number holds
].-infty, a .] \/ {b} <> REAL
proof
let a, b be real number;
set ab = max (a,b) + 1;
A1: ab in REAL by XREAL_0:def 1;
A2: max (a,b) >= a & max (a,b) >= b by SQUARE_1:46;
A3: ab > max (a,b) by REAL_1:69;
then ab > a & ab > b by A2,AXIOMS:22;
then A4: not ab in ].-infty, a.] by Th16;
not ab in {b} by A2,A3,TARSKI:def 1;
hence thesis by A1,A4,XBOOLE_0:def 2;
end;
theorem
for TS being TopStruct,
A, B being Subset of TS st A <> B holds A` <> B`
proof
let TS be TopStruct,
A, B be Subset of TS;
assume
A1: A <> B;
assume A` = B`;
then A = B``;
hence thesis by A1;
end;
theorem
for A being Subset of R^1 st REAL = A` holds A = {}
proof
let A be Subset of R^1;
reconsider AB = {}R^1 as Subset of R^1;
assume REAL = A`;
then [#]R^1 = A` by PRE_TOPC:12,TOPMETR:24;
then AB` = A` by PRE_TOPC:27;
then AB = A``;
hence thesis;
end;
begin :: Subcontinua of a real line
definition
cluster I[01] -> arcwise_connected;
coherence
proof
for a, b being Point of I[01] ex f being map of I[01], I[01] st
f is continuous & f.0 = a & f.1 = b
proof
let a, b be Point of I[01];
per cases;
suppose
A1: a <= b;
then reconsider B = [. a, b .] as non empty Subset of I[01]
by BORSUK_4:49;
0 <= a & b <= 1 by JORDAN5A:2;
then A2: Closed-Interval-TSpace(a,b) = I[01]|B by A1,JGRAPH_5:7;
then A3: L[01]((#)(a,b),(a,b)(#)) is continuous map of
I[01], I[01]|B by A1,TOPMETR:27,TREAL_1:11;
the carrier of I[01]|B c= the carrier of I[01] by BORSUK_1:35;
then reconsider g = L[01]((#)(a,b),(a,b)(#)) as Function of
the carrier of I[01], the carrier of I[01]
by A2,FUNCT_2:9,TOPMETR:27;
reconsider g as map of I[01], I[01];
take g;
thus g is continuous by A3,TOPMETR:7;
0 = (#)(0,1) by TREAL_1:def 1;
hence g.0 = (#)(a,b) by A1,TREAL_1:12 .= a by A1,TREAL_1:def 1;
1 = (0,1)(#) by TREAL_1:def 2;
hence g.1 = (a,b)(#) by A1,TREAL_1:12 .= b by A1,TREAL_1:def 2;
suppose
A4: b <= a;
then reconsider B = [. b, a .] as non empty Subset of I[01]
by BORSUK_4:49;
0 <= b & a <= 1 by JORDAN5A:2;
then A5: Closed-Interval-TSpace(b,a) = I[01]|B by A4,JGRAPH_5:7;
then A6: L[01]((#)(b,a),(b,a)(#)) is continuous map of
I[01], I[01]|B by A4,TOPMETR:27,TREAL_1:11;
the carrier of I[01]|B c= the carrier of I[01] by BORSUK_1:35;
then reconsider g = L[01]((#)(b,a),(b,a)(#)) as Function of
the carrier of I[01], the carrier of I[01]
by A5,FUNCT_2:9,TOPMETR:27;
reconsider g as map of I[01], I[01];
A7: g is continuous by A6,TOPMETR:7;
0 = (#)(0,1) by TREAL_1:def 1;
then A8: g.0 = (#)(b,a) by A4,TREAL_1:12 .= b by A4,TREAL_1:def 1;
1 = (0,1)(#) by TREAL_1:def 2;
then A9: g.1 = (b,a)(#) by A4,TREAL_1:12 .= a by A4,TREAL_1:def 2;
then reconsider P = g as Path of b, a by A7,A8,BORSUK_2:def 1;
take h = -P;
ex t being map of I[01], I[01] st
t is continuous & t.0 = a & t.1 = b by A7,A8,A9,Th11;
hence thesis by BORSUK_2:def 1;
end;
hence thesis by BORSUK_2:def 2;
end;
end;
theorem Th107:
for X being compact Subset of R^1,
X' being Subset of REAL st X' = X holds
X' is bounded_above bounded_below
proof
let X be compact Subset of R^1,
X' be Subset of REAL;
assume X' = X;
then X' is compact by TOPREAL6:81;
then X' is bounded by RCOMP_1:28;
hence thesis by SEQ_4:def 3;
end;
theorem Th108:
for X being compact Subset of R^1,
X' being Subset of REAL,
x being real number st x in X' & X' = X holds
inf X' <= x & x <= sup X'
proof
let X be compact Subset of R^1,
X' be Subset of REAL,
x be real number;
assume
A1: x in X' & X' = X;
then X' is bounded_above bounded_below by Th107;
hence thesis by A1,SEQ_4:def 4,def 5;
end;
theorem Th109:
for C being non empty compact connected Subset of R^1,
C' being Subset of REAL st C = C' & [. inf C', sup C' .] c= C' holds
[. inf C', sup C' .] = C'
proof
let C be non empty compact connected Subset of R^1,
C' be Subset of REAL;
assume
A1: C = C' & [. inf C', sup C' .] c= C';
assume [. inf C', sup C' .] <> C';
then not C' c= [. inf C', sup C' .] by A1,XBOOLE_0:def 10;
then consider c being set such that
A2: c in C' & not c in [. inf C', sup C' .] by TARSKI:def 3;
reconsider c as real number by A2,XREAL_0:def 1;
inf C' <= c & c <= sup C' by A1,A2,Th108;
hence thesis by A2,TOPREAL5:1;
end;
theorem Th110: :: TOPREAL5:9
for A being connected Subset of R^1,
a, b, c being real number st
a <= b & b <= c & a in A & c in A holds b in A
proof
let A be connected Subset of R^1,
a, b, c be real number;
assume
A1: a <= b & b <= c & a in A & c in A;
per cases by A1,REAL_1:def 5;
suppose a = b or b = c;
hence thesis by A1;
suppose A2: a < b & b < c & a in A & c in A;
assume not b in A;
then A c= REAL \ {b} by TOPMETR:24,ZFMISC_1:40;
then A3: A c= ].-infty,b .[ \/ ]. b,+infty.[ by Th18;
reconsider B = ].-infty,b .[, C = ]. b,+infty.[ as Subset of R^1
by TOPMETR:24;
A4: B, C are_separated by Th79;
now per cases by A3,A4,CONNSP_1:17;
suppose A c= B;
hence contradiction by A2,Th17;
suppose A c= C;
hence contradiction by A2,Th14;
end;
hence thesis;
end;
theorem Th111:
for A being connected Subset of R^1,
a, b being real number st a in A & b in A holds
[.a,b.] c= A
proof
let A be connected Subset of R^1,
a, b be real number;
assume
A1: a in A & b in A;
let x be set;
assume x in [.a,b.];
then x in { y where y is Real : a <= y & y <= b } by RCOMP_1:def 1;
then consider z being Real such that
A2: z = x & a <= z & z <= b;
thus thesis by A1,A2,Th110;
end;
theorem Th112:
for X being non empty compact connected Subset of R^1 holds
X is non empty closed-interval Subset of REAL
proof
let C be non empty compact connected Subset of R^1;
reconsider C' = C as non empty Subset of REAL by TOPMETR:24;
C is closed by COMPTS_1:16;
then A1: C' is closed by TOPREAL6:79;
A2: C' is bounded_below bounded_above by Th107;
then A3: inf C' in C' by A1,RCOMP_1:31;
sup C' in C' by A1,A2,RCOMP_1:30;
then [. inf C', sup C' .] c= C' by A3,Th111;
then A4: [. inf C', sup C' .] = C' by Th109;
C' is bounded by A2,SEQ_4:def 3;
then inf C' <= sup C' by SEQ_4:24;
hence thesis by A4,INTEGRA1:def 1;
end;
theorem
for A being non empty compact connected Subset of R^1 holds
ex a, b being real number st a <= b & A = [. a, b .]
proof
let C be non empty compact connected Subset of R^1;
reconsider C' = C as closed-interval Subset of REAL by Th112;
A1: C' = [. inf C', sup C' .] by INTEGRA1:5;
inf C' <= sup C' by BORSUK_4:53;
then inf C' in C & sup C' in C by A1,RCOMP_1:15;
then reconsider p1 = inf C', p2 = sup C' as Point of R^1;
take p1, p2;
thus p1 <= p2 by BORSUK_4:53;
thus thesis by INTEGRA1:5;
end;
begin :: Sets with Proper Subsets Only
definition let TS be TopStruct; let F be Subset-Family of TS;
attr F is with_proper_subsets means :Def6:
not the carrier of TS in F;
end;
theorem
for TS being TopStruct,
F, G being Subset-Family of TS st
F is with_proper_subsets & G c= F holds
G is with_proper_subsets
proof
let TS be TopStruct,
F, G being Subset-Family of TS;
assume
A1: F is with_proper_subsets & G c= F;
assume not G is with_proper_subsets;
then the carrier of TS in G by Def6;
hence thesis by A1,Def6;
end;
definition let TS be non empty TopStruct;
cluster with_proper_subsets Subset-Family of TS;
existence
proof
{ {} } is Subset-Family of TS by MEASURE1:9;
then reconsider F = { {} } as Subset-Family of TS;
take F;
assume the carrier of TS in F;
hence thesis by TARSKI:def 1;
end;
end;
theorem
for TS being non empty TopStruct,
A, B being with_proper_subsets Subset-Family of TS holds
A \/ B is with_proper_subsets
proof
let TS be non empty TopStruct,
A, B be with_proper_subsets Subset-Family of TS;
assume the carrier of TS in A \/ B;
then the carrier of TS in A or the carrier of TS in B by XBOOLE_0:def 2;
hence thesis by Def6;
end;
definition let T be TopStruct, F be Subset-Family of T;
attr F is open means :: TOPS_2:def 1
for P being Subset of T holds P in F implies P is open;
attr F is closed means :: TOPS_2:def 2
for P being Subset of T holds P in F implies P is closed;
end;
definition let T be TopSpace;
cluster open closed non empty Subset-Family of T;
existence
proof
reconsider F = {{}T} as Subset-Family of T by Th30;
A1: F is open
proof
let P be Subset of T;
assume P in F;
hence thesis by TARSKI:def 1;
end;
F is closed
proof
let P be Subset of T;
assume P in F;
hence thesis by TARSKI:def 1;
end;
hence thesis by A1;
end;
end;