:: On the Subcontinua of a Real Line
:: by Adam Grabowski
::
:: Received June 12, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, TARSKI, XBOOLE_0, ZFMISC_1, CARD_1, ARYTM_3, TOPMETR,
BORSUK_2, PRE_TOPC, XXREAL_0, XXREAL_1, SUBSET_1, RELAT_1, STRUCT_0,
TREAL_1, VALUED_1, FUNCT_1, BORSUK_1, ORDINAL2, GRAPH_1, ARYTM_1,
RELAT_2, XREAL_0, CONNSP_1, REAL_1, LIMFUNC1, METRIC_1, COMPLEX1, RAT_1,
POWER, IRRAT_1, INT_1, XCMPLX_0, RCOMP_1, PCOMPS_1, XXREAL_2, SEQ_4,
SETFAM_1, BORSUK_5, MEASURE5;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
XCMPLX_0, XREAL_0, ENUMSET1, FUNCT_1, FUNCT_2, XXREAL_2, MEASURE6,
STRUCT_0, INT_1, COMPLEX1, PRE_TOPC, TOPS_2, COMPTS_1, RCOMP_1, SEQ_4,
TREAL_1, CONNSP_1, BORSUK_2, TOPMETR, LIMFUNC1, IRRAT_1, RAT_1, MEASURE5,
METRIC_1, PCOMPS_1, XXREAL_0;
constructors COMPLEX1, PROB_1, LIMFUNC1, POWER, CONNSP_1, TOPS_2, COMPTS_1,
TREAL_1, MEASURE6, BORSUK_2, INTEGRA1, SEQ_4, BINOP_2, PCOMPS_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, XXREAL_0, XREAL_0,
INT_1, RAT_1, MEMBERED, STRUCT_0, PRE_TOPC, TOPS_1, METRIC_1, TOPMETR,
BORSUK_2, TOPREAL6, FCONT_3, RCOMP_1, MEASURE5, ORDINAL1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions XBOOLE_0, TARSKI, BORSUK_2;
equalities SUBSET_1, STRUCT_0, LIMFUNC1, PROB_1;
expansions TARSKI, BORSUK_2, TOPS_2, ZFMISC_1;
theorems BORSUK_1, PRE_TOPC, COMPTS_1, TARSKI, TOPMETR, RCOMP_1, CONNSP_1,
ZFMISC_1, JORDAN5A, XREAL_0, TREAL_1, XBOOLE_0, XBOOLE_1, SEQ_4,
INTEGRA1, FUNCT_2, TOPS_1, BORSUK_4, BORSUK_2, ENUMSET1, RAT_1, METRIC_1,
ABSVALUE, XCMPLX_1, CARD_2, INT_1, YELLOW_8, IRRAT_1, NUMBERS, XREAL_1,
SUBSET_1, GOBOARD6, XXREAL_0, XXREAL_1, XXREAL_2, MEASURE5;
begin :: Preliminaries
::$CT
reserve x1, x2, x3, x4, x5, x6, x7 for object;
theorem
{ x1, x2, x3, x4, x5, x6 } = { x1, x3, x6 } \/ { x2, x4, x5 }
proof
thus { x1, x2, x3, x4, x5, x6 } c= { x1, x3, x6 } \/ { x2, x4, x5 }
proof
let x be object;
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:def 4;
then x in { x1, x3, x6 } or x in { x2, x4, x5 } by ENUMSET1:def 1;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
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 3;
then x = x1 or x = x3 or x = x6 or x = x2 or x = x4 or x = x5
by ENUMSET1:def 1;
hence thesis by ENUMSET1:def 4;
end;
theorem Th2:
x1,x2,x3,x4,x5,x6 are_mutually_distinct implies card {x1,x2,x3,x4,x5,x6} = 6
proof
A1: {x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5} \/ {x6} by ENUMSET1:15;
assume
A2: x1, x2, x3, x4, x5, x6 are_mutually_distinct;
then x1, x2, x3, x4, x5 are_mutually_distinct;
then
A12: card {x1,x2,x3,x4,x5} = 5 by CARD_2:63;
A14: x2 <> x6 by A2;
A13: x3 <> x6 by A2;
A16: x4 <> x6 by A2;
A15: x5 <> x6 by A2;
x1 <> x6 by A2;
then not x6 in {x1,x2,x3,x4,x5} by A14,A13,A16,A15,ENUMSET1:def 3;
hence card {x1,x2,x3,x4,x5,x6} = 5+1 by A12,A1,CARD_2:41
.= 6;
end;
theorem
x1,x2,x3,x4,x5,x6,x7 are_mutually_distinct implies
card {x1,x2,x3,x4,x5,x6,x7} = 7
proof
A1: {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5,x6} \/ {x7} by ENUMSET1:21;
assume
A2: x1, x2, x3, x4, x5, x6, x7 are_mutually_distinct;
A7: x2 <> x7 by A2;
A6: x3 <> x7 by A2;
A5: x4 <> x7 by A2;
A4: x5 <> x7 by A2;
x1, x2, x3, x4, x5, x6 are_mutually_distinct by A2;
then
A21: card {x1,x2,x3,x4,x5,x6} = 6 by Th2;
A22: x6 <> x7 by A2;
x1 <> x7 by A2;
then not x7 in {x1,x2,x3,x4,x5,x6} by A7,A6,A5,A4,A22,ENUMSET1:def 4;
hence card {x1,x2,x3,x4,x5,x6,x7} = 6+1 by A21,A1,CARD_2:41
.= 7;
end;
theorem Th4:
{ 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 };
A2: x5 in { x4, x5, x6 } by ENUMSET1:def 1;
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
A3: x4 in { x1, x2, x3 } or x5 in { x1, x2, x3 } or x6 in { x1, x2, x3 }
by ENUMSET1:def 1;
A4: x6 in { x4, x5, x6 } by ENUMSET1:def 1;
x4 in { x4, x5, x6 } by ENUMSET1:def 1;
hence thesis by A1,A3,A2,A4,XBOOLE_0:3;
end;
theorem
x1, x2, x3 are_mutually_distinct & x4, x5, x6 are_mutually_distinct
& { x1, x2, x3 } misses { x4, x5, x6 } implies
x1, x2, x3, x4, x5, x6 are_mutually_distinct by Th4;
theorem
x1, x2, x3, x4, x5, x6 are_mutually_distinct &
{ x1, x2, x3, x4, x5, x6 } misses { x7 } implies
x1, x2, x3, x4, x5, x6, x7 are_mutually_distinct
proof
assume that
A1: x1, x2, x3, x4, x5, x6 are_mutually_distinct and
A2: { x1, x2, x3, x4, x5, x6 } misses { x7 };
A8: not x7 in { x1, x2, x3, x4, x5, x6 } by A2,ZFMISC_1:48;
then
A9: x7 <> x1 by ENUMSET1:def 4;
A22: x7 <> x3 by A8,ENUMSET1:def 4;
A21: x7 <> x4 by A8,ENUMSET1:def 4;
A20: x7 <> x5 by A8,ENUMSET1:def 4;
A18: x7 <> x6 by A8,ENUMSET1:def 4;
x7 <> x2 by A8,ENUMSET1:def 4;
hence thesis by A1,A9,A22,A21,A20,A18;
end;
theorem
x1, x2, x3, x4, x5, x6, x7 are_mutually_distinct implies
x7, x1, x2, x3, x4, x5, x6 are_mutually_distinct;
theorem
x1, x2, x3, x4, x5, x6, x7 are_mutually_distinct implies
x1, x2, x5, x3, x6, x7, x4 are_mutually_distinct;
Lm1: R^1 is pathwise_connected
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:17;
reconsider B as non empty Subset of R^1 by A1,XXREAL_1:1;
A2: Closed-Interval-TSpace(a,b) = R^1|B by A1,TOPMETR:19;
the carrier of R^1|B c= the carrier of R^1 by BORSUK_1:1;
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:7,TOPMETR:20;
reconsider g as Function of I[01], R^1;
take g;
L[01]((#)(a,b),(a,b)(#)) is continuous Function of I[01], R^1|B by A1,A2,
TOPMETR:20,TREAL_1:8;
hence g is continuous by PRE_TOPC:26;
0 = (#)(0,1) by TREAL_1:def 1;
hence g.0 = (#)(a,b) by A1,TREAL_1:9
.= a by A1,TREAL_1:def 1;
1 = (0,1)(#) by TREAL_1:def 2;
hence g.1 = (a,b)(#) by A1,TREAL_1:9
.= b by A1,TREAL_1:def 2;
end;
suppose
A3: b <= a;
reconsider B = [. b, a .] as Subset of R^1 by TOPMETR:17;
b in B by A3,XXREAL_1:1;
then reconsider B = [. b, a .] as non empty Subset of R^1;
A4: Closed-Interval-TSpace(b,a) = R^1|B by A3,TOPMETR:19;
the carrier of R^1|B c= the carrier of R^1 by BORSUK_1:1;
then reconsider g = L[01]((#)(b,a),(b,a)(#)) as Function of the carrier of
I[01], the carrier of R^1 by A4,FUNCT_2:7,TOPMETR:20;
reconsider g as Function of I[01], R^1;
0 = (#)(0,1) by TREAL_1:def 1;
then
A5: g.0 = (#)(b,a) by A3,TREAL_1:9
.= b by A3,TREAL_1:def 1;
1 = (0,1)(#) by TREAL_1:def 2;
then
A6: g.1 = (b,a)(#) by A3,TREAL_1:9
.= a by A3,TREAL_1:def 2;
L[01]((#)(b,a),(b,a)(#)) is continuous Function of I[01], R^1|B by A3,A4,
TOPMETR:20,TREAL_1:8;
then
A7: g is continuous by PRE_TOPC:26;
then b,a are_connected by A5,A6;
then reconsider P = g as Path of b, a by A7,A5,A6,BORSUK_2:def 2;
take -P;
ex t being Function of I[01], R^1 st t is continuous & t.0 = a & t.1
= b by A7,A5,A6,BORSUK_2:15;
then a,b are_connected;
hence thesis by BORSUK_2:def 2;
end;
end;
registration
cluster R^1 -> pathwise_connected;
coherence by Lm1;
end;
registration
cluster connected non empty for TopSpace;
existence
proof
take R^1;
thus thesis;
end;
end;
begin :: Intervals
theorem
for A, B being Subset of R^1, a, b, c, d being Real 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;
assume that
A1: a < b and
A2: b <= c and
A3: c < d and
A4: A = [. a, b .[ and
A5: B = ]. c, d .];
Cl ]. c, d .] = [. c, d .] by A3,BORSUK_4:11;
then Cl B = [. c, d .] by A5,JORDAN5A:24;
then
A6: Cl B misses A by A2,A4,XXREAL_1:95;
Cl [. a, b .[ = [. a, b .] by A1,BORSUK_4:12;
then Cl A = [. a, b .] by A4,JORDAN5A:24;
then Cl A misses B by A2,A5,XXREAL_1:90;
hence thesis by A6,CONNSP_1:def 1;
end;
theorem Th10:
for a, b, c being Real st a <= c & c <= b holds [.a,b.]
\/ [.c,+infty .[ = [.a,+infty .[
proof
let a, b, c be Real;
assume that
A1: a <= c and
A2: c <= b;
A3: [.a,+infty .[ c= [.a,b.] \/ [.c,+infty .[
proof
let r be object;
assume
A4: r in [.a,+infty .[;
then reconsider s = r as Real;
A5: a <= s by A4,XXREAL_1:236;
per cases;
suppose
s <= b;
then s in [.a,b.] by A5,XXREAL_1:1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
not s <= b;
then c <= s by A2,XXREAL_0:2;
then s in [.c,+infty .[ by XXREAL_1:236;
hence thesis by XBOOLE_0:def 3;
end;
end;
A6: [.a,b.] c= right_closed_halfline a by XXREAL_1:251;
[.c,+infty .[ c= [.a,+infty .[ by A1,XXREAL_1:38;
then [.a,b.] \/ [.c,+infty .[ c= [.a,+infty .[ by A6,XBOOLE_1:8;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem Th11:
for a, b, c being Real st a <= c & c <= b holds ]. -infty
, c .] \/ [. a, b .] = ]. -infty, b .]
proof
let a, b, c be Real;
assume that
A1: a <= c and
A2: c <= b;
thus ]. -infty, c .] \/ [. a, b .] c= ]. -infty, b .]
proof
let x be object;
assume
A3: x in ]. -infty, c .] \/ [. a, b .];
then reconsider x as Real;
per cases by A3,XBOOLE_0:def 3;
suppose
x in ]. -infty, c .];
then x <= c by XXREAL_1:234;
then x <= b by A2,XXREAL_0:2;
hence thesis by XXREAL_1:234;
end;
suppose
x in [. a, b .];
then x <= b by XXREAL_1:1;
hence thesis by XXREAL_1:234;
end;
end;
let x be object;
assume
A4: x in ]. -infty, b .];
then reconsider x as Real;
per cases;
suppose
x <= c;
then x in ]. -infty, c .] by XXREAL_1:234;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A5: x > c;
A6: x <= b by A4,XXREAL_1:234;
x > a by A1,A5,XXREAL_0:2;
then x in [. a, b .] by A6,XXREAL_1:1;
hence thesis by XBOOLE_0:def 3;
end;
end;
registration
cluster -> real for Element of RAT;
coherence;
end;
theorem
for A being Subset of R^1, p being Point of RealSpace holds p in Cl A
iff for r being Real st r > 0 holds Ball (p, r) meets A by GOBOARD6:92
,TOPMETR:def 6;
theorem Th13:
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 XREAL_1:48;
dist (p, q) = |.q - p.| by TOPMETR:11
.= q - p by A1,ABSVALUE:def 1;
hence thesis;
end;
theorem Th14:
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;
the carrier of R^1 c= Cl A
proof
let x be object;
assume x in the carrier of R^1;
then reconsider p = x as Element of RealSpace by METRIC_1:def 13,TOPMETR:17
;
now
let r be Real;
reconsider pr = p + r as Element of RealSpace by METRIC_1:def 13
,XREAL_0:def 1;
assume r > 0;
then consider Q being Rational such that
A2: p < Q and
A3: Q < pr by RAT_1:7,XREAL_1:29;
reconsider P = Q as Element of RealSpace by METRIC_1:def 13,XREAL_0:def 1
;
P - p < pr - p by A3,XREAL_1:9;
then dist (p, P) < r by A2,Th13;
then
A4: P in Ball (p, r) by METRIC_1:11;
Q in A by A1,RAT_1:def 2;
hence Ball (p, r) meets A by A4,XBOOLE_0:3;
end;
hence thesis by GOBOARD6:92,TOPMETR:def 6;
end;
hence thesis by XBOOLE_0:def 10;
end;
theorem Th15:
for A being Subset of R^1, a, b being Real st A = ]. a, b
.[ & a <> b holds Cl A = [. a, b .]
proof
let A be Subset of R^1, a, b be Real;
assume that
A1: A = ]. a, b .[ and
A2: a <> b;
Cl ]. a, b .[ = [. a, b .] by A2,JORDAN5A:26;
hence thesis by A1,JORDAN5A:24;
end;
begin :: Rational and Irrational Numbers
registration
cluster number_e -> irrational;
coherence by IRRAT_1:41;
end;
definition
func IRRAT -> Subset of REAL equals
REAL \ RAT;
coherence;
end;
definition
let a, b be Real;
func RAT (a, b) -> Subset of REAL equals
RAT /\ ]. a, b .[;
coherence;
func IRRAT (a, b) -> Subset of REAL equals
IRRAT /\ ]. a, b .[;
coherence;
end;
theorem Th16:
for x being Real holds x is irrational iff x in IRRAT
proof
let x be Real;
A1: x in REAL by XREAL_0:def 1;
hereby
assume x is irrational;
then not x in RAT;
hence x in IRRAT by A1,XBOOLE_0:def 5;
end;
assume x in IRRAT;
then not x in RAT by XBOOLE_0:def 5;
hence thesis by RAT_1:def 2;
end;
registration
cluster irrational for Real;
existence by IRRAT_1:41;
end;
registration
cluster IRRAT -> non empty;
coherence by Th16,IRRAT_1:41;
end;
registration
let a be Rational, b be irrational Real;
cluster a + b -> irrational;
coherence
proof
set m1 = the Integer;
assume a + b is rational;
then consider m, n being Integer such that
n > 0 and
A1: a + b = m / n by RAT_1:2;
a + b - a = (m*m1 - m1*n) / (m1*n) by A1;
hence thesis;
end;
cluster b + a -> irrational;
coherence;
end;
theorem
for a being Rational, b being irrational Real
holds a + b is irrational;
registration
let a be irrational Real;
cluster -a -> irrational;
coherence
proof
assume -a is rational;
then reconsider b = -a as Rational;
-b is rational;
hence thesis;
end;
end;
theorem
for a being irrational Real holds -a is irrational;
registration
let a be Rational, b be irrational Real;
cluster a - b -> irrational;
coherence
proof
a + -b is irrational;
hence thesis;
end;
cluster b - a -> irrational;
coherence
proof
b + -a is irrational;
hence thesis;
end;
end;
theorem
for a being Rational, b being irrational Real
holds a - b is irrational;
theorem
for a being Rational, b being irrational Real
holds b - a is irrational;
theorem Th21:
for a being Rational, b being irrational Real st
a <> 0 holds a * b is irrational
proof
let a be Rational, b be irrational Real;
assume
A1: a <> 0;
assume a * b is rational;
then consider m, n being Integer such that
n > 0 and
A2: a * b = m / n by RAT_1:2;
consider m1, n1 being Integer such that
n1 > 0 and
A3: a = m1 / n1 by RAT_1:2;
a * b / a = (m * n1) / (n * m1) by A2,A3,XCMPLX_1:84;
hence thesis by A1,XCMPLX_1:89;
end;
theorem Th22:
for a being Rational, b being irrational Real st
a <> 0 holds b / a is irrational
proof
let a be Rational, b be irrational Real;
assume
A1: a <> 0;
assume b / a is rational;
then reconsider c = b / a as Rational;
c * a is rational;
hence thesis by A1,XCMPLX_1:87;
end;
registration
cluster irrational -> non zero for Real;
coherence;
end;
theorem Th23:
for a being Rational, b being irrational Real st
a <> 0 holds a / b is irrational
proof
let a be Rational, b be irrational Real;
assume
A1: a <> 0;
assume a / b is rational;
then reconsider c = a / b as Rational;
c * b is irrational by A1,Th21,XCMPLX_1:50;
hence thesis by XCMPLX_1:87;
end;
registration
let r be irrational Real;
cluster frac r -> irrational;
coherence
proof
frac r = r - [\ r /] by INT_1:def 8;
hence thesis;
end;
end;
theorem
for r being irrational Real holds frac r is irrational;
registration
cluster non zero for Rational;
existence
proof
1 <> 0;
hence thesis;
end;
end;
registration
let a be non zero Rational, b be irrational Real;
cluster a * b -> irrational;
coherence by Th21;
cluster b * a -> irrational;
coherence;
cluster a / b -> irrational;
coherence by Th23;
cluster b / a -> irrational;
coherence by Th22;
end;
theorem Th25:
for a, b being Real st a < b ex p1, p2 being Rational
st a < p1 & p1 < p2 & p2 < b
proof
let a, b be Real;
assume a < b;
then consider p1 being Rational such that
A1: a < p1 and
A2: p1 < b by RAT_1:7;
ex p2 being Rational st p1 < p2 & p2 < b by A2,RAT_1:7;
hence thesis by A1;
end;
theorem Th26:
for a, b being Real st a < b ex p being irrational Real st a < p & p < b
proof
set x = frac number_e;
let a, b be Real;
A1: x < 1 by INT_1:43;
assume a < b;
then consider p1, p2 being Rational such that
A2: a < p1 and
A3: p1 < p2 and
A4: p2 < b by Th25;
set y = (1 - x) * p1 + x * p2;
A5: 0 < x by INT_1:43;
then y < p2 by A3,A1,XREAL_1:178;
then
A6: y < b by A4,XXREAL_0:2;
y > p1 by A3,A5,A1,XREAL_1:177;
then
A7: y > a by A2,XXREAL_0:2;
A8: y = p1 + x * (p2 - p1);
p2 - p1 <> 0 by A3;
hence thesis by A8,A6,A7;
end;
theorem Th27:
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;
the carrier of R^1 c= Cl A
proof
let x be object;
assume x in the carrier of R^1;
then reconsider p = x as Element of RealSpace by METRIC_1:def 13,TOPMETR:17
;
now
let r be Real;
reconsider pr = p + r as Element of RealSpace by METRIC_1:def 13
,XREAL_0:def 1;
assume r > 0;
then consider Q being irrational Real such that
A2: p < Q and
A3: Q < pr by Th26,XREAL_1:29;
reconsider P = Q as Element of RealSpace by METRIC_1:def 13,XREAL_0:def 1
;
P - p < pr - p by A3,XREAL_1:9;
then dist (p, P) < r by A2,Th13;
then
A4: P in Ball (p, r) by METRIC_1:11;
Q in A by A1,Th16;
hence Ball (p, r) meets A by A4,XBOOLE_0:3;
end;
hence thesis by GOBOARD6:92,TOPMETR:def 6;
end;
hence thesis by XBOOLE_0:def 10;
end;
Lm2: for A being Subset of R^1, a, b being Real 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;
assume that
A1: a < b and
A2: A = RAT (a, b);
thus a in Cl A
proof
reconsider a9 = a as Element of RealSpace by METRIC_1:def 13,XREAL_0:def 1;
for r being Real st r > 0 holds Ball (a9, r) meets A
proof
set p = a;
let r be Real;
reconsider pp = a + r as Element of RealSpace by METRIC_1:def 13
,XREAL_0:def 1;
set pr = min (pp, (p + b)/2);
A3: pr <= (p + b)/2 by XXREAL_0:17;
assume
A4: r > 0;
p < pr
proof
per cases by XXREAL_0:15;
suppose
pr = pp;
hence thesis by A4,XREAL_1:29;
end;
suppose
pr = (p + b)/2;
hence thesis by A1,XREAL_1:226;
end;
end;
then consider Q being Rational such that
A5: p < Q and
A6: Q < pr by RAT_1:7;
(p + b)/2 < b by A1,XREAL_1:226;
then pr < b by A3,XXREAL_0:2;
then Q < b by A6,XXREAL_0:2;
then
A7: Q in ]. a, b .[ by A5,XXREAL_1:4;
pr <= pp by XXREAL_0:17;
then
A8: pr - p <= pp - p by XREAL_1:9;
reconsider P = Q as Element of RealSpace by METRIC_1:def 13,XREAL_0:def 1
;
P - p < pr - p by A6,XREAL_1:9;
then P - p < r by A8,XXREAL_0:2;
then dist (a9, P) < r by A5,Th13;
then
A9: P in Ball (a9, r) by METRIC_1:11;
Q in RAT by RAT_1:def 2;
then Q in A by A2,A7,XBOOLE_0:def 4;
hence thesis by A9,XBOOLE_0:3;
end;
hence thesis by GOBOARD6:92,TOPMETR:def 6;
end;
b in Cl A
proof
reconsider a9 = b as Element of RealSpace by METRIC_1:def 13,XREAL_0:def 1;
for r being Real st r > 0 holds Ball (a9, r) meets A
proof
set p = b;
let r be Real;
reconsider pp = b - r as Element of RealSpace by METRIC_1:def 13
,XREAL_0:def 1;
set pr = max (pp, (p + a)/2);
A10: pr >= (p + a)/2 by XXREAL_0:25;
assume r > 0;
then
A11: b < b + r by XREAL_1:29;
p > pr
proof
per cases by XXREAL_0:16;
suppose
pr = pp;
hence thesis by A11,XREAL_1:19;
end;
suppose
pr = (p + a)/2;
hence thesis by A1,XREAL_1:226;
end;
end;
then consider Q being Rational such that
A12: pr < Q and
A13: Q < p by RAT_1:7;
(p + a)/2 > a by A1,XREAL_1:226;
then a < pr by A10,XXREAL_0:2;
then a < Q by A12,XXREAL_0:2;
then
A14: Q in ]. a, b .[ by A13,XXREAL_1:4;
pr >= pp by XXREAL_0:25;
then
A15: p - pr <= p - pp by XREAL_1:13;
reconsider P = Q as Element of RealSpace by METRIC_1:def 13,XREAL_0:def 1
;
p - P < p - pr by A12,XREAL_1:10;
then p - P < r by A15,XXREAL_0:2;
then dist (a9, P) < r by A13,Th13;
then
A16: P in Ball (a9, r) by METRIC_1:11;
Q in RAT by RAT_1:def 2;
then Q in A by A2,A14,XBOOLE_0:def 4;
hence thesis by A16,XBOOLE_0:3;
end;
hence thesis by GOBOARD6:92,TOPMETR:def 6;
end;
hence thesis;
end;
Lm3: for A being Subset of R^1, a, b being Real 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;
assume that
A1: a < b and
A2: A = IRRAT (a, b);
thus a in Cl A
proof
reconsider a9 = a as Element of RealSpace by METRIC_1:def 13,XREAL_0:def 1;
for r being Real st r > 0 holds Ball (a9, r) meets A
proof
set p = a;
let r be Real;
reconsider pp = a + r as Element of RealSpace by METRIC_1:def 13
,XREAL_0:def 1;
set pr = min (pp, (p + b)/2);
A3: pr <= (p + b)/2 by XXREAL_0:17;
assume
A4: r > 0;
p < pr
proof
per cases by XXREAL_0:15;
suppose
pr = pp;
hence thesis by A4,XREAL_1:29;
end;
suppose
pr = (p + b)/2;
hence thesis by A1,XREAL_1:226;
end;
end;
then consider Q being irrational Real such that
A5: p < Q and
A6: Q < pr by Th26;
(p + b)/2 < b by A1,XREAL_1:226;
then pr < b by A3,XXREAL_0:2;
then Q < b by A6,XXREAL_0:2;
then
A7: Q in ]. a, b .[ by A5,XXREAL_1:4;
pr <= pp by XXREAL_0:17;
then
A8: pr - p <= pp - p by XREAL_1:9;
reconsider P = Q as Element of RealSpace by METRIC_1:def 13,XREAL_0:def 1
;
P - p < pr - p by A6,XREAL_1:9;
then P - p < r by A8,XXREAL_0:2;
then dist (a9, P) < r by A5,Th13;
then
A9: P in Ball (a9, r) by METRIC_1:11;
Q in IRRAT by Th16;
then Q in A by A2,A7,XBOOLE_0:def 4;
hence thesis by A9,XBOOLE_0:3;
end;
hence thesis by GOBOARD6:92,TOPMETR:def 6;
end;
b in Cl A
proof
reconsider a9 = b as Element of RealSpace by METRIC_1:def 13,XREAL_0:def 1;
for r being Real st r > 0 holds Ball (a9, r) meets A
proof
set p = b;
let r be Real;
reconsider pp = b - r as Element of RealSpace by METRIC_1:def 13
,XREAL_0:def 1;
set pr = max (pp, (p + a)/2);
A10: pr >= (p + a)/2 by XXREAL_0:25;
assume r > 0;
then
A11: b < b + r by XREAL_1:29;
p > pr
proof
per cases by XXREAL_0:16;
suppose
pr = pp;
hence thesis by A11,XREAL_1:19;
end;
suppose
pr = (p + a)/2;
hence thesis by A1,XREAL_1:226;
end;
end;
then consider Q being irrational Real such that
A12: pr < Q and
A13: Q < p by Th26;
(p + a)/2 > a by A1,XREAL_1:226;
then a < pr by A10,XXREAL_0:2;
then a < Q by A12,XXREAL_0:2;
then
A14: Q in ]. a, b .[ by A13,XXREAL_1:4;
pr >= pp by XXREAL_0:25;
then
A15: p - pr <= p - pp by XREAL_1:13;
reconsider P = Q as Element of RealSpace by METRIC_1:def 13,XREAL_0:def 1
;
p - P < p - pr by A12,XREAL_1:10;
then p - P < r by A15,XXREAL_0:2;
then dist (a9, P) < r by A13,Th13;
then
A16: P in Ball (a9, r) by METRIC_1:11;
Q in IRRAT by Th16;
then Q in A by A2,A14,XBOOLE_0:def 4;
hence thesis by A16,XBOOLE_0:3;
end;
hence thesis by GOBOARD6:92,TOPMETR:def 6;
end;
hence thesis;
end;
theorem Th28:
for a, b, c being Real holds c in RAT (a,b) iff c is
rational & a < c & c < b
proof
let a, b, c be Real;
hereby
assume
A1: c in RAT (a,b);
then c in ]. a, b .[ by XBOOLE_0:def 4;
hence c is rational & a < c & c < b by A1,XXREAL_1:4;
end;
assume that
A2: c is rational and
A3: a < c and
A4: c < b;
A5: c in RAT by A2,RAT_1:def 2;
c in ]. a, b .[ by A3,A4,XXREAL_1:4;
hence thesis by A5,XBOOLE_0:def 4;
end;
theorem Th29:
for a, b, c being Real holds c in IRRAT (a,b) iff c is
irrational & a < c & c < b
proof
let a, b, c be Real;
hereby
assume
A1: c in IRRAT (a,b);
then
A2: c in ]. a, b .[ by XBOOLE_0:def 4;
c in IRRAT by A1,XBOOLE_0:def 4;
hence c is irrational & a < c & c < b by A2,Th16,XXREAL_1:4;
end;
assume that
A3: c is irrational and
A4: a < c and
A5: c < b;
A6: c in ]. a, b .[ by A4,A5,XXREAL_1:4;
c in IRRAT by A3,Th16;
hence thesis by A6,XBOOLE_0:def 4;
end;
theorem Th30:
for A being Subset of R^1, a, b being Real st a < b & A =
RAT (a, b) holds Cl A = [. a, b .]
proof
let A be Subset of R^1, a, b be Real;
assume that
A1: a < b and
A2: A = RAT (a, b);
reconsider ab = ]. a, b .[, RT = RAT as Subset of R^1 by NUMBERS:12
,TOPMETR:17;
reconsider RR = RAT /\ ]. a, b .[ as Subset of R^1 by TOPMETR:17;
A3: (the carrier of R^1) /\ Cl ab = Cl ab by XBOOLE_1:28;
A4: Cl RR c= (Cl RT) /\ Cl ab by PRE_TOPC:21;
thus Cl A c= [. a, b .]
proof
let x be object;
assume x in Cl A;
then x in (Cl RT) /\ Cl ab by A2,A4;
then x in (the carrier of R^1) /\ Cl ab by Th14;
hence thesis by A1,A3,Th15;
end;
thus [. a, b .] c= Cl A
proof
let x be object;
assume
A5: x in [. a, b .];
then reconsider p = x as Element of RealSpace by METRIC_1:def 13;
A6: a <= p by A5,XXREAL_1:1;
A7: p <= b by A5,XXREAL_1:1;
per cases by A7,XXREAL_0:1;
suppose
A8: p < b;
now
let r be Real;
reconsider pp = p + r as Element of RealSpace by METRIC_1:def 13
,XREAL_0:def 1;
set pr = min (pp, (p + b)/2);
A9: pr <= (p + b)/2 by XXREAL_0:17;
assume
A10: r > 0;
p < pr
proof
per cases by XXREAL_0:15;
suppose
pr = pp;
hence thesis by A10,XREAL_1:29;
end;
suppose
pr = (p + b)/2;
hence thesis by A8,XREAL_1:226;
end;
end;
then consider Q being Rational such that
A11: p < Q and
A12: Q < pr by RAT_1:7;
(p + b)/2 < b by A8,XREAL_1:226;
then pr < b by A9,XXREAL_0:2;
then
A13: Q < b by A12,XXREAL_0:2;
pr <= pp by XXREAL_0:17;
then
A14: pr - p <= pp - p by XREAL_1:9;
reconsider P = Q as Element of RealSpace by METRIC_1:def 13
,XREAL_0:def 1;
P - p < pr - p by A12,XREAL_1:9;
then P - p < r by A14,XXREAL_0:2;
then dist (p, P) < r by A11,Th13;
then
A15: P in Ball (p, r) by METRIC_1:11;
a < Q by A6,A11,XXREAL_0:2;
then
A16: Q in ]. a, b .[ by A13,XXREAL_1:4;
Q in RAT by RAT_1:def 2;
then Q in A by A2,A16,XBOOLE_0:def 4;
hence Ball (p, r) meets A by A15,XBOOLE_0:3;
end;
hence thesis by GOBOARD6:92,TOPMETR:def 6;
end;
suppose
p = b;
hence thesis by A1,A2,Lm2;
end;
end;
end;
theorem Th31:
for A being Subset of R^1, a, b being Real st a < b & A =
IRRAT (a, b) holds Cl A = [. a, b .]
proof
let A be Subset of R^1, a, b be Real;
assume that
A1: a < b and
A2: A = IRRAT (a, b);
reconsider ab = ]. a, b .[, RT = IRRAT as Subset of R^1 by TOPMETR:17;
reconsider RR = IRRAT /\ ]. a, b .[ as Subset of R^1 by TOPMETR:17;
A3: (the carrier of R^1) /\ Cl ab = Cl ab by XBOOLE_1:28;
A4: Cl RR c= (Cl RT) /\ Cl ab by PRE_TOPC:21;
thus Cl A c= [. a, b .]
proof
let x be object;
assume x in Cl A;
then x in (Cl RT) /\ Cl ab by A2,A4;
then x in (the carrier of R^1) /\ Cl ab by Th27;
hence thesis by A1,A3,Th15;
end;
thus [. a, b .] c= Cl A
proof
let x be object;
assume
A5: x in [. a, b .];
then reconsider p = x as Element of RealSpace by METRIC_1:def 13;
A6: a <= p by A5,XXREAL_1:1;
A7: p <= b by A5,XXREAL_1:1;
per cases by A7,XXREAL_0:1;
suppose
A8: p < b;
now
let r be Real;
reconsider pp = p + r as Element of RealSpace by METRIC_1:def 13
,XREAL_0:def 1;
set pr = min (pp, (p + b)/2);
A9: pr <= (p + b)/2 by XXREAL_0:17;
assume
A10: r > 0;
p < pr
proof
per cases by XXREAL_0:15;
suppose
pr = pp;
hence thesis by A10,XREAL_1:29;
end;
suppose
pr = (p + b)/2;
hence thesis by A8,XREAL_1:226;
end;
end;
then consider Q being irrational Real such that
A11: p < Q and
A12: Q < pr by Th26;
(p + b)/2 < b by A8,XREAL_1:226;
then pr < b by A9,XXREAL_0:2;
then
A13: Q < b by A12,XXREAL_0:2;
pr <= pp by XXREAL_0:17;
then
A14: pr - p <= pp - p by XREAL_1:9;
reconsider P = Q as Element of RealSpace by METRIC_1:def 13
,XREAL_0:def 1;
P - p < pr - p by A12,XREAL_1:9;
then P - p < r by A14,XXREAL_0:2;
then dist (p, P) < r by A11,Th13;
then
A15: P in Ball (p, r) by METRIC_1:11;
a < Q by A6,A11,XXREAL_0:2;
then
A16: Q in ]. a, b .[ by A13,XXREAL_1:4;
Q in IRRAT by Th16;
then Q in A by A2,A16,XBOOLE_0:def 4;
hence Ball (p, r) meets A by A15,XBOOLE_0:3;
end;
hence thesis by GOBOARD6:92,TOPMETR:def 6;
end;
suppose
p = b;
hence thesis by A1,A2,Lm3;
end;
end;
end;
theorem Th32:
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` <> {} by A2,PRE_TOPC:4;
A misses A` by SUBSET_1:24;
then
A4: A, A` are_separated by CONNSP_1:2;
A5: [#]T = A \/ A` by PRE_TOPC:2;
A <> {}T by A1;
then not [#]T is connected by A5,A4,A3,CONNSP_1:15;
hence thesis by CONNSP_1:27;
end;
theorem Th33:
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 Th32;
hence thesis by TOPMETR:17;
end;
begin :: Topological Properties of Intervals
theorem Th34:
for A being Subset of R^1, a, b being Real st A = [. a, b
.[ & a <> b holds Cl A = [. a, b .]
proof
let A be Subset of R^1, a, b be Real;
assume that
A1: A = [. a, b .[ and
A2: a <> b;
Cl [. a, b .[ = [. a, b .] by A2,BORSUK_4:12;
hence thesis by A1,JORDAN5A:24;
end;
theorem Th35:
for A being Subset of R^1, a, b being Real st A = ]. a, b
.] & a <> b holds Cl A = [. a, b .]
proof
let A be Subset of R^1, a, b be Real;
assume that
A1: A = ]. a, b .] and
A2: a <> b;
Cl ]. a, b .] = [. a, b .] by A2,BORSUK_4:11;
hence thesis by A1,JORDAN5A:24;
end;
theorem
for A being Subset of R^1, a, b, c being Real 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;
assume that
A1: A = [. a, b .[ \/ ]. b, c .] and
A2: a < b and
A3: b < c;
reconsider B = [. a, b .[, C = ]. b, c .] as Subset of R^1 by TOPMETR:17;
Cl A = Cl B \/ Cl C by A1,PRE_TOPC:20
.= [. a, b .] \/ Cl C by A2,Th34
.= [. a, b .] \/ [. b, c .] by A3,Th35
.= [. a, c .] by A2,A3,XXREAL_1:174;
hence thesis;
end;
theorem Th37:
for A being Subset of R^1, a being Real st A = {a} holds Cl A = {a}
proof
let A be Subset of R^1, a be Real;
A1: a is Point of R^1 by TOPMETR:17,XREAL_0:def 1;
assume A = {a};
hence thesis by A1,YELLOW_8:26;
end;
theorem Th38:
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:5;
then A in the topology of TopSpaceMetr RealSpace by TOPMETR:12;
hence B is open by A1,PRE_TOPC:def 2,TOPMETR:def 6;
end;
assume B is open;
then B in the topology of R^1 by PRE_TOPC:def 2;
then A in Family_open_set RealSpace by A1,TOPMETR:12,def 6;
hence thesis by JORDAN5A:5;
end;
Lm4: for a being Real holds ]. -infty,a.] is closed
proof
let a be Real;
]. -infty,a.] = left_closed_halfline a;
hence thesis;
end;
Lm5: for a being Real holds [.a,+infty .[ is closed
proof
let a be Real;
[. a,+infty .[ = right_closed_halfline a;
hence thesis;
end;
registration
let A, B be open Subset of REAL;
reconsider A1 = A, B1 = B as Subset of R^1 by TOPMETR:17;
cluster A /\ B -> open for Subset of REAL;
coherence
proof
A1: B1 is open by Th38;
A1 is open by Th38;
then A1 /\ B1 is open by A1;
hence thesis by Th38;
end;
cluster A \/ B -> open for Subset of REAL;
coherence
proof
A2: B1 is open by Th38;
A1 is open by Th38;
then A1 \/ B1 is open by A2;
hence thesis by Th38;
end;
end;
Lm6: for a,b being ExtReal holds ]. a,b .[ is open
proof
let a,b be ExtReal;
set A = ]. a,b .[;
per cases by XXREAL_0:14;
suppose
a in REAL & b in REAL;
then reconsider a, b as Real;
A = ].-infty,b.[ /\ ].a,+infty.[ by XXREAL_1:269;
hence thesis;
end;
suppose
a = +infty;
then A = {} by XXREAL_1:214;
hence thesis;
end;
suppose that
A1: a = -infty and
A2: b in REAL;
reconsider b as Real by A2;
A = left_open_halfline b by A1;
hence thesis;
end;
suppose that
A3: a in REAL and
A4: b = +infty;
reconsider a as Real by A3;
A = right_open_halfline a by A4;
hence thesis;
end;
suppose
b = -infty;
then A = {} by XXREAL_1:210;
hence thesis;
end;
suppose
a = -infty & b = +infty;
then A = [#]REAL by XXREAL_1:224;
hence thesis;
end;
end;
theorem Th39:
for A being Subset of R^1, a,b being ExtReal st A = ]. a
,b .[ holds A is open
proof
let A be Subset of R^1, a,b be ExtReal;
]. a,b .[ is open by Lm6;
hence thesis by Th38;
end;
theorem Th40:
for A being Subset of R^1, a being Real st A = ]. -infty,
a.] holds A is closed
proof
let A be Subset of R^1, a be Real;
assume
A1: A = ]. -infty,a.];
]. -infty,a.] is closed by Lm4;
hence thesis by A1,JORDAN5A:23;
end;
theorem Th41:
for A being Subset of R^1, a being Real st A = [. a,
+infty .[ holds A is closed
proof
let A be Subset of R^1, a be Real;
assume
A1: A = [. a,+infty .[;
[. a,+infty .[ is closed by Lm5;
hence thesis by A1,JORDAN5A:23;
end;
theorem Th42:
for a being Real holds [. a,+infty .[ = {a} \/ ]. a, +infty .[
proof
let a be Real;
thus [. a,+infty .[ c= {a} \/ ]. a,+infty .[
proof
let x be object;
assume
A1: x in [. a,+infty .[;
then reconsider x as Real;
A2: x >= a by A1,XXREAL_1:236;
per cases by A2,XXREAL_0:1;
suppose
x = a;
then x in {a} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x > a;
then x in ]. a,+infty .[ by XXREAL_1:235;
hence thesis by XBOOLE_0:def 3;
end;
end;
let x be object;
assume
A3: x in {a} \/ ]. a,+infty .[;
then reconsider x as Real;
x in {a} or x in ]. a,+infty .[ by A3,XBOOLE_0:def 3;
then x = a or x > a by TARSKI:def 1,XXREAL_1:235;
hence thesis by XXREAL_1:236;
end;
theorem Th43:
for a being Real holds ]. -infty,a.] = {a} \/ ]. -infty,a .[
proof
let a be Real;
thus ]. -infty,a.] c= {a} \/ ]. -infty,a.[
proof
let x be object;
assume
A1: x in ]. -infty,a.];
then reconsider x as Real;
A2: x <= a by A1,XXREAL_1:234;
per cases by A2,XXREAL_0:1;
suppose
x = a;
then x in {a} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x < a;
then x in ]. -infty,a.[ by XXREAL_1:233;
hence thesis by XBOOLE_0:def 3;
end;
end;
let x be object;
assume
A3: x in {a} \/ ]. -infty,a.[;
then reconsider x as Real;
x in {a} or x in ]. -infty,a.[ by A3,XBOOLE_0:def 3;
then x = a or x < a by TARSKI:def 1,XXREAL_1:233;
hence thesis by XXREAL_1:234;
end;
registration
let a be Real;
cluster ]. a,+infty .[ -> non empty;
coherence
proof
a < a + 1 by XREAL_1:29;
hence thesis by XXREAL_1:235;
end;
cluster ]. -infty,a .] -> non empty;
coherence by XXREAL_1:234;
cluster ]. -infty,a .[ -> non empty;
coherence
proof
a - 1 < a by XREAL_1:146;
hence thesis by XXREAL_1:233;
end;
cluster [. a,+infty .[ -> non empty;
coherence by XXREAL_1:236;
end;
theorem Th44:
for a being Real holds ]. a,+infty .[ <> REAL
by XREAL_0:def 1,XXREAL_1:235;
theorem
for a being Real holds [. a,+infty .[ <> REAL
proof
let a be Real;
A1: a - 1 < a by XREAL_1:146;
a - 1 in REAL by XREAL_0:def 1;
hence thesis by A1,XXREAL_1:236;
end;
theorem
for a being Real holds ]. -infty, a .] <> REAL
proof
let a be Real;
A1: a + 1 > a by XREAL_1:29;
a + 1 in REAL by XREAL_0:def 1;
hence thesis by A1,XXREAL_1:234;
end;
theorem Th47:
for a being Real holds ]. -infty, a .[ <> REAL
by XREAL_0:def 1,XXREAL_1:233;
theorem Th48:
for A being Subset of R^1, a being Real st A = ]. a,
+infty .[ holds Cl A = [. a,+infty .[
proof
let A be Subset of R^1, a be Real;
reconsider A9 = A as Subset of R^1;
reconsider C = [. a,+infty .[ as Subset of R^1 by TOPMETR:17;
assume
A1: A = ]. a,+infty .[;
then
A2: A9 is open by Th39;
C is closed by Th41;
then
A3: Cl A9 c= C by A1,TOPS_1:5,XXREAL_1:45;
A4: C = A9 \/ {a} by A1,Th42;
per cases by A4,A3,PRE_TOPC:18,ZFMISC_1:138;
suppose
Cl A9 = C;
hence thesis;
end;
suppose
Cl A9 = A9;
hence thesis by A1,A2,Th33,Th44;
end;
end;
theorem
for a being Real holds Cl ]. a,+infty .[ = [. a,+infty .[
proof
let a be Real;
reconsider A = ]. a,+infty .[ as Subset of R^1 by TOPMETR:17;
Cl A = [. a,+infty .[ by Th48;
hence thesis by JORDAN5A:24;
end;
theorem Th50:
for A being Subset of R^1, a being Real st A = ]. -infty,
a .[ holds Cl A = ]. -infty, a .]
proof
let A be Subset of R^1, a be Real;
reconsider A9 = A as Subset of R^1;
reconsider C = ]. -infty, a .] as Subset of R^1 by TOPMETR:17;
assume
A1: A = ]. -infty, a .[;
then
A2: A9 is open by Th39;
C is closed by Th40;
then
A3: Cl A9 c= C by A1,TOPS_1:5,XXREAL_1:41;
A4: C = A9 \/ {a} by A1,Th43;
per cases by A4,A3,PRE_TOPC:18,ZFMISC_1:138;
suppose
Cl A9 = C;
hence thesis;
end;
suppose
Cl A9 = A9;
hence thesis by A1,A2,Th33,Th47;
end;
end;
theorem
for a being Real holds Cl ]. -infty, a .[ = ]. -infty, a .]
proof
let a be Real;
reconsider A = ]. -infty, a .[ as Subset of R^1 by TOPMETR:17;
Cl A = ]. -infty, a .] by Th50;
hence thesis by JORDAN5A:24;
end;
theorem Th52:
for A, B being Subset of R^1, b being Real st A = ].
-infty, b .[ & B = ]. b,+infty .[ holds A, B are_separated
proof
let A, B be Subset of R^1, b be Real;
assume that
A1: A = ]. -infty, b .[ and
A2: B = ]. b,+infty .[;
Cl B = [. b,+infty .[ by A2,Th48;
then
A3: Cl B misses A by A1,XXREAL_1:94;
Cl A = ]. -infty, b .] by A1,Th50;
then Cl A misses B by A2,XXREAL_1:91;
hence thesis by A3,CONNSP_1:def 1;
end;
theorem
for A being Subset of R^1, a, b being Real 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;
assume that
A1: a < b and
A2: A = [. a, b .[ \/ ]. b,+infty .[;
reconsider B = [. a, b .[, C = ]. b,+infty .[ as Subset of R^1 by TOPMETR:17;
A3: Cl A = Cl B \/ Cl C by A2,PRE_TOPC:20;
A4: Cl C = [. b,+infty .[ by Th48;
Cl B = [. a, b .] by A1,Th34;
hence thesis by A1,A4,A3,Th10;
end;
theorem Th54:
for A being Subset of R^1, a, b being Real 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;
assume that
A1: a < b and
A2: A = ]. a, b .[ \/ ]. b,+infty .[;
reconsider B = ]. a, b .[, C = ]. b,+infty .[ as Subset of R^1 by TOPMETR:17;
A3: Cl A = Cl B \/ Cl C by A2,PRE_TOPC:20;
A4: Cl C = [. b,+infty .[ by Th48;
Cl B = [. a, b .] by A1,Th15;
hence thesis by A1,A3,A4,Th10;
end;
theorem
for A being Subset of R^1, a, b, c being Real 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;
assume that
A1: a < b and
A2: b < c;
reconsider B = RAT (a,b) as Subset of R^1 by TOPMETR:17;
reconsider C = ]. b, c .[ \/ ]. c,+infty .[ as Subset of R^1 by TOPMETR:17;
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:20;
then Cl A = Cl B \/ [. b,+infty .[ by A2,Th54;
then Cl A = [. a, b .] \/ [. b,+infty .[ by A1,Th30;
hence thesis by A1,Th10;
end;
theorem Th56:
for a, b being Real holds IRRAT (a, b) misses RAT (a, b)
proof
let a, b be Real;
assume IRRAT (a, b) meets RAT (a, b);
then consider x being object such that
A1: x in IRRAT (a, b) and
A2: x in RAT (a, b) by XBOOLE_0:3;
thus thesis by A1,A2,Th29;
end;
theorem Th57:
for a, b being Real holds REAL \ RAT (a, b) = ]. -infty,a
.] \/ IRRAT (a, b) \/ [.b,+infty .[
proof
let a, b be Real;
thus REAL \ RAT (a, b) c= ]. -infty,a.] \/ IRRAT (a, b) \/ [.b,+infty .[
proof
let x be object;
assume
A1: x in REAL \ RAT (a, b);
then
A2: not x in RAT (a, b) by XBOOLE_0:def 5;
reconsider x as Real by A1;
per cases;
suppose
x <= a & x < b;
then x in ]. -infty,a.] by XXREAL_1:234;
then x in ]. -infty,a.] \/ IRRAT (a, b) by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x <= a & x >= b;
then x in ]. -infty,a.] by XXREAL_1:234;
then x in ]. -infty,a.] \/ IRRAT (a, b) by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A3: x > a & x < b;
x in IRRAT (a, b)
proof
per cases;
suppose
x is rational;
hence thesis by A2,A3,Th28;
end;
suppose
x is irrational;
hence thesis by A3,Th29;
end;
end;
then x in ]. -infty,a.] \/ IRRAT (a, b) by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x > a & x >= b;
then x in [.b,+infty .[ by XXREAL_1:236;
hence thesis by XBOOLE_0:def 3;
end;
end;
let x be object;
assume
A4: x in ]. -infty,a.] \/ IRRAT (a, b) \/ [.b,+infty .[;
then reconsider x as Real;
A5: x in ]. -infty,a.] \/ IRRAT (a, b) or x in [.b,+infty .[ by A4,
XBOOLE_0:def 3;
per cases by A5,XBOOLE_0:def 3;
suppose
x in ]. -infty,a.];
then x <= a by XXREAL_1:234;
then
A6: not x in RAT (a, b) by Th28;
x in REAL by XREAL_0:def 1;
hence thesis by A6,XBOOLE_0:def 5;
end;
suppose
A7: x in IRRAT (a, b);
IRRAT (a, b) misses RAT (a, b) by Th56;
then
A8: not x in RAT (a,b) by A7,XBOOLE_0:3;
x in REAL by XREAL_0:def 1;
hence thesis by A8,XBOOLE_0:def 5;
end;
suppose
x in [.b,+infty .[;
then x >= b by XXREAL_1:236;
then
A9: not x in RAT (a, b) by Th28;
x in REAL by XREAL_0:def 1;
hence thesis by A9,XBOOLE_0:def 5;
end;
end;
theorem Th58:
for a, b being Real st a < b holds [.a,+infty .[ \ (]. a,
b .[ \/ ]. b,+infty .[) = {a} \/ {b}
proof
let a, b be Real;
A1: not b in ]. a,b .[ \/ ]. b,+infty .[ by XXREAL_1:205;
assume
A2: a < b;
then
A3: not a in ]. a,b .[ \/ ]. b,+infty .[ by XXREAL_1:223;
[. a,+infty .[ = [. a,b .] \/ [. b,+infty .[ by A2,Th10
.= {a, b} \/ ]. a,b .[ \/ [. b,+infty .[ by A2,XXREAL_1:128
.= {a, b} \/ ]. a,b .[ \/ ({b} \/ ]. b,+infty .[) by Th42
.= {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:9
.= {a, b} \/ (]. a,b .[ \/ ]. b,+infty .[) by XBOOLE_1:4;
then [.a,+infty .[ \ (]. a, b .[ \/ ]. b,+infty .[) = {a, b} by A3,A1,
XBOOLE_1:88,ZFMISC_1:51;
hence thesis by ENUMSET1:1;
end;
theorem
for A being Subset of R^1 st A = RAT (2,4) \/ ]. 4, 5 .[ \/ ]. 5,
+infty .[ holds A` = ]. -infty,2 .] \/ IRRAT(2,4) \/ {4} \/ {5}
proof
A1: ]. -infty,2.] \/ IRRAT (2, 4) c= ]. -infty,4.]
proof
let x be object;
assume
A2: x in ]. -infty,2.] \/ IRRAT (2, 4);
then reconsider x as Real;
per cases by A2,XBOOLE_0:def 3;
suppose
x in ]. -infty,2.];
then x <= 2 by XXREAL_1:234;
then x <= 4 by XXREAL_0:2;
hence thesis by XXREAL_1:234;
end;
suppose
x in IRRAT (2, 4);
then x < 4 by Th29;
hence thesis by XXREAL_1:234;
end;
end;
let A be Subset of R^1;
A3: ]. 4, 5 .[ \/ ]. 5,+infty .[ c= ]. 4,+infty .[
proof
let x be object;
assume
A4: x in ]. 4, 5 .[ \/ ]. 5,+infty .[;
then reconsider x as Real;
per cases by A4,XBOOLE_0:def 3;
suppose
x in ]. 4, 5 .[;
then x > 4 by XXREAL_1:4;
hence thesis by XXREAL_1:235;
end;
suppose
x in ]. 5,+infty .[;
then x > 5 by XXREAL_1:235;
then x > 4 by XXREAL_0:2;
hence thesis by XXREAL_1:235;
end;
end;
assume A = RAT (2,4) \/ ]. 4, 5 .[ \/ ]. 5,+infty .[;
then
A5: A` = REAL \ (RAT (2,4) \/ (]. 4, 5 .[ \/ ]. 5,+infty .[)) by TOPMETR:17
,XBOOLE_1:4
.= REAL \ RAT (2,4) \ (]. 4, 5 .[ \/ ]. 5,+infty .[) by XBOOLE_1:41
.= (]. -infty,2.] \/ IRRAT (2, 4) \/ [.4,+infty .[) \ (]. 4, 5 .[ \/ ].
5,+infty .[) by Th57;
]. -infty,4.] misses ]. 4,+infty .[ by XXREAL_1:91;
then
A` = ([.4,+infty .[ \ (]. 4, 5 .[ \/ ]. 5,+infty .[)) \/ (]. -infty,2.]
\/ IRRAT (2, 4)) by A5,A1,A3,XBOOLE_1:64,87
.= (]. -infty,2.] \/ IRRAT (2, 4)) \/ ({4} \/ {5}) by Th58
.= ]. -infty,2 .] \/ IRRAT(2,4) \/ {4} \/ {5} by XBOOLE_1:4;
hence thesis;
end;
theorem
for A being Subset of R^1, a being Real st A = {a} holds A` =
]. -infty, a .[ \/ ]. a,+infty .[ by TOPMETR:17,XXREAL_1:389;
Lm7: IRRAT(2,4) \/ {4} \/ {5} c= ]. 1,+infty .[
proof
let x be object;
assume
A1: x in IRRAT(2,4) \/ {4} \/ {5};
then reconsider x as Real;
A2: x in IRRAT(2,4) \/ {4} or x in {5} by A1,XBOOLE_0:def 3;
per cases by A2,XBOOLE_0:def 3;
suppose
x in IRRAT(2,4);
then x > 2 by Th29;
then x > 1 by XXREAL_0:2;
hence thesis by XXREAL_1:235;
end;
suppose
x in {4};
then x = 4 by TARSKI:def 1;
hence thesis by XXREAL_1:235;
end;
suppose
x in {5};
then x = 5 by TARSKI:def 1;
hence thesis by XXREAL_1:235;
end;
end;
Lm8: ]. 1,+infty .[ c= [. 1,+infty .[ by XXREAL_1:45;
Lm9: ]. -infty, 1 .[ /\ (]. -infty, 2 .] \/ IRRAT(2,4) \/ {4} \/ {5}) = ].
-infty, 1 .[
proof
A1: ]. -infty, 1 .[ c= ]. -infty, 2 .]
proof
let x be object;
assume
A2: x in ]. -infty, 1 .[;
then reconsider x as Real;
x < 1 by A2,XXREAL_1:233;
then x < 2 by XXREAL_0:2;
hence thesis by XXREAL_1:234;
end;
[. 1,+infty .[ misses ]. -infty, 1 .[ by XXREAL_1:94;
then
A3: IRRAT(2,4) \/ {4} \/ {5} misses ]. -infty, 1 .[ by Lm7,Lm8,XBOOLE_1:1,63;
]. -infty, 1 .[ /\ (]. -infty, 2 .] \/ IRRAT(2,4) \/ {4} \/ {5}) = ].
-infty, 1 .[ /\ (]. -infty, 2 .] \/ (IRRAT(2,4) \/ {4} \/ {5})) by XBOOLE_1:113
.= ]. -infty, 1 .[ /\ ]. -infty, 2 .] by A3,XBOOLE_1:78
.= ]. -infty, 1 .[ by A1,XBOOLE_1:28;
hence thesis;
end;
Lm10: ]. 1,+infty .[ /\ (]. -infty, 2 .] \/ IRRAT(2,4) \/ {4} \/ {5}) = ]. 1,
2 .] \/ IRRAT(2,4) \/ {4} \/ {5}
proof
]. 1,+infty .[ /\ (]. -infty, 2 .] \/ IRRAT(2,4) \/ {4} \/ {5}) = ]. 1,
+infty .[ /\ (]. -infty, 2 .] \/ (IRRAT(2,4) \/ {4} \/ {5})) by XBOOLE_1:113
.= (]. 1,+infty .[ /\ ]. -infty, 2 .]) \/ (]. 1,+infty .[ /\ (IRRAT(2,4)
\/ {4} \/ {5})) by XBOOLE_1:23
.= (]. 1,+infty .[ /\ ]. -infty, 2 .]) \/ (IRRAT(2,4) \/ {4} \/ {5}) by Lm7
,XBOOLE_1:28
.= ]. 1,2 .] \/ (IRRAT(2,4) \/ {4} \/ {5}) by XXREAL_1:270
.= ]. 1,2 .] \/ IRRAT(2,4) \/ {4} \/ {5} by XBOOLE_1:113;
hence thesis;
end;
theorem
(]. -infty, 1 .[ \/ ]. 1,+infty .[) /\ (]. -infty, 2 .] \/ IRRAT(2,4)
\/ {4} \/ {5}) = ]. -infty, 1 .[ \/ ]. 1, 2 .] \/ IRRAT(2,4) \/ {4} \/ {5}
proof
(]. -infty, 1 .[ \/ ]. 1,+infty .[) /\ (]. -infty, 2 .] \/ IRRAT(2,4) \/
{4} \/ {5}) = ]. -infty, 1 .[ \/ (]. 1,+infty .[ /\ (]. -infty, 2 .] \/ IRRAT(2
,4) \/ {4} \/ {5})) by Lm9,XBOOLE_1:23
.= ]. -infty, 1 .[ \/ (]. 1, 2 .] \/ IRRAT(2,4) \/ ({4} \/ {5})) by Lm10,
XBOOLE_1:4
.= ]. -infty, 1 .[ \/ ]. 1, 2 .] \/ IRRAT(2,4) \/ ({4} \/ {5}) by
XBOOLE_1:113;
hence thesis by XBOOLE_1:4;
end;
theorem
for A being Subset of R^1, a, b being Real 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;
assume that
A1: a <= b and
A2: A = {a} \/ [. b,+infty .[;
A` = (REAL \ [. b,+infty .[) \ {a} by A2,TOPMETR:17,XBOOLE_1:41
.= ]. -infty,b.[ \ {a} by XXREAL_1:224,294;
hence thesis by A1,XXREAL_1:349;
end;
theorem
for A being Subset of R^1, a, b being Real 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;
assume that
A1: a < b and
A2: A = ]. -infty, a .[ \/ ]. a, b .[;
reconsider B = ]. -infty, a .[, C = ]. a, b .[ as Subset of R^1 by TOPMETR:17
;
A3: Cl C = [. a, b .] by A1,Th15;
Cl A = Cl B \/ Cl C by A2,PRE_TOPC:20
.= ]. -infty, a .] \/ [. a, b .] by A3,Th50
.= ]. -infty, b .] by A1,Th11;
hence thesis;
end;
theorem Th64:
for A being Subset of R^1, a, b being Real 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;
assume that
A1: a < b and
A2: A = ]. -infty, a .[ \/ ]. a, b .];
reconsider B = ]. -infty, a .[, C = ]. a, b .] as Subset of R^1 by TOPMETR:17
;
A3: Cl C = [. a, b .] by A1,Th35;
Cl A = Cl B \/ Cl C by A2,PRE_TOPC:20
.= ]. -infty, a .] \/ [. a, b .] by A3,Th50
.= ]. -infty, b .] by A1,Th11;
hence thesis;
end;
theorem Th65:
for A being Subset of R^1, a, b, c being Real 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;
assume that
A1: a < b and
A2: b < c and
A3: 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:17;
A4: c in ]. -infty, c .] by XXREAL_1:234;
Cl A = Cl (B \/ C \/ D) \/ Cl E by A3,PRE_TOPC:20
.= Cl (B \/ C \/ D) \/ E by Th37
.= Cl (B \/ C) \/ Cl D \/ E by PRE_TOPC:20
.= ]. -infty, b .] \/ Cl D \/ E by A1,Th64
.= ]. -infty, b .] \/ [. b,c .] \/ E by A2,Th31
.= ]. -infty, c .] \/ E by A2,Th11
.= ]. -infty, c .] by A4,ZFMISC_1:40;
hence thesis;
end;
theorem
for A being Subset of R^1, a, b, c, d being Real 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;
assume that
A1: a < b and
A2: b < c and
A3: 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:17;
Cl A = Cl (B \/ C \/ D \/ E) \/ Cl F by A3,PRE_TOPC:20
.= Cl (B \/ C \/ D \/ E) \/ {d} by Th37;
hence thesis by A1,A2,Th65;
end;
theorem
for A being Subset of R^1, a, b being Real 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;
assume that
A1: a <= b and
A2: A = ]. -infty, a .] \/ {b};
A` = (REAL \ ]. -infty, a .]) \ {b} by A2,TOPMETR:17,XBOOLE_1:41
.= ]. a,+infty .[ \ {b} by XXREAL_1:224,288
.= ]. a, b .[ \/ ]. b,+infty .[ by A1,XXREAL_1:365;
hence thesis;
end;
theorem
for a, b being Real holds [. a,+infty .[ \/ {b} <> REAL
proof
let a, b be Real;
set ab = min (a,b) - 1;
A1: ab < min (a,b) by XREAL_1:146;
min (a,b) <= b by XXREAL_0:17;
then
A2: not ab in {b} by A1,TARSKI:def 1;
min (a,b) <= a by XXREAL_0:17;
then ab < a by XREAL_1:146,XXREAL_0:2;
then
A3: not ab in [. a,+infty .[ by XXREAL_1:236;
ab in REAL by XREAL_0:def 1;
hence thesis by A3,A2,XBOOLE_0:def 3;
end;
theorem
for a, b being Real holds ]. -infty, a .] \/ {b} <> REAL
proof
let a, b be Real;
set ab = max (a,b) + 1;
A1: ab > max (a,b) by XREAL_1:29;
max (a,b) >= a by XXREAL_0:25;
then ab > a by A1,XXREAL_0:2;
then
A2: not ab in ]. -infty, a.] by XXREAL_1:234;
max (a,b) >= b by XXREAL_0:25;
then
A3: not ab in {b} by A1,TARSKI:def 1;
ab in REAL by XREAL_0:def 1;
hence thesis by A2,A3,XBOOLE_0:def 3;
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
reconsider AB = {}R^1 as Subset of R^1;
let A be Subset of R^1;
assume REAL = A`;
then AB` = A` by TOPMETR:17;
then AB = A``;
hence thesis;
end;
begin :: Subcontinua of a real line
theorem Th72:
for X being compact Subset of R^1, X9 being Subset of REAL st
X9 = X holds X9 is bounded_above bounded_below
proof
let X be compact Subset of R^1, X9 be Subset of REAL;
assume X9 = X;
then X9 is compact by JORDAN5A:25;
then X9 is real-bounded by RCOMP_1:10;
hence thesis by XXREAL_2:def 11;
end;
theorem Th73:
for X being compact Subset of R^1, X9 being Subset of REAL, x
being Real st x in X9 & X9 = X holds lower_bound X9 <= x &
x <= upper_bound X9
proof
let X be compact Subset of R^1, X9 be Subset of REAL, x be Real;
assume that
A1: x in X9 and
A2: X9 = X;
X9 is bounded_above bounded_below by A2,Th72;
hence thesis by A1,SEQ_4:def 1,def 2;
end;
theorem Th74:
for C being non empty compact connected Subset of R^1, C9 being
Subset of REAL st C = C9 & [. lower_bound C9, upper_bound C9 .] c= C9
holds [. lower_bound C9, upper_bound C9.] = C9
proof
let C be non empty compact connected Subset of R^1, C9 be Subset of REAL;
assume that
A1: C = C9 and
A2: [. lower_bound C9, upper_bound C9 .] c= C9;
assume [. lower_bound C9, upper_bound C9 .] <> C9;
then not C9 c= [. lower_bound C9, upper_bound C9 .] by A2,XBOOLE_0:def 10;
then consider c being object such that
A3: c in C9 and
A4: not c in [. lower_bound C9, upper_bound C9 .];
reconsider c as Real by A3;
A5: c <= upper_bound C9 by A1,A3,Th73;
lower_bound C9 <= c by A1,A3,Th73;
hence thesis by A4,A5,XXREAL_1:1;
end;
theorem Th75:
for A being connected Subset of R^1, a, b, c being Real
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;
assume that
A1: a <= b and
A2: b <= c and
A3: a in A and
A4: c in A;
per cases by A1,A2,A3,A4,XXREAL_0:1;
suppose
a = b or b = c;
hence thesis by A3,A4;
end;
suppose
A5: a < b & b < c & a in A & c in A;
reconsider B = ]. -infty,b .[, C = ]. b,+infty .[ as Subset of R^1 by
TOPMETR:17;
assume not b in A;
then A c= REAL \ {b} by TOPMETR:17,ZFMISC_1:34;
then
A6: A c= ]. -infty,b .[ \/ ]. b,+infty .[ by XXREAL_1:389;
now
per cases by A6,Th52,CONNSP_1:16;
suppose
A c= B;
hence contradiction by A5,XXREAL_1:233;
end;
suppose
A c= C;
hence contradiction by A5,XXREAL_1:235;
end;
end;
hence thesis;
end;
end;
theorem Th76:
for A being connected Subset of R^1, a, b being Real 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;
assume that
A1: a in A and
A2: b in A;
let x be object;
assume x in [.a,b.];
then x in { y where y is Real: a <= y & y <= b } by RCOMP_1:def 1;
then ex z being Real st z = x & a <= z & z <= b;
hence thesis by A1,A2,Th75;
end;
theorem Th77:
for X being non empty compact connected Subset of R^1 holds X
is non empty non empty closed_interval Subset of REAL
proof
let C be non empty compact connected Subset of R^1;
reconsider C9 = C as non empty Subset of REAL by TOPMETR:17;
C is closed by COMPTS_1:7;
then
A1: C9 is closed by JORDAN5A:23;
then
A2: upper_bound C9 in C9 by Th72,RCOMP_1:12;
C9 is bounded_below bounded_above by Th72;
then C9 is real-bounded by XXREAL_2:def 11;
then
A3: lower_bound C9 <= upper_bound C9 by SEQ_4:11;
lower_bound C9 in C9 by A1,Th72,RCOMP_1:13;
then [. lower_bound C9, upper_bound C9 .] = C9 by A2,Th74,Th76;
then C9 is non empty closed_interval by A3,MEASURE5:14;
hence thesis;
end;
theorem
for A being non empty compact connected Subset of R^1 holds ex a, b
being Real st a <= b & A = [. a, b .]
proof
let C be non empty compact connected Subset of R^1;
reconsider C9 = C as non empty closed_interval Subset of REAL by Th77;
A1: lower_bound C9 <= upper_bound C9 by BORSUK_4:28;
A2: C9 = [. lower_bound C9, upper_bound C9 .] by INTEGRA1:4;
then
A3: upper_bound C9 in C by A1,XXREAL_1:1;
lower_bound C9 in C by A2,A1,XXREAL_1:1;
then reconsider p1 = lower_bound C9, p2 = upper_bound C9 as Point of R^1
by A3;
take p1, p2;
thus p1 <= p2 by BORSUK_4:28;
thus thesis by INTEGRA1:4;
end;
registration
let T be TopSpace;
cluster open closed non empty for Subset-Family of T;
existence
proof
reconsider F = {{}T} as Subset-Family of T by ZFMISC_1:31;
A1: F is closed
by TARSKI:def 1;
F is open
by TARSKI:def 1;
hence thesis by A1;
end;
end;