:: Compactness of the Bounded Closed Subsets of TOP-REAL 2
:: by Artur Korni{\l}owicz
::
:: Received February 19, 1999
:: Copyright (c) 1999-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, REAL_1, SUBSET_1, XBOOLE_0, METRIC_1, PRE_TOPC, EUCLID,
CARD_1, XXREAL_0, SQUARE_1, ARYTM_3, RELAT_1, COMPLEX1, ARYTM_1, CARD_3,
FINSEQ_2, FINSEQ_1, NAT_1, FUNCT_1, NEWTON, RVSUM_1, TARSKI, XXREAL_1,
ORDINAL2, XXREAL_2, FINSET_1, RELAT_2, CONNSP_1, T_0TOPSP, TOPS_2,
SETFAM_1, RCOMP_1, ZFMISC_1, STRUCT_0, FUNCOP_1, SUPINF_2, MCART_1,
RLTOPSP1, PSCOMP_1, SPPOL_1, TOPREAL4, CONVEX1, TOPREAL1, TOPREAL2,
SPRECT_1, PCOMPS_1, SEQ_1, SEQ_2, TOPMETR, PARTFUN1, CONNSP_2, TOPS_1,
BORSUK_1, SEQ_4, FUNCT_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1, FINSET_1, ORDINAL1,
NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, SQUARE_1, NAT_1, NAT_D,
FUNCOP_1, FUNCT_4, SEQ_1, SEQ_2, SEQ_4, STRUCT_0, METRIC_1, TBSP_1,
FINSEQ_1, FINSEQ_2, RVSUM_1, NEWTON, XXREAL_0, XXREAL_2, CARD_3,
FINSEQ_4, RCOMP_1, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_1, CONNSP_2,
COMPTS_1, BORSUK_1, MEASURE6, PCOMPS_1, RLVECT_1, RLTOPSP1, EUCLID,
WEIERSTR, TOPMETR, TOPREAL1, TOPREAL2, T_0TOPSP, TOPREAL4, PSCOMP_1,
SPPOL_1, SPRECT_1;
constructors SETFAM_1, FUNCT_3, REAL_1, SQUARE_1, NAT_1, CARD_3, FINSEQOP,
RCOMP_1, FINSEQ_4, FINSOP_1, NEWTON, NAT_D, TOPS_1, CONNSP_1, TOPS_2,
COMPTS_1, TBSP_1, T_0TOPSP, MONOID_0, TOPREAL1, TOPREAL2, TOPREAL4,
SPPOL_1, JORDAN1, PSCOMP_1, WEIERSTR, SPRECT_1, JORDAN2C, XXREAL_2,
SEQ_4, FUNCSDOM, CONVEX1, BINOP_2, SEQ_2, MEASURE6, PCOMPS_1, COMSEQ_2;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_4, FINSET_1,
NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, MEMBERED, FINSEQ_1, RCOMP_1,
STRUCT_0, PRE_TOPC, TOPS_1, COMPTS_1, METRIC_1, PCOMPS_1, BORSUK_1,
TEX_4, MONOID_0, EUCLID, TOPMETR, JORDAN1, PSCOMP_1, GOBOARD9, WAYBEL_2,
JORDAN2C, VALUED_0, XXREAL_2, RLTOPSP1, TBSP_1, SPRECT_1, FUNCT_2,
JORDAN5A, NEWTON, RVSUM_1, NAT_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, FUNCT_1, TOPS_2, CONNSP_1, BORSUK_1, SPPOL_1, T_0TOPSP,
TOPREAL2, XBOOLE_0, JORDAN1, XXREAL_2;
equalities SUBSET_1, BORSUK_1, BINOP_1, EUCLID, SQUARE_1, STRUCT_0, FINSEQ_2,
RLTOPSP1;
expansions TARSKI, FUNCT_1, TOPS_2, CONNSP_1, SPPOL_1, T_0TOPSP, XBOOLE_0,
XXREAL_2;
theorems ABSVALUE, BORSUK_1, BORSUK_3, CARD_3, FUNCT_4, COMPTS_1, CONNSP_1,
CONNSP_2, EUCLID, FINSEQ_1, FINSEQ_2, FUNCT_1, FUNCT_2, FUNCT_3,
GOBOARD6, GOBOARD7, JGRAPH_1, JORDAN1, JORDAN2C, JORDAN5A, JORDAN6,
METRIC_1, METRIC_6, NEWTON, NAT_1, PCOMPS_1, PRE_TOPC, PREPOWER,
PSCOMP_1, RCOMP_1, RELAT_1, RVSUM_1, SEQ_4, SPRECT_1, SQUARE_1, SUBSET_1,
TARSKI, TBSP_1, TOPMETR, TOPREAL1, TOPREAL3, TOPREAL4, TOPS_1, TOPS_2,
WEIERSTR, YELLOW12, ZFMISC_1, XREAL_0, FUNCOP_1, XBOOLE_0, XBOOLE_1,
XCMPLX_1, COMPLEX1, XREAL_1, XXREAL_0, XXREAL_1, XXREAL_2, NAT_D,
VALUED_1, MEASURE6, RLTOPSP1, ORDINAL1, RLVECT_1;
schemes FINSET_1, NAT_1, BINOP_1;
begin :: Real numbers
reserve a, b for Real,
r for Real,
rr for Real,
i, j, n for Nat,
M for non empty MetrSpace,
p, q, s for Point of TOP-REAL 2,
e for Point of Euclid 2,
w for Point of Euclid n,
z for Point of M,
A, B for Subset of TOP-REAL n,
P for Subset of TOP-REAL 2,
D for non empty Subset of TOP-REAL 2;
::$CT
theorem Th1:
0 <= a & a <= b implies |.a.| <= |.b.|
proof
assume that
A1: 0 <= a and
A2: a <= b;
|.a.| = a by A1,ABSVALUE:def 1;
hence thesis by A1,A2,ABSVALUE:def 1;
end;
theorem Th2:
b <= a & a <= 0 implies |.a.| <= |.b.|
proof
assume that
A1: b <= a and
A2: a <= 0;
per cases by A2;
suppose
a = 0;
then |.a.| = 0 by ABSVALUE:2;
hence thesis by COMPLEX1:46;
end;
suppose
A3: a < 0;
then
A4: |.a.| = -a by ABSVALUE:def 1;
|.b.| = -b by A1,A3,ABSVALUE:def 1;
hence thesis by A1,A4,XREAL_1:24;
end;
end;
theorem
Product(0|->rr) = 1
by RVSUM_1:94;
theorem Th4:
Product(1|->rr) = rr
proof
thus Product(1|->rr) = Product<*rr*> by FINSEQ_2:59
.= rr;
end;
theorem
Product(2|->rr) = rr * rr
proof
thus Product(2|->rr) = Product<*rr,rr*> by FINSEQ_2:61
.= rr * rr by RVSUM_1:99;
end;
theorem Th6:
Product((n+1) |-> rr) = (Product(n|->rr))*rr
proof
thus Product((n+1) |->rr) = (Product(n|->rr))*(Product(1|->rr))
by RVSUM_1:104
.= (Product(n|->rr))*rr by Th4;
end;
theorem Th7:
j <> 0 & rr = 0 iff Product(j|->rr) = 0
proof
set f = j|->rr;
A1: dom f = Seg j by FUNCOP_1:13;
hereby
assume that
A2: j <> 0 and
A3: rr = 0;
ex n be Nat st j = n + 1 by A2,NAT_1:6;
then 1 <= j by NAT_1:11;
then
A4: 1 in Seg j by FINSEQ_1:1;
then f.1 = 0 by A3,FUNCOP_1:7;
hence Product f = 0 by A1,A4,RVSUM_1:103;
end;
assume Product f = 0;
then ex n being Nat st n in dom f & f.n = 0 by RVSUM_1:103;
hence thesis by A1,FUNCOP_1:7;
end;
theorem Th8:
rr <> 0 & j <= i implies Product((i-'j) |-> rr) = Product(i|->rr) /
Product(j|->rr)
proof
assume that
A1: rr <> 0 and
A2: j <= i;
defpred P[Nat] means j <= $1
implies Product(($1-'j) |-> rr) =
Product($1|->rr) / Product(j|->rr);
A3: Product(j|->rr) <> 0 by A1,Th7;
A4: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume that
A5: P[n] and
A6: j <= n+1;
per cases by A6,NAT_1:8;
suppose
A7: j <= n;
Product((n-'j+1) |-> rr) = Product((n-'j) |-> rr)*Product(1|->rr)
by RVSUM_1:104
.= Product(n|->rr) / Product(j|->rr) * rr by A5,A7,Th4
.= Product(n|->rr) * rr / Product(j|->rr) by XCMPLX_1:74
.= Product((n+1) |-> rr) / Product(j|->rr) by Th6;
hence thesis by A7,NAT_D:38;
end;
suppose
A8: j = n+1;
hence Product(((n+1)-'j) |-> rr) = Product(0|->rr) by XREAL_1:232
.= 1 by RVSUM_1:94
.= Product((n+1) |-> rr) / Product(j|->rr) by A3,A8,XCMPLX_1:60;
end;
end;
A9: P[0]
proof
assume
A10: j <= 0;
then j = 0;
hence Product((0-'j) |-> rr) = Product(0|->rr) / Product<*>REAL by NAT_D:40
,RVSUM_1:94
.= Product(0|->rr) / Product(j|->rr) by A10;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A9,A4);
hence thesis by A2;
end;
theorem
r <> 0 & j <= i implies r|^(i-'j) = r|^i / r|^j
proof
assume that
A1: r <> 0 and
A2: j <= i;
reconsider rr=r as Real;
thus r|^i / r|^j = (Product(i |-> rr)) / rr|^j by NEWTON:def 1
.= (Product(i |-> rr)) / (Product(j |-> rr)) by NEWTON:def 1
.= Product((i-'j) |-> rr) by A1,A2,Th8
.= r|^(i-'j) by NEWTON:def 1;
end;
reserve a, b for Real;
theorem Th10:
for a,b being Real holds sqr <*a,b*> = <*a^2,b^2*>
proof let a,b be Real;
dom sqrreal = REAL by FUNCT_2:def 1;
then
A1: rng <*a,b*> c= dom sqrreal;
A2: dom <*a^2,b^2*> = {1,2} by FINSEQ_1:2,89;
A3: for i being object st i in dom <*a^2,b^2*> holds (sqr <*a,b*>).i = <*a^2,b
^2*>.i
proof
let i be object;
A4: <*a,b*>.1 = a;
A5: <*a,b*>.2 = b;
assume
A6: i in dom <*a^2,b^2*>;
per cases by A2,A6,TARSKI:def 2;
suppose
A7: i = 1;
hence (sqr <*a,b*>).i = a^2 by A4,VALUED_1:11
.= <*a^2,b^2*>.i by A7;
end;
suppose
A8: i = 2;
hence (sqr <*a,b*>).i = b^2 by A5,VALUED_1:11
.= <*a^2,b^2*>.i by A8;
end;
end;
dom sqr <*a,b*> = dom (sqrreal*<*a,b*>) by RVSUM_1:def 8
.= dom <*a,b*> by A1,RELAT_1:27
.= {1,2} by FINSEQ_1:2,89;
hence thesis by A3,FINSEQ_1:2,89,FUNCT_1:2;
end;
theorem Th11:
for i be Nat for F being FinSequence of REAL st i in dom abs F &
a = F.i holds (abs F).i = |.a.|
proof
let i be Nat;
let F be FinSequence of REAL such that
A1: i in dom abs F and
A2: a = F.i;
(abs F).i = absreal.a by A1,A2,FUNCT_1:12;
hence thesis by EUCLID:def 2;
end;
theorem
for a,b being Real
holds abs <*a,b*> = <*|.a.|,|.b.|*>
proof let a,b be Real;
dom absreal = REAL by FUNCT_2:def 1;
then rng <*a,b*> c= dom absreal;
then
A1: dom abs <*a,b*> = dom <*a,b*> by RELAT_1:27
.= {1,2} by FINSEQ_1:2,89;
A2: dom <*|.a.|,|.b.|*> = {1,2} by FINSEQ_1:2,89;
reconsider a,b as Element of REAL by XREAL_0:def 1;
for i being object st i in dom <*|.a.|,|.b.|*> holds (abs <*a,b*>).i = <*
|.a.|,|.b.|*>.i
proof
let i be object;
A3: <*a,b*>.1 = a;
A4: <*a,b*>.2 = b;
A5: 2 in {1,2} by TARSKI:def 2;
A6: 1 in {1,2} by TARSKI:def 2;
assume
A7: i in dom <*|.a.|,|.b.|*>;
per cases by A2,A7,TARSKI:def 2;
suppose
A8: i = 1;
hence (abs <*a,b*>).i = |.a.| by A1,A3,A6,Th11
.= <*|.a.|,|.b.|*>.i by A8;
end;
suppose
A9: i = 2;
hence (abs <*a,b*>).i = |.b.| by A1,A4,A5,Th11
.= <*|.a.|,|.b.|*>.i by A9;
end;
end;
hence thesis by A1,FINSEQ_1:2,89,FUNCT_1:2;
end;
reserve a, b for Real;
theorem
for a, b, c, d being Real st a <= b & c <= d holds |.b-a.| +
|.d-c.| = (b-a) + (d-c)
proof
let a, b, c, d be Real;
assume that
A1: a <= b and
A2: c <= d;
a - a <= b - a by A1,XREAL_1:13;
then
A3: |.b-a.| = b - a by ABSVALUE:def 1;
c - c <= d - c by A2,XREAL_1:13;
hence thesis by A3,ABSVALUE:def 1;
end;
theorem Th14:
for a, r being Real holds r > 0 implies a in ].a-r,a+r.[
proof
let a, r be Real;
assume r > 0;
then |.a-a.| < r by ABSVALUE:def 1;
hence thesis by RCOMP_1:1;
end;
theorem
for a, r being Real holds r >= 0 implies a in [.a-r,a+r.]
proof
let a, r be Real;
assume
A1: r >= 0;
reconsider a, r as Real;
A2: a+0 <= a+r by A1,XREAL_1:7;
reconsider amr=a-r, apr=a+r as Real;
reconsider X = [.amr,apr.] as Subset of REAL;
A3: X = {b where b is Real : amr <= b & b <= apr} by RCOMP_1:def 1;
a-r <= a-0 by A1,XREAL_1:13;
hence thesis by A3,A2;
end;
theorem Th16:
for a, b being Real holds a < b implies lower_bound ].a,b.[ = a &
upper_bound ].a,b.[ = b
proof
let a, b be Real;
assume
A1: a < b;
set X = ].a,b.[;
reconsider a, b as Real;
A2: (a+b)/2 < b by A1,XREAL_1:226;
A3: a < (a+b)/2 by A1,XREAL_1:226;
then
A4: (a+b)/2 in { l where l is Real : a < l & l < b } by A2;
A5: for s being Real st 0 < s ex r being Real st r in X & r < a+s
proof
let s be Real such that
A6: 0 < s and
A7: for r being Real st r in X holds r >= a+s;
reconsider s as Real;
per cases;
suppose
A8: a + s >= b;
A9: (a+b)/2 in X by A4,RCOMP_1:def 2;
(a+b)/2 < a+s by A2,A8,XXREAL_0:2;
hence thesis by A7,A9;
end;
suppose
A10: a + s < b;
A11: a < a + s by A6,XREAL_1:29;
then (a+(a+s))/2 < a+s by XREAL_1:226;
then
A12: (a+(a+s))/2 < b by A10,XXREAL_0:2;
a < (a+(a+s))/2 by A11,XREAL_1:226;
then (a+(a+s))/2 in {r : a < r & r < b } by A12;
then (a+(a+s))/2 in X by RCOMP_1:def 2;
hence thesis by A7,A11,XREAL_1:226;
end;
end;
A13: for s being Real st 0 < s ex r being Real st r in X & b-s
< r
proof
let s be Real such that
A14: 0 < s and
A15: for r being Real st r in X holds r <= b-s;
reconsider s as Real;
per cases;
suppose
A16: b - s <= a;
A17: (a+b)/2 in X by A4,RCOMP_1:def 2;
(a+b)/2 > b-s by A3,A16,XXREAL_0:2;
hence thesis by A15,A17;
end;
suppose
A18: b - s > a;
A19: b - s < b - 0 by A14,XREAL_1:15;
then b-s < (b+(b-s))/2 by XREAL_1:226;
then
A20: a < (b+(b-s))/2 by A18,XXREAL_0:2;
(b+(b-s))/2 < b by A19,XREAL_1:226;
then (b+(b-s))/2 in {r : a < r & r < b } by A20;
then (b+(b-s))/2 in X by RCOMP_1:def 2;
hence thesis by A15,A19,XREAL_1:226;
end;
end;
a is LowerBound of X
proof
let r be ExtReal;
assume r in X;
then r in { l where l is Real: a < l & l < b } by RCOMP_1:def 2;
then ex r1 being Real st r1 = r & a < r1 & r1 < b;
hence thesis;
end;
then
A21: X is bounded_below;
A22: for r being Real st r in X holds a <= r
proof
let r be Real;
assume r in X;
then r in { l where l is Real: a < l & l < b } by RCOMP_1:def 2;
then ex r1 being Real st r1 = r & a < r1 & r1 < b;
hence thesis;
end;
b is UpperBound of X
proof
let r be ExtReal;
assume r in X;
then r in { l where l is Real: a < l & l < b } by RCOMP_1:def 2;
then ex r1 being Real st r1 = r & a < r1 & r1 < b;
hence thesis;
end;
then
A23: X is bounded_above;
A24: for r being Real st r in X holds b >= r
proof
let r be Real;
assume r in X;
then r in { l where l is Real: a < l & l < b } by RCOMP_1:def 2;
then ex r1 being Real st r1 = r & a < r1 & r1 < b;
hence thesis;
end;
(a+b)/2 in X by A4,RCOMP_1:def 2;
hence thesis by A21,A23,A22,A5,A24,A13,SEQ_4:def 1,def 2;
end;
begin :: Topological preliminaries
registration
let T be TopStruct, A be finite Subset of T;
cluster T|A -> finite;
coherence by PRE_TOPC:8;
end;
registration
let T be TopStruct;
cluster empty -> connected for Subset of T;
coherence
proof
let C be Subset of T;
assume C is empty;
then reconsider D = C as empty Subset of T;
let A, B be Subset of T|C such that
[#](T|C) = A \/ B and
A,B are_separated;
[#](T|D) = {};
hence thesis;
end;
end;
::$CT
theorem Th17:
for S, T being TopSpace st S, T are_homeomorphic & S is
connected holds T is connected
proof
let S, T be TopSpace;
given f being Function of S,T such that
A1: f is being_homeomorphism;
A2: rng f = [#]T by A1;
assume
A3: S is connected;
dom f = [#]S by A1;
then f.:[#]S = [#]T by A2,RELAT_1:113;
hence thesis by A1,A3,CONNSP_1:14;
end;
theorem
for T being TopSpace, F being finite Subset-Family of T st for X being
Subset of T st X in F holds X is compact holds union F is compact
proof
let T be TopSpace, F be finite Subset-Family of T such that
A1: for X being Subset of T st X in F holds X is compact;
defpred P[set] means ex A being Subset of T st A = union $1 & A is compact;
A2: for x, B being set st x in F & B c= F & P[B] holds P[B \/ {x}]
proof
let x, B be set such that
A3: x in F and
A4: B c= F;
B c= bool the carrier of T
proof
let b be object;
assume b in B;
then b in F by A4;
hence thesis;
end;
then reconsider C = B as Subset-Family of T;
reconsider X = x as Subset of T by A3;
given A being Subset of T such that
A5: A = union B and
A6: A is compact;
set K = union C \/ X;
take K;
union {x} = x by ZFMISC_1:25;
hence K = union (B \/ {x}) by ZFMISC_1:78;
X is compact by A1,A3;
hence thesis by A5,A6,COMPTS_1:10;
end;
A7: P[{}]
proof
take {}T;
thus thesis by ZFMISC_1:2;
end;
A8: F is finite;
P[F] from FINSET_1:sch 2(A8,A7,A2);
hence thesis;
end;
begin
theorem Th19:
for A, B, C, D being set, a, b being object st A c= B & C c= D
holds product (a,b) --> (A,C) c= product (a,b) --> (B,D)
proof
let A, B, C, D being set, a, b be object such that
A1: A c= B and
A2: C c= D;
set f = (a,b) --> (A,C), g = (a,b) --> (B,D);
A3: dom f = {a,b} by FUNCT_4:62;
A4: for x being object st x in dom f holds f.x c= g.x
proof
let x be object;
assume x in dom f;
then
A5: x = a or x = b by A3,TARSKI:def 2;
per cases;
suppose
A6: a <> b;
A7: f.b = C by FUNCT_4:63;
f.a = A by A6,FUNCT_4:63;
hence thesis by A1,A2,A5,A6,A7,FUNCT_4:63;
end;
suppose
A8: a = b;
then f = a .--> C by FUNCT_4:81;
then
A9: f.a = C by FUNCOP_1:72;
g = a .--> D by A8,FUNCT_4:81;
hence thesis by A2,A5,A8,A9,FUNCOP_1:72;
end;
end;
dom g = {a,b} by FUNCT_4:62;
hence thesis by A4,CARD_3:27,FUNCT_4:62;
end;
theorem Th20:
for A, B being Subset of REAL holds product ((1,2) --> (A,B)) is
Subset of TOP-REAL 2
proof
let A, B be Subset of REAL;
set f = (1,2) --> (A,B);
product f c= the carrier of TOP-REAL 2
proof
let a be object;
A1: f.1 = A by FUNCT_4:63;
A2: f.2 = B by FUNCT_4:63;
assume a in product f;
then consider g being Function such that
A3: a = g and
A4: dom g = dom f and
A5: for x being object st x in dom f holds g.x in f.x by CARD_3:def 5;
A6: dom f = {1,2} by FUNCT_4:62;
then 2 in dom f by TARSKI:def 2;
then
A7: g.2 in B by A5,A2;
1 in dom f by A6,TARSKI:def 2;
then g.1 in A by A5,A1;
then reconsider m = g.1, n = g.2 as Real by A7;
A8: now
let k be object;
assume k in dom g;
then k = 1 or k = 2 by A4,TARSKI:def 2;
hence g.k = <*g.1,g.2*>.k;
end;
dom <*g.1,g.2*> = {1,2} by FINSEQ_1:2,89;
then a = |[m,n]| by A3,A4,A8,FUNCT_1:2,FUNCT_4:62;
hence thesis;
end;
hence thesis;
end;
theorem
|.|[0,a]|.| = |.a.| & |.|[a,0]|.| = |.a.|
proof
reconsider aa = a as Real;
reconsider a2 = aa^2, z2 = 0^2 as Real;
|.<*0,aa*>.| = sqrt Sum <*z2,a2*> by Th10
.= sqrt (0+a^2) by RVSUM_1:77
.= |.a.| by COMPLEX1:72;
hence |.|[0,a]|.| = |.a.|;
|.<*aa,0 *>.| = sqrt Sum <*a2,z2 *> by Th10
.= sqrt (a^2+0) by RVSUM_1:77
.= |.a.| by COMPLEX1:72;
hence thesis;
end;
theorem Th22:
for p being Point of Euclid 2, q being Point of TOP-REAL 2 st p
= 0.TOP-REAL 2 & p = q holds q = <* 0,0 *> & q`1 = 0 & q`2 = 0
proof
let p be Point of Euclid 2, q be Point of TOP-REAL 2 such that
A1: p = 0.TOP-REAL 2 and
A2: p = q;
0.REAL 2 = 0.TOP-REAL 2 by EUCLID:66;
then p = <*0,0 *> by A1,FINSEQ_2:61;
hence thesis by A2;
end;
theorem
for p, q being Point of Euclid 2, z being Point of TOP-REAL 2 st p =
0.REAL 2 & q = z holds dist(p,q) = |.z.|
proof
let p, q be Point of Euclid 2, z be Point of TOP-REAL 2 such that
A1: p = 0.REAL 2 and
A2: q = z;
reconsider P = p as Point of TOP-REAL 2 by TOPREAL3:8;
A3: 0.REAL 2 = 0.TOP-REAL 2 by EUCLID:66;
then
A4: P`1 = 0 by A1,Th22;
A5: P`2 = 0 by A1,A3,Th22;
dist(p,q) = (Pitag_dist 2).(p,q) by METRIC_1:def 1
.= sqrt ((P`1 - z`1)^2 + (P`2 - z`2)^2) by A2,TOPREAL3:7
.= sqrt ((z`1)^2 + (z`2)^2) by A4,A5;
hence thesis by JGRAPH_1:30;
end;
theorem Th24:
r*p = |[r*p`1,r*p`2]|
proof
p = |[p`1,p`2]| by EUCLID:53;
hence thesis by EUCLID:58;
end;
theorem Th25:
s = (1-r)*p + r*q & s <> p & 0 <= r implies 0 < r
proof
assume that
A1: s = (1-r)*p + r*q and
A2: s <> p and
A3: 0 <= r;
assume
A4: r <= 0;
then s = (1-0)*p + r*q by A1,A3
.= (1-0)*p + 0 * q by A3,A4
.= 1 * p + 0.TOP-REAL 2 by RLVECT_1:10
.= 1 * p by RLVECT_1:4
.= p by RLVECT_1:def 8;
hence thesis by A2;
end;
theorem Th26:
s = (1-r)*p + r*q & s <> q & r <= 1 implies r < 1
proof
assume that
A1: s = (1-r)*p + r*q and
A2: s <> q and
A3: r <= 1;
assume
A4: r >= 1;
then s = (1-1)*p + r*q by A1,A3,XXREAL_0:1
.= 0 * p + 1 * q by A3,A4,XXREAL_0:1
.= 0.TOP-REAL 2 + 1 * q by RLVECT_1:10
.= 1 * q by RLVECT_1:4
.= q by RLVECT_1:def 8;
hence thesis by A2;
end;
theorem
s in LSeg(p,q) & s <> p & s <> q & p`1 < q`1 implies p`1 < s`1 & s`1 < q`1
proof
assume that
A1: s in LSeg(p,q) and
A2: s <> p and
A3: s <> q and
A4: p`1 < q`1;
A5: p`1-q`1 < 0 by A4,XREAL_1:49;
consider r such that
A6: s = (1-r)*p + r*q and
A7: 0 <= r and
A8: r <= 1 by A1;
(1-r)*p = |[(1-r)*p`1,(1-r)*p`2]| by Th24;
then
A9: ((1-r)*p)`1 = (1-r)*p`1;
r*q = |[r*q`1,r*q`2]| by Th24;
then
A10: (r*q)`1 = r*q`1;
s = |[((1-r)*p)`1 + (r*q)`1,((1-r)*p)`2 + (r*q)`2]| by A6,EUCLID:55;
then
A11: s`1 = (1-r)*p`1 + r*q`1 by A9,A10;
then
A12: p`1 - s`1 = r*(p`1-q`1);
r < 1 by A3,A6,A8,Th26;
then
A13: 1-r > 0 by XREAL_1:50;
A14: q`1-p`1 > 0 by A4,XREAL_1:50;
r > 0 by A2,A6,A7,Th25;
then
A15: p`1 - s`1 < 0 by A12,A5,XREAL_1:132;
q`1 - s`1 = (1-r)*(q`1-p`1) by A11;
then q`1 - s`1 > 0 by A14,A13,XREAL_1:129;
hence thesis by A15,XREAL_1:47,48;
end;
theorem
s in LSeg(p,q) & s <> p & s <> q & p`2 < q`2 implies p`2 < s`2 & s`2 < q`2
proof
assume that
A1: s in LSeg(p,q) and
A2: s <> p and
A3: s <> q and
A4: p`2 < q`2;
A5: p`2-q`2 < 0 by A4,XREAL_1:49;
consider r such that
A6: s = (1-r)*p + r*q and
A7: 0 <= r and
A8: r <= 1 by A1;
(1-r)*p = |[(1-r)*p`1,(1-r)*p`2]| by Th24;
then
A9: ((1-r)*p)`2 = (1-r)*p`2;
r*q = |[r*q`1,r*q`2]| by Th24;
then
A10: (r*q)`2 = r*q`2;
s = |[((1-r)*p)`1 + (r*q)`1,((1-r)*p)`2 + (r*q)`2]| by A6,EUCLID:55;
then
A11: s`2 = (1-r)*p`2 + r*q`2 by A9,A10;
then
A12: p`2 - s`2 = r*(p`2-q`2);
r < 1 by A3,A6,A8,Th26;
then
A13: 1-r > 0 by XREAL_1:50;
A14: q`2-p`2 > 0 by A4,XREAL_1:50;
r > 0 by A2,A6,A7,Th25;
then
A15: p`2 - s`2 < 0 by A12,A5,XREAL_1:132;
q`2 - s`2 = (1-r)*(q`2-p`2) by A11;
then q`2 - s`2 > 0 by A14,A13,XREAL_1:129;
hence thesis by A15,XREAL_1:47,48;
end;
theorem
for p being Point of TOP-REAL 2 ex q being Point of TOP-REAL 2 st q`1
< W-bound D & p <> q
proof
let p be Point of TOP-REAL 2;
take q = |[W-bound D - 1, p`2 - 1]|;
W-bound D - 1 < W-bound D - 0 by XREAL_1:15;
hence q`1 < W-bound D;
thus thesis;
end;
theorem
for p being Point of TOP-REAL 2 ex q being Point of TOP-REAL 2 st q`1
> E-bound D & p <> q
proof
let p be Point of TOP-REAL 2;
take q = |[E-bound D + 1, p`2 - 1]|;
E-bound D + 1 > E-bound D + 0 by XREAL_1:6;
hence q`1 > E-bound D;
thus thesis;
end;
theorem
for p being Point of TOP-REAL 2 ex q being Point of TOP-REAL 2 st q`2
> N-bound D & p <> q
proof
let p be Point of TOP-REAL 2;
take q = |[p`1 - 1,N-bound D + 1]|;
N-bound D + 1 > N-bound D + 0 by XREAL_1:6;
hence q`2 > N-bound D;
thus thesis;
end;
theorem
for p being Point of TOP-REAL 2 ex q being Point of TOP-REAL 2 st q`2
< S-bound D & p <> q
proof
let p be Point of TOP-REAL 2;
take q = |[p`1 - 1,S-bound D - 1]|;
S-bound D - 1 < S-bound D - 0 by XREAL_1:15;
hence q`2 < S-bound D;
thus thesis;
end;
registration
cluster non horizontal -> non empty for Subset of TOP-REAL 2;
coherence;
cluster non vertical -> non empty for Subset of TOP-REAL 2;
coherence;
cluster being_Region -> open connected for Subset of TOP-REAL 2;
coherence by TOPREAL4:def 3;
cluster open connected -> being_Region for Subset of TOP-REAL 2;
coherence by TOPREAL4:def 3;
end;
registration
cluster empty -> horizontal for Subset of TOP-REAL 2;
coherence;
cluster empty -> vertical for Subset of TOP-REAL 2;
coherence;
end;
registration
cluster non empty convex for Subset of TOP-REAL 2;
existence
proof
set C = the non empty convex Subset of TOP-REAL 2;
take C;
thus thesis;
end;
end;
registration
let a, b be Point of TOP-REAL 2;
cluster LSeg(a,b) -> connected;
coherence;
end;
registration
cluster R^2-unit_square -> connected;
coherence
proof
A1: LSeg(|[0,1]|,|[1,1]|) meets LSeg(|[1,0]|,|[1,1]|) by TOPREAL1:18;
A2: LSeg(|[0,0]|,|[1,0]|) meets LSeg(|[1,0]|,|[1,1]|) by TOPREAL1:16;
A3: LSeg(|[0,0]|,|[0,1]|) meets LSeg(|[0,1]|,|[1,1]|) by TOPREAL1:15;
R^2-unit_square = LSeg(|[ 0,0 ]|, |[ 0,1 ]|) \/ LSeg(|[ 0,1 ]|, |[ 1,1
]|) \/ LSeg(|[ 1,1 ]|, |[ 1,0 ]|) \/ LSeg(|[ 1,0 ]|, |[ 0,0 ]|) by
TOPREAL1:def 2,XBOOLE_1:4;
hence thesis by A3,A2,A1,JORDAN1:5;
end;
end;
registration
cluster being_simple_closed_curve -> connected for Subset of TOP-REAL 2;
coherence
proof
let P be Subset of TOP-REAL 2;
given f being Function of (TOP-REAL 2) | R^2-unit_square, (TOP-REAL 2) |P
such that
A1: f is being_homeomorphism;
A2: (TOP-REAL 2) |R^2-unit_square, (TOP-REAL 2) |P are_homeomorphic
by A1;
(TOP-REAL 2) |R^2-unit_square is connected by CONNSP_1:def 3;
then (TOP-REAL 2) |P is connected by A2,Th17;
hence thesis;
end;
end;
theorem :: SPRECT_3:26
LSeg(NE-corner P,SE-corner P) c= L~SpStSeq P
proof
A1: LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P) c= (LSeg(
NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P)) \/ (LSeg(SE-corner P
,SW-corner P) \/ LSeg(SW-corner P,NW-corner P)) by XBOOLE_1:7;
LSeg(NE-corner P,SE-corner P) c= (LSeg(NW-corner P,NE-corner P) \/ LSeg(
NE-corner P,SE-corner P)) by XBOOLE_1:7;
then
LSeg(NE-corner P,SE-corner P) c= (LSeg(NW-corner P,NE-corner P) \/ LSeg(
NE-corner P,SE-corner P)) \/ (LSeg(SE-corner P,SW-corner P) \/ LSeg(SW-corner P
,NW-corner P)) by A1;
hence thesis by SPRECT_1:41;
end;
theorem
LSeg(SW-corner P,SE-corner P) c= L~SpStSeq P
proof
LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P) \/ LSeg(
SE-corner P,SW-corner P) c= LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,
SE-corner P) \/ LSeg(SE-corner P,SW-corner P) \/ LSeg(SW-corner P,NW-corner P)
by XBOOLE_1:7;
then
A1: LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P) \/ LSeg(
SE-corner P,SW-corner P) c= LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,
SE-corner P) \/ (LSeg(SE-corner P,SW-corner P) \/ LSeg(SW-corner P,NW-corner P)
) by XBOOLE_1:4;
LSeg(SW-corner P,SE-corner P) c= (LSeg(NW-corner P,NE-corner P) \/ LSeg(
NE-corner P,SE-corner P)) \/ LSeg(SW-corner P,SE-corner P) by XBOOLE_1:7;
then
LSeg(SW-corner P,SE-corner P) c= (LSeg(NW-corner P,NE-corner P) \/ LSeg(
NE-corner P,SE-corner P)) \/ (LSeg(SE-corner P,SW-corner P) \/ LSeg(SW-corner P
,NW-corner P)) by A1;
hence thesis by SPRECT_1:41;
end;
theorem
LSeg(SW-corner P,NW-corner P) c= L~SpStSeq P
proof
LSeg(SW-corner P,NW-corner P) c= LSeg(NW-corner P,NE-corner P) \/ LSeg(
NE-corner P,SE-corner P) \/ LSeg(SE-corner P,SW-corner P) \/ LSeg(SW-corner P,
NW-corner P) by XBOOLE_1:7;
then
LSeg(SW-corner P,NW-corner P) c= LSeg(NW-corner P,NE-corner P) \/ LSeg(
NE-corner P,SE-corner P) \/ (LSeg(SE-corner P,SW-corner P) \/ LSeg(SW-corner P,
NW-corner P)) by XBOOLE_1:4;
hence thesis by SPRECT_1:41;
end;
theorem
for C being Subset of TOP-REAL 2 holds {p where p is Point of TOP-REAL
2: p`1 < W-bound C} is non empty convex connected Subset of TOP-REAL 2
proof
let C be Subset of TOP-REAL 2;
set A = {p where p is Point of TOP-REAL 2: p`1 < W-bound C};
A c= the carrier of TOP-REAL 2
proof
let a be object;
assume a in A;
then ex p being Point of TOP-REAL 2 st a = p & p`1 < W-bound C;
hence thesis;
end;
then reconsider A as Subset of TOP-REAL 2;
set p = W-bound C;
set b = |[p-1,0]|;
A1: b`1 = p-1;
p - 1 < p - 0 by XREAL_1:15;
then
A2: b in A by A1;
A is convex
proof
let w1, w2 be Point of TOP-REAL 2;
assume w1 in A;
then consider p being Point of TOP-REAL 2 such that
A3: w1 = p and
A4: p`1 < W-bound C;
assume w2 in A;
then consider q being Point of TOP-REAL 2 such that
A5: w2 = q and
A6: q`1 < W-bound C;
let k be object;
assume
A7: k in LSeg(w1,w2);
then reconsider z = k as Point of TOP-REAL 2;
per cases by XXREAL_0:1;
suppose
p`1 < q`1;
then z`1 <= w2`1 by A3,A5,A7,TOPREAL1:3;
then z`1 < W-bound C by A5,A6,XXREAL_0:2;
hence thesis;
end;
suppose
q`1 < p`1;
then z`1 <= w1`1 by A3,A5,A7,TOPREAL1:3;
then z`1 < W-bound C by A3,A4,XXREAL_0:2;
hence thesis;
end;
suppose
p`1 = q`1;
then z`1 = p`1 by A3,A5,A7,GOBOARD7:5;
hence thesis by A4;
end;
end;
then reconsider A as non empty convex Subset of TOP-REAL 2 by A2;
A is connected;
hence thesis;
end;
begin :: Balls as subsets of TOP-REAL n
reserve r for Real;
theorem Th37:
e = q & p in Ball(e,r) implies q`1-r < p`1 & p`1 < q`1+r
proof
assume that
A1: e = q and
A2: p in Ball(e,r);
reconsider f = p as Point of Euclid 2 by TOPREAL3:8;
A3: dist(e,f) < r by A2,METRIC_1:11;
A4: dist(e,f) = (Pitag_dist 2).(e,f) by METRIC_1:def 1
.= sqrt ((q`1 - p`1)^2 + (q`2 - p`2)^2) by A1,TOPREAL3:7;
A5: r > 0 by A2,TBSP_1:12;
assume
A6: not thesis;
per cases by A6;
suppose
A7: q`1-r >= p`1;
(q`2-p`2)^2 >= 0 by XREAL_1:63;
then
A8: (q`1-p`1)^2 + (q`2-p`2)^2 >= (q`1-p`1)^2 + 0 by XREAL_1:6;
q`1-p`1 >= r by A7,XREAL_1:11;
then (q`1-p`1)^2 >= r^2 by A5,SQUARE_1:15;
then (q`1-p`1)^2 + (q`2-p`2)^2 >= r^2 by A8,XXREAL_0:2;
then sqrt((q`1-p`1)^2 + (q`2-p`2)^2) >= sqrt(r^2) by A5,SQUARE_1:26;
hence contradiction by A3,A4,A5,SQUARE_1:22;
end;
suppose
A9: p`1 >= q`1+r;
(q`2-p`2)^2 >= 0 by XREAL_1:63;
then
A10: (q`1-p`1)^2 + (q`2-p`2)^2 >= (q`1-p`1)^2 + 0 by XREAL_1:6;
p`1-q`1 >= r by A9,XREAL_1:19;
then (-(q`1-p`1))^2 >= r^2 by A5,SQUARE_1:15;
then (q`1-p`1)^2 + (q`2-p`2)^2 >= r^2 by A10,XXREAL_0:2;
then sqrt((q`1-p`1)^2 + (q`2-p`2)^2) >= sqrt(r^2) by A5,SQUARE_1:26;
hence contradiction by A3,A4,A5,SQUARE_1:22;
end;
end;
theorem Th38:
e = q & p in Ball(e,r) implies q`2-r < p`2 & p`2 < q`2+r
proof
assume that
A1: e = q and
A2: p in Ball(e,r);
reconsider f = p as Point of Euclid 2 by TOPREAL3:8;
A3: dist(e,f) < r by A2,METRIC_1:11;
A4: dist(e,f) = (Pitag_dist 2).(e,f) by METRIC_1:def 1
.= sqrt ((q`1 - p`1)^2 + (q`2 - p`2)^2) by A1,TOPREAL3:7;
A5: r > 0 by A2,TBSP_1:12;
assume
A6: not thesis;
per cases by A6;
suppose
A7: q`2-r >= p`2;
(q`1-p`1)^2 >= 0 by XREAL_1:63;
then
A8: (q`1-p`1)^2 + (q`2-p`2)^2 >= (q`2-p`2)^2 + 0 by XREAL_1:6;
q`2-p`2 >= r by A7,XREAL_1:11;
then (q`2-p`2)^2 >= r^2 by A5,SQUARE_1:15;
then (q`1-p`1)^2 + (q`2-p`2)^2 >= r^2 by A8,XXREAL_0:2;
then sqrt((q`1-p`1)^2 + (q`2-p`2)^2) >= sqrt(r^2) by A5,SQUARE_1:26;
hence contradiction by A3,A4,A5,SQUARE_1:22;
end;
suppose
A9: p`2 >= q`2+r;
(q`1-p`1)^2 >= 0 by XREAL_1:63;
then
A10: (q`1-p`1)^2 + (q`2-p`2)^2 >= (q`2-p`2)^2 + 0 by XREAL_1:6;
p`2-q`2 >= r by A9,XREAL_1:19;
then (-(q`2-p`2))^2 >= r^2 by A5,SQUARE_1:15;
then (q`1-p`1)^2 + (q`2-p`2)^2 >= r^2 by A10,XXREAL_0:2;
then sqrt((q`1-p`1)^2 + (q`2-p`2)^2) >= sqrt(r^2) by A5,SQUARE_1:26;
hence contradiction by A3,A4,A5,SQUARE_1:22;
end;
end;
theorem Th39:
p = e implies product ((1,2) --> (].p`1-r/sqrt 2,p`1+r/sqrt 2.[,
].p`2-r/sqrt 2,p`2+r/sqrt 2.[)) c= Ball(e,r)
proof
set A = ].p`1-r/sqrt 2,p`1+r/sqrt 2.[, B = ].p`2-r/sqrt 2,p`2+r/sqrt 2.[, f
= (1,2) --> (A,B);
assume
A1: p = e;
let a be object;
A2: A = {m where m is Real : p`1-r/sqrt 2 < m & m < p`1+r/sqrt 2 } by
RCOMP_1:def 2;
A3: f.2 = B by FUNCT_4:63;
A4: B = {n where n is Real : p`2-r/sqrt 2 < n & n < p`2+r/sqrt 2 } by
RCOMP_1:def 2;
A5: f.1 = A by FUNCT_4:63;
assume a in product f;
then consider g being Function such that
A6: a = g and
A7: dom g = dom f and
A8: for x being object st x in dom f holds g.x in f.x by CARD_3:def 5;
A9: dom f = {1,2} by FUNCT_4:62;
then 1 in dom f by TARSKI:def 2;
then
A10: g.1 in A by A8,A5;
then consider m being Real such that
A11: m = g.1 and
p`1-r/sqrt 2 < m and
m < p`1+r/sqrt 2 by A2;
A12: 0 <= (m-p`1)^2 by XREAL_1:63;
2 in dom f by A9,TARSKI:def 2;
then
A13: g.2 in B by A8,A3;
then consider n being Real such that
A14: n = g.2 and
p`2-r/sqrt 2 < n and
n < p`2+r/sqrt 2 by A4;
|.n-p`2.| < r/sqrt 2 by A13,A14,RCOMP_1:1;
then (|.n-p`2.|)^2 < (r/sqrt 2)^2 by COMPLEX1:46,SQUARE_1:16;
then (|.n-p`2.|)^2 < r^2/(sqrt 2)^2 by XCMPLX_1:76;
then (|.n-p`2.|)^2 < r^2/2 by SQUARE_1:def 2;
then
A15: (n-p`2)^2 < r^2/2 by COMPLEX1:75;
p`1-(p`1+r/sqrt 2) < p`1-(p`1-r/sqrt 2) by A10,XREAL_1:15,XXREAL_1:28;
then -r/sqrt 2+r/sqrt 2 < r/sqrt 2+r/sqrt 2 by XREAL_1:6;
then
A16: 0 < r by SQUARE_1:19;
A17: now
let k be object;
assume k in dom g;
then k = 1 or k = 2 by A7,TARSKI:def 2;
hence g.k = <*g.1,g.2*>.k;
end;
A18: 0 <= (n-p`2)^2 by XREAL_1:63;
|.m-p`1.| < r/sqrt 2 by A10,A11,RCOMP_1:1;
then (|.m-p`1.|)^2 < (r/sqrt 2)^2 by COMPLEX1:46,SQUARE_1:16;
then (|.m-p`1.|)^2 < r^2/(sqrt 2)^2 by XCMPLX_1:76;
then (|.m-p`1.|)^2 < r^2/2 by SQUARE_1:def 2;
then (m-p`1)^2 < r^2/2 by COMPLEX1:75;
then (m-p`1)^2 + (n-p`2)^2 < r^2/2 + r^2/2 by A15,XREAL_1:8;
then sqrt((m-p`1)^2 + (n-p`2)^2) < sqrt(r^2) by A12,A18,SQUARE_1:27;
then
A19: sqrt((m-p`1)^2 + (n-p`2)^2) < r by A16,SQUARE_1:22;
dom <*g.1,g.2*> = {1,2} by FINSEQ_1:2,89;
then a = |[m,n]| by A6,A7,A11,A14,A17,FUNCT_1:2,FUNCT_4:62;
then reconsider c = a as Point of TOP-REAL 2;
reconsider b = c as Point of Euclid 2 by TOPREAL3:8;
dist(b,e) = (Pitag_dist 2).(b,e) by METRIC_1:def 1
.= sqrt ((c`1 - p`1)^2 + (c`2 - p`2)^2) by A1,TOPREAL3:7;
hence thesis by A6,A11,A14,A19,METRIC_1:11;
end;
theorem Th40:
p = e implies Ball(e,r) c= product((1,2)-->(].p`1-r,p`1+r.[,].p
`2-r,p`2+r.[))
proof
set A = ].p`1-r,p`1+r.[, B = ].p`2-r,p`2+r.[, f = (1,2)-->(A,B);
assume that
A1: p = e;
let a be object;
assume
A2: a in Ball(e,r);
then reconsider b = a as Point of Euclid 2;
reconsider q = b as Point of TOP-REAL 2 by TOPREAL3:8;
reconsider g = q as FinSequence;
A3: for x being object st x in dom f holds g.x in f.x
proof
let x be object;
assume
A4: x in dom f;
per cases by A4,TARSKI:def 2;
suppose
A5: x = 1;
A6: f.1 = A by FUNCT_4:63;
A7: q`1 < p`1+r by A1,A2,Th37;
p`1-r < q`1 by A1,A2,Th37;
hence thesis by A5,A6,A7,XXREAL_1:4;
end;
suppose
A8: x = 2;
A9: f.2 = B by FUNCT_4:63;
A10: q`2 < p`2+r by A1,A2,Th38;
p`2-r < q`2 by A1,A2,Th38;
hence thesis by A8,A9,A10,XXREAL_1:4;
end;
end;
q is Function of Seg 2, REAL by EUCLID:23;
then
A11: dom g = {1,2} by FINSEQ_1:2,FUNCT_2:def 1;
dom f = {1,2} by FUNCT_4:62;
hence thesis by A11,A3,CARD_3:9;
end;
theorem Th41:
P = Ball(e,r) & p = e implies proj1.:P = ].p`1-r,p`1+r.[
proof
assume that
A1: P = Ball(e,r) and
A2: p = e;
hereby
let a be object;
assume a in proj1.:P;
then consider x being object such that
A3: x in the carrier of TOP-REAL 2 and
A4: x in P and
A5: a = proj1.x by FUNCT_2:64;
reconsider b = a as Real by A5;
reconsider x as Point of TOP-REAL 2 by A3;
A6: a = x`1 by A5,PSCOMP_1:def 5;
then
A7: b < p`1+r by A1,A2,A4,Th37;
p`1-r < b by A1,A2,A4,A6,Th37;
hence a in ].p`1-r,p`1+r.[ by A7,XXREAL_1:4;
end;
let a be object;
assume
A8: a in ].p`1-r,p`1+r.[;
then reconsider b = a as Real;
reconsider f = |[b,p`2]| as Point of Euclid 2 by TOPREAL3:8;
A9: dist(f,e) = (Pitag_dist 2).(f,e) by METRIC_1:def 1
.= sqrt ((|[b,p`2]|`1 - p`1)^2 + (|[b,p`2]|`2 - p`2)^2 ) by A2,TOPREAL3:7
.= sqrt ((b - p`1)^2 + (|[b,p`2]|`2 - p`2)^2)
.= sqrt ((b - p`1)^2 + (p`2 - p`2)^2)
.= sqrt ((b - p`1)^2 + 0);
b < p`1+r by A8,XXREAL_1:4;
then
A10: b - p`1 < p`1+r - p`1 by XREAL_1:9;
now
per cases;
case
0 <= b - p`1;
hence dist(f,e) < r by A10,A9,SQUARE_1:22;
end;
case
A11: 0 > b - p`1;
p`1 - r < b by A8,XXREAL_1:4;
then p`1 - r + r < b + r by XREAL_1:6;
then
A12: p`1 - b < r + b - b by XREAL_1:9;
sqrt ((b - p`1)^2) = sqrt ((-(b - p`1))^2)
.= -(b - p`1) by A11,SQUARE_1:22;
hence dist(f,e) < r by A9,A12;
end;
end;
then
A13: |[b,p`2]| in P by A1,METRIC_1:11;
a = |[b,p`2]|`1
.= proj1.(|[b,p`2]|) by PSCOMP_1:def 5;
hence thesis by A13,FUNCT_2:35;
end;
theorem Th42:
P = Ball(e,r) & p = e implies proj2.:P = ].p`2-r,p`2+r.[
proof
assume that
A1: P = Ball(e,r) and
A2: p = e;
hereby
let a be object;
assume a in proj2.:P;
then consider x being object such that
A3: x in the carrier of TOP-REAL 2 and
A4: x in P and
A5: a = proj2.x by FUNCT_2:64;
reconsider b = a as Real by A5;
reconsider x as Point of TOP-REAL 2 by A3;
A6: a = x`2 by A5,PSCOMP_1:def 6;
then
A7: b < p`2+r by A1,A2,A4,Th38;
p`2-r < b by A1,A2,A4,A6,Th38;
hence a in ].p`2-r,p`2+r.[ by A7,XXREAL_1:4;
end;
let a be object;
assume
A8: a in ].p`2-r,p`2+r.[;
then reconsider b = a as Real;
reconsider f = |[p`1,b]| as Point of Euclid 2 by TOPREAL3:8;
A9: dist(f,e) = (Pitag_dist 2).(f,e) by METRIC_1:def 1
.= sqrt ((|[p`1,b]|`1 - p`1)^2 + (|[p`1,b]|`2 - p`2)^2 ) by A2,TOPREAL3:7
.= sqrt ((p`1 - p`1)^2 + (|[p`1,b]|`2 - p`2)^2)
.= sqrt (0 + (b - p`2)^2);
b < p`2+r by A8,XXREAL_1:4;
then
A10: b - p`2 < p`2+r - p`2 by XREAL_1:9;
now
per cases;
case
0 <= b - p`2;
hence dist(f,e) < r by A10,A9,SQUARE_1:22;
end;
case
A11: 0 > b - p`2;
p`2 - r < b by A8,XXREAL_1:4;
then p`2 - r + r < b + r by XREAL_1:6;
then
A12: p`2 - b < r + b - b by XREAL_1:9;
sqrt ((b - p`2)^2) = sqrt ((-(b - p`2))^2)
.= -(b - p`2) by A11,SQUARE_1:22;
hence dist(f,e) < r by A9,A12;
end;
end;
then
A13: |[p`1,b]| in P by A1,METRIC_1:11;
a = |[p`1,b]|`2
.= proj2.(|[p`1,b]|) by PSCOMP_1:def 6;
hence thesis by A13,FUNCT_2:35;
end;
theorem
D = Ball(e,r) & p = e implies W-bound D = p`1 - r
proof
assume that
A1: D = Ball(e,r) and
A2: p = e;
r > 0 by A1,TBSP_1:12;
then
A3: p`1+0 < p`1+r by XREAL_1:6;
p`1-r < p`1-0 by A1,TBSP_1:12,XREAL_1:15;
then p`1-r < p`1+r by A3,XXREAL_0:2;
then
A4: lower_bound ].p`1-r,p`1+r.[ = p`1-r by Th16;
proj1.:D = ].p`1-r,p`1+r.[ by A1,A2,Th41;
hence thesis by A4,SPRECT_1:43;
end;
theorem
D = Ball(e,r) & p = e implies E-bound D = p`1 + r
proof
assume that
A1: D = Ball(e,r) and
A2: p = e;
r > 0 by A1,TBSP_1:12;
then
A3: p`1+0 < p`1+r by XREAL_1:6;
p`1-r < p`1-0 by A1,TBSP_1:12,XREAL_1:15;
then p`1-r < p`1+r by A3,XXREAL_0:2;
then
A4: upper_bound ].p`1-r,p`1+r.[ = p`1+r by Th16;
proj1.:D = ].p`1-r,p`1+r.[ by A1,A2,Th41;
hence thesis by A4,SPRECT_1:46;
end;
theorem
D = Ball(e,r) & p = e implies S-bound D = p`2 - r
proof
assume that
A1: D = Ball(e,r) and
A2: p = e;
r > 0 by A1,TBSP_1:12;
then
A3: p`2+0 < p`2+r by XREAL_1:6;
p`2-r < p`2-0 by A1,TBSP_1:12,XREAL_1:15;
then p`2-r < p`2+r by A3,XXREAL_0:2;
then
A4: lower_bound ].p`2-r,p`2+r.[ = p`2-r by Th16;
proj2.:D = ].p`2-r,p`2+r.[ by A1,A2,Th42;
hence thesis by A4,SPRECT_1:44;
end;
theorem
D = Ball(e,r) & p = e implies N-bound D = p`2 + r
proof
assume that
A1: D = Ball(e,r) and
A2: p = e;
r > 0 by A1,TBSP_1:12;
then
A3: p`2+0 < p`2+r by XREAL_1:6;
p`2-r < p`2-0 by A1,TBSP_1:12,XREAL_1:15;
then p`2-r < p`2+r by A3,XXREAL_0:2;
then
A4: upper_bound ].p`2-r,p`2+r.[ = p`2+r by Th16;
proj2.:D = ].p`2-r,p`2+r.[ by A1,A2,Th42;
hence thesis by A4,SPRECT_1:45;
end;
theorem
D = Ball(e,r) implies D is non horizontal
proof
reconsider p = e as Point of TOP-REAL 2 by TOPREAL3:8;
assume
A1: D = Ball(e,r);
then
A2: r > 0 by TBSP_1:12;
take p, q = |[p`1,p`2-r/2]|;
thus p in D by A1,TBSP_1:11,12;
reconsider f = q as Point of Euclid 2 by TOPREAL3:8;
dist(e,f) = (Pitag_dist 2).(e,f) by METRIC_1:def 1
.= sqrt ((p`1 - q`1)^2 + (p`2 - q`2)^2) by TOPREAL3:7
.= sqrt ((p`1 - p`1)^2 + (p`2 - q`2)^2)
.= sqrt (0 + (p`2 - (p`2-r/2))^2)
.= r/2 by A2,SQUARE_1:22;
then dist(e,f) < r by A1,TBSP_1:12,XREAL_1:216;
hence q in D by A1,METRIC_1:11;
r/2 > 0 by A2,XREAL_1:139;
then p`2-r/2 < p`2-0 by XREAL_1:15;
hence thesis;
end;
theorem
D = Ball(e,r) implies D is non vertical
proof
reconsider p = e as Point of TOP-REAL 2 by TOPREAL3:8;
assume
A1: D = Ball(e,r);
then
A2: r > 0 by TBSP_1:12;
take p, q = |[p`1-r/2,p`2]|;
thus p in D by A1,TBSP_1:11,12;
reconsider f = q as Point of Euclid 2 by TOPREAL3:8;
dist(e,f) = (Pitag_dist 2).(e,f) by METRIC_1:def 1
.= sqrt ((p`1 - q`1)^2 + (p`2 - q`2)^2) by TOPREAL3:7
.= sqrt ((p`1 - (p`1-r/2))^2 + (p`2 - q`2)^2)
.= sqrt ((p`1 - (p`1-r/2))^2 + (p`2 - p`2)^2)
.= r/2 by A2,SQUARE_1:22;
then dist(e,f) < r by A1,TBSP_1:12,XREAL_1:216;
hence q in D by A1,METRIC_1:11;
r/2 > 0 by A2,XREAL_1:139;
then p`1-r/2 < p`1-0 by XREAL_1:15;
hence thesis;
end;
theorem
for f being Point of Euclid 2, x being Point of TOP-REAL 2 st x in
Ball(f,a) holds not |[x`1-2*a,x`2]| in Ball(f,a)
proof
let f be Point of Euclid 2, x be Point of TOP-REAL 2 such that
A1: x in Ball(f,a);
A2: a > 0 by A1,TBSP_1:12;
set p = |[x`1-2*a,x`2]|;
reconsider z = p, X = x as Point of Euclid 2 by TOPREAL3:8;
A3: dist(X,z) = (Pitag_dist 2).(X,z) by METRIC_1:def 1
.= sqrt ((x`1 - p`1)^2 + (x`2 - p`2)^2) by TOPREAL3:7
.= sqrt ((x`1 - (x`1-2*a))^2 + (x`2 - p`2)^2)
.= sqrt (0^2 + 2*(x`1 - x`1)*(2*a) + (2*a)^2 + (x`2 - x`2)^2)
.= 2*a by A2,SQUARE_1:22;
assume |[x`1-2*a,x`2]| in Ball(f,a);
then
A4: dist(f,z) < a by METRIC_1:11;
dist(f,X) < a by A1,METRIC_1:11;
then dist(f,X) + dist(f,z) < a + a by A4,XREAL_1:8;
hence contradiction by A3,METRIC_1:4;
end;
theorem
for X being non empty compact Subset of TOP-REAL 2, p being Point of
Euclid 2 st p = 0.TOP-REAL 2 & a > 0 holds X
c= Ball(p, |.E-bound X.|+|.N-bound X.|+|.W-bound X.|+|.S-bound X.|+a)
proof
let X be non empty compact Subset of TOP-REAL 2, p be Point of Euclid 2 such
that
A1: p = 0.TOP-REAL 2 and
A2: a > 0;
set A = X, n = N-bound A, s = S-bound A, e = E-bound A, w = W-bound A, r =
|.e.|+|.n.|+|.w.|+|.s.|+a;
A3: |.e.| + |.n.| + |.w.| + |.s.| + 0 < |.e.| + |.n.| + |.w.| + |.s.| + a
by A2,XREAL_1:8;
let x be object;
assume
A4: x in X;
then reconsider b = x as Point of Euclid 2 by TOPREAL3:8;
reconsider P = p, B = b as Point of TOP-REAL 2 by TOPREAL3:8;
A5: P`1 = 0 by A1,Th22;
A6: B`1 <= e by A4,PSCOMP_1:24;
A7: B`2 <= n by A4,PSCOMP_1:24;
A8: s <= B`2 by A4,PSCOMP_1:24;
A9: P`2 = 0 by A1,Th22;
A10: dist(p,b) = (Pitag_dist 2).(p,b) by METRIC_1:def 1
.= sqrt ((P`1 - B`1)^2 + (P`2 - B`2)^2) by TOPREAL3:7
.= sqrt ((B`1)^2 + (B`2)^2) by A5,A9;
A11: 0 <= (B`2)^2 by XREAL_1:63;
0 <= (B`1)^2 by XREAL_1:63;
then sqrt ((B`1)^2 + (B`2)^2) <= sqrt(B`1)^2 + sqrt(B`2)^2
by A11,SQUARE_1:59;
then sqrt ((B`1)^2 + (B`2)^2) <= |.B`1.| + sqrt(B`2)^2 by COMPLEX1:72;
then
A12: sqrt ((B`1)^2 + (B`2)^2) <= |.B`1.| + |.B`2.| by COMPLEX1:72;
A13: 0 <= |.n.| by COMPLEX1:46;
A14: 0 <= |.e.| by COMPLEX1:46;
A15: 0 <= |.w.| by COMPLEX1:46;
A16: 0 <= |.s.| by COMPLEX1:46;
A17: w <= B`1 by A4,PSCOMP_1:24;
now
per cases;
case
A18: B`1 >= 0 & B`2 >= 0;
|.e.| + |.n.| + 0 <= |.e.| + |.n.| + |.w.| by A15,XREAL_1:7;
then |.e.| + |.n.| <= |.e.| + |.n.| + |.w.| + |.s.| by A16,XREAL_1:7;
then
A19: |.e.| + |.n.| < r by A3,XXREAL_0:2;
A20: |.B`2.| <= |.n.| by A7,A18,Th1;
|.B`1.| <= |.e.| by A6,A18,Th1;
then |.B`1.| + |.B`2.| <= |.e.| + |.n.| by A20,XREAL_1:7;
then dist(p,b) <= |.e.| + |.n.| by A10,A12,XXREAL_0:2;
hence dist(p,b) < r by A19,XXREAL_0:2;
end;
case
A21: B`1 < 0 & B`2 >= 0;
0 + (|.n.| + |.w.|) <= |.e.| + (|.n.| + |.w.|) by A14,XREAL_1:7;
then |.w.| + |.n.| <= |.e.| + |.n.| + |.w.| + |.s.| by A16,XREAL_1:7;
then
A22: |.w.| + |.n.| < r by A3,XXREAL_0:2;
A23: |.B`2.| <= |.n.| by A7,A21,Th1;
|.B`1.| <= |.w.| by A17,A21,Th2;
then |.B`1.| + |.B`2.| <= |.w.| + |.n.| by A23,XREAL_1:7;
then dist(p,b) <= |.w.| + |.n.| by A10,A12,XXREAL_0:2;
hence dist(p,b) < r by A22,XXREAL_0:2;
end;
case
A24: B`1 >= 0 & B`2 < 0;
A25: |.e.| + |.n.| + |.s.| + 0 <= |.e.| + |.n.| + |.s.| + |.w.|
by A15,XREAL_1:7;
|.e.| + |.s.| + 0 <= |.e.| + |.s.| + |.n.| by A13,XREAL_1:7;
then |.e.| + |.s.| <= |.e.| + |.n.| + |.w.| + |.s.| by A25,XXREAL_0:2;
then
A26: |.e.| + |.s.| < r by A3,XXREAL_0:2;
A27: |.B`2.| <= |.s.| by A8,A24,Th2;
|.B`1.| <= |.e.| by A6,A24,Th1;
then |.B`1.| + |.B`2.| <= |.e.| + |.s.| by A27,XREAL_1:7;
then dist(p,b) <= |.e.| + |.s.| by A10,A12,XXREAL_0:2;
hence dist(p,b) < r by A26,XXREAL_0:2;
end;
case
A28: B`1 < 0 & B`2 < 0;
then
A29: |.B`2.| <= |.s.| by A8,Th2;
|.B`1.| <= |.w.| by A17,A28,Th2;
then |.B`1.| + |.B`2.| <= |.w.| + |.s.| by A29,XREAL_1:7;
then
A30: dist(p,b) <= |.w.| + |.s.| by A10,A12,XXREAL_0:2;
0 + (|.w.| + |.s.|) <= |.e.| + |.n.| + (|.w.| + |.s.|) by A14,A13,
XREAL_1:7;
then |.w.| + |.s.| < r by A2,XREAL_1:8;
hence dist(p,b) < r by A30,XXREAL_0:2;
end;
end;
hence thesis by METRIC_1:11;
end;
theorem Th51:
for M being Reflexive symmetric triangle non empty MetrStruct,
z being Point of M holds r < 0 implies Sphere(z,r) = {}
proof
let M be Reflexive symmetric triangle non empty MetrStruct, z be Point of
M;
assume
A1: r < 0;
thus Sphere(z,r) c= {}
proof
let a be object;
assume
A2: a in Sphere(z,r);
then reconsider b = a as Point of M;
dist(b,z) = r by A2,METRIC_1:13;
hence thesis by A1,METRIC_1:5;
end;
thus thesis;
end;
theorem
for M being Reflexive discerning non empty MetrStruct, z being Point
of M holds Sphere(z,0) = {z}
proof
let M be Reflexive discerning non empty MetrStruct, z be Point of M;
thus Sphere(z,0) c= {z}
proof
let a be object;
assume
A1: a in Sphere(z,0);
then reconsider b = a as Point of M;
dist(z,b) = 0 by A1,METRIC_1:13;
then b = z by METRIC_1:2;
hence thesis by TARSKI:def 1;
end;
let a be object;
assume a in {z};
then
A2: a = z by TARSKI:def 1;
dist(z,z) = 0 by METRIC_1:1;
hence thesis by A2,METRIC_1:13;
end;
theorem
for M being Reflexive symmetric triangle non empty MetrStruct, z
being Point of M holds r < 0 implies cl_Ball(z,r) = {}
proof
let M be Reflexive symmetric triangle non empty MetrStruct, z be Point of
M;
A1: Sphere(z,r) \/ Ball(z,r) = cl_Ball(z,r) by METRIC_1:16;
assume
A2: r < 0;
then Ball(z,r) = {} by TBSP_1:12;
hence thesis by A2,A1,Th51;
end;
theorem
cl_Ball(z,0) = {z}
proof
thus cl_Ball(z,0) c= {z}
proof
let a be object;
assume
A1: a in cl_Ball(z,0);
then reconsider b = a as Point of M;
dist(b,z) <= 0 by A1,METRIC_1:12;
then dist(b,z) = 0 by METRIC_1:5;
then b = z by METRIC_1:2;
hence thesis by TARSKI:def 1;
end;
let a be object;
assume a in {z};
then
A2: a = z by TARSKI:def 1;
dist(z,z) = 0 by METRIC_1:1;
hence thesis by A2,METRIC_1:12;
end;
Lm1: for A being Subset of TopSpaceMetr M st A = cl_Ball(z,r) holds A` is open
proof
let A be Subset of TopSpaceMetr M such that
A1: A = cl_Ball(z,r);
for x being set holds x in A` iff ex Q being Subset of TopSpaceMetr M st
Q is open & Q c= A` & x in Q
proof
let x be set;
thus x in A` implies ex Q being Subset of TopSpaceMetr M st Q is open & Q
c= A` & x in Q
proof
assume
A2: x in A`;
then reconsider e = x as Point of M by TOPMETR:12;
reconsider Q = Ball(e,dist(e,z)-r) as Subset of TopSpaceMetr M by
TOPMETR:12;
take Q;
thus Q is open by TOPMETR:14;
thus Q c= A`
proof
let q be object;
assume
A3: q in Q;
then reconsider f = q as Point of M;
dist(e,z) <= dist(e,f) + dist(f,z) by METRIC_1:4;
then
A4: dist(e,z) - r <= dist(e,f) + dist(f,z) - r by XREAL_1:9;
dist(e,f) < dist(e,z)-r by A3,METRIC_1:11;
then dist(e,f) < dist(e,f) + dist(f,z) - r by A4,XXREAL_0:2;
then dist(e,f) - dist(e,f) < dist(e,f) + dist(f,z) - r - dist(e,f) by
XREAL_1:9;
then 0 < dist(e,f) - dist(e,f) + dist(f,z) - r;
then dist(f,z) > r by XREAL_1:47;
then not q in A by A1,METRIC_1:12;
hence thesis by A3,SUBSET_1:29;
end;
not x in A by A2,XBOOLE_0:def 5;
then dist(z,e) > r by A1,METRIC_1:12;
then dist(e,z)-r > r-r by XREAL_1:9;
hence thesis by TBSP_1:11;
end;
thus thesis;
end;
hence thesis by TOPS_1:25;
end;
theorem Th55:
for A being Subset of TopSpaceMetr M st A = cl_Ball(z,r) holds A is closed
proof
let A be Subset of TopSpaceMetr M;
assume A = cl_Ball(z,r);
then A` is open by Lm1;
hence thesis by TOPS_1:3;
end;
theorem
A = cl_Ball(w,r) implies A is closed
proof
A1: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider E=A as Subset of TopSpaceMetr Euclid n;
assume A = cl_Ball(w,r);
then E is closed by Th55;
hence A is closed by A1,PRE_TOPC:31;
end;
theorem Th57:
for r being Real for M be Reflexive symmetric triangle
non empty MetrStruct for x be Element of M holds cl_Ball(x,r) is bounded
proof
let r be Real;
let M be Reflexive symmetric triangle non empty MetrStruct;
let x be Element of M;
cl_Ball(x,r) c= Ball(x,r+1)
proof
let y be object such that
A1: y in cl_Ball(x,r);
reconsider Y=y as Point of M by A1;
A2: r+0<r+1 by XREAL_1:8;
dist(x,Y)<=r by A1,METRIC_1:12;
then dist(x,Y)<r+1 by A2,XXREAL_0:2;
hence thesis by METRIC_1:11;
end;
hence thesis by TBSP_1:14;
end;
theorem Th58:
for A being Subset of TopSpaceMetr M st A = Sphere(z,r) holds A is closed
proof
let A be Subset of TopSpaceMetr M such that
A1: A = Sphere(z,r);
reconsider B = cl_Ball(z,r), C = Ball(z,r) as Subset of TopSpaceMetr M by
TOPMETR:12;
A2: (cl_Ball(z,r))` = B` by TOPMETR:12;
A3: A` = B` \/ C
proof
hereby
let a be object;
assume
A4: a in A`;
then reconsider e = a as Point of M by TOPMETR:12;
not a in A by A4,XBOOLE_0:def 5;
then dist(e,z) <> r by A1,METRIC_1:13;
then dist(e,z) < r or dist(e,z) > r by XXREAL_0:1;
then e in Ball(z,r) or not e in cl_Ball(z,r) by METRIC_1:11,12;
then e in Ball(z,r) or e in cl_Ball(z,r)` by SUBSET_1:29;
hence a in B` \/ C by A2,XBOOLE_0:def 3;
end;
let a be object;
assume
A5: a in B` \/ C;
then reconsider e = a as Point of M by TOPMETR:12;
a in B` or a in C by A5,XBOOLE_0:def 3;
then not e in cl_Ball(z,r) or e in C by XBOOLE_0:def 5;
then dist(e,z) > r or dist(e,z) < r by METRIC_1:11,12;
then not a in A by A1,METRIC_1:13;
hence thesis by A5,SUBSET_1:29;
end;
A6: C is open by TOPMETR:14;
B` is open by Lm1;
hence thesis by A3,A6,TOPS_1:3;
end;
theorem
A = Sphere(w,r) implies A is closed
proof
A1: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider E=A as Subset of TopSpaceMetr Euclid n;
assume A = Sphere(w,r);
then E is closed by Th58;
hence A is closed by A1,PRE_TOPC:31;
end;
theorem
Sphere(z,r) is bounded
proof
Sphere(z,r) c= cl_Ball(z,r) by METRIC_1:15;
hence thesis by Th57,TBSP_1:14;
end;
theorem
A is bounded implies Cl A is bounded;
theorem
for M being non empty MetrStruct holds M is bounded iff for X being
Subset of M holds X is bounded
proof
let M be non empty MetrStruct;
hereby
assume
A1: M is bounded;
let X be Subset of M;
[#]M is bounded by A1;
hence X is bounded by TBSP_1:14;
end;
assume for X being Subset of M holds X is bounded;
then [#]M is bounded;
hence thesis by TBSP_1:18;
end;
theorem Th63:
for M being Reflexive symmetric triangle non empty MetrStruct,
X, Y being Subset of M st the carrier of M = X \/ Y & M is non bounded & X is
bounded holds Y is non bounded
proof
let M be Reflexive symmetric triangle non empty MetrStruct, X, Y be Subset
of M such that
A1: the carrier of M = X \/ Y and
A2: M is non bounded;
assume that
A3: X is bounded and
A4: Y is bounded;
[#]M is bounded by A1,A3,A4,TBSP_1:13;
hence thesis by A2,TBSP_1:18;
end;
theorem
for X, Y being Subset of TOP-REAL n st n >= 1 & the carrier of
TOP-REAL n = X \/ Y & X is bounded holds Y is non bounded
proof
set M = TOP-REAL n;
let X, Y be Subset of M such that
A1: n >= 1 and
A2: the carrier of M = X \/ Y;
reconsider E = [#]M as Subset of Euclid n by TOPREAL3:8;
[#](TOP-REAL n) is non bounded by A1,JORDAN2C:35;
then
A3: E is non bounded by JORDAN2C:11;
reconsider D = Y as Subset of Euclid n by TOPREAL3:8;
assume X is bounded;
then reconsider C = X as bounded Subset of Euclid n by JORDAN2C:11;
A4: the carrier of Euclid n = C \/ D by A2,TOPREAL3:8;
E = [#]Euclid n by TOPREAL3:8;
then Euclid n is non bounded by A3;
then D is non bounded by A4,Th63;
hence thesis by JORDAN2C:11;
end;
theorem Th65:
A is bounded & B is bounded implies A \/ B is bounded
proof
assume A is bounded;
then
A1: A is bounded Subset of Euclid n by JORDAN2C:11;
then reconsider A as Subset of Euclid n;
assume B is bounded;
then
A2: B is bounded Subset of Euclid n by JORDAN2C:11;
then reconsider B as Subset of Euclid n;
reconsider E = A \/ B as Subset of Euclid n;
E is bounded Subset of Euclid n by A1,A2,TBSP_1:13;
hence thesis by JORDAN2C:11;
end;
begin :: Topological properties of real numbers subsets
registration
let X be non empty Subset of REAL;
cluster Cl X -> non empty;
coherence by MEASURE6:58,XBOOLE_1:3;
end;
registration
let D be bounded_below Subset of REAL;
cluster Cl D -> bounded_below;
coherence
proof
consider p being Real such that
A1: p is LowerBound of D by XXREAL_2:def 9;
A2: for r being Real st r in D holds p <= r by A1,XXREAL_2:def 2;
take p;
let r be ExtReal;
assume r in Cl D;
then consider s being Real_Sequence such that
A3: rng s c= D and
A4: s is convergent and
A5: lim s = r by MEASURE6:64;
for n holds s.n >= p
proof
let n;
A6: n in NAT by ORDINAL1:def 12;
dom s = NAT by FUNCT_2:def 1;
then s.n in rng s by A6,FUNCT_1:def 3;
hence thesis by A2,A3;
end;
hence thesis by A4,A5,PREPOWER:1;
end;
end;
registration
let D be bounded_above Subset of REAL;
cluster Cl D -> bounded_above;
coherence
proof
consider p being Real such that
A1: p is UpperBound of D by XXREAL_2:def 10;
A2: for r being Real st r in D holds r <= p by A1,XXREAL_2:def 1;
take p;
let r be ExtReal;
assume r in Cl D;
then consider s being Real_Sequence such that
A3: rng s c= D and
A4: s is convergent and
A5: lim s = r by MEASURE6:64;
for n holds s.n <= p
proof
let n;
A6: n in NAT by ORDINAL1:def 12;
dom s = NAT by FUNCT_2:def 1;
then s.n in rng s by A6,FUNCT_1:def 3;
hence thesis by A2,A3;
end;
hence thesis by A4,A5,PREPOWER:2;
end;
end;
theorem Th66:
for D being non empty bounded_below Subset of REAL holds lower_bound D =
lower_bound Cl D
proof
let D be non empty bounded_below Subset of REAL;
A1: for q being Real st for p being Real st p in D holds p >=
q holds lower_bound Cl D >= q
proof
let q be Real such that
A2: for p being Real st p in D holds p >= q;
for p being Real st p in Cl D holds p >= q
proof
let p be Real;
assume p in Cl D;
then consider s being Real_Sequence such that
A3: rng s c= D and
A4: s is convergent and
A5: lim s = p by MEASURE6:64;
for n holds s.n >= q
proof
let n;
A6: n in NAT by ORDINAL1:def 12;
dom s = NAT by FUNCT_2:def 1;
then s.n in rng s by A6,FUNCT_1:def 3;
hence thesis by A2,A3;
end;
hence thesis by A4,A5,PREPOWER:1;
end;
hence thesis by SEQ_4:43;
end;
A7: lower_bound Cl D <= lower_bound D by MEASURE6:58,SEQ_4:47;
for p being Real st p in D holds p >= lower_bound Cl D
proof
let p be Real;
assume p in D;
then lower_bound D <= p by SEQ_4:def 2;
hence thesis by A7,XXREAL_0:2;
end;
hence thesis by A1,SEQ_4:44;
end;
theorem Th67:
for D being non empty bounded_above Subset of REAL holds upper_bound D =
upper_bound Cl D
proof
let D be non empty bounded_above Subset of REAL;
A1: for q being Real st for p being Real st p in D holds p <=
q holds upper_bound Cl D <= q
proof
let q be Real such that
A2: for p being Real st p in D holds p <= q;
for p being Real st p in Cl D holds p <= q
proof
let p be Real;
assume p in Cl D;
then consider s being Real_Sequence such that
A3: rng s c= D and
A4: s is convergent and
A5: lim s = p by MEASURE6:64;
for n holds s.n <= q
proof
let n;
A6: n in NAT by ORDINAL1:def 12;
dom s = NAT by FUNCT_2:def 1;
then s.n in rng s by A6,FUNCT_1:def 3;
hence thesis by A2,A3;
end;
hence thesis by A4,A5,PREPOWER:2;
end;
hence thesis by SEQ_4:45;
end;
A7: upper_bound Cl D >= upper_bound D by MEASURE6:58,SEQ_4:48;
for p being Real st p in D holds p <= upper_bound Cl D
proof
let p be Real;
assume p in D;
then upper_bound D >= p by SEQ_4:def 1;
hence thesis by A7,XXREAL_0:2;
end;
hence thesis by A1,SEQ_4:46;
end;
registration
cluster R^1 -> T_2;
coherence by PCOMPS_1:34,TOPMETR:def 6;
end;
::$CT 5
theorem Th68:
for A, B being Subset of REAL, f being Function of [:R^1,R^1:],
TOP-REAL 2 st for x, y being Real holds f. [x,y] = <*x,y*> holds f.:[:A,B:] =
product ((1,2) --> (A,B))
proof
let A, B be Subset of REAL, f be Function of [:R^1,R^1:], TOP-REAL 2 such
that
A1: for x, y being Real holds f. [x,y] = <*x,y*>;
set h = (1,2) --> (A,B);
A2: dom h = {1,2} by FUNCT_4:62;
thus f.:[:A,B:] c= product h
proof
let x be object;
assume x in f.:[:A,B:];
then consider a being object such that
A3: a in the carrier of [:R^1,R^1:] and
A4: a in [:A,B:] and
A5: f.a = x by FUNCT_2:64;
reconsider a as Point of [:R^1,R^1:] by A3;
consider m, n being object such that
A6: m in A and
A7: n in B and
A8: a = [m,n] by A4,ZFMISC_1:def 2;
f.a = x by A5;
then reconsider g = x as Function of Seg 2, REAL by EUCLID:23;
reconsider m, n as Real by A6,A7;
A9: for y being object st y in dom h holds g.y in h.y
proof
let y be object;
assume y in dom h;
then
A11: y = 1 or y = 2 by TARSKI:def 2;
f. [m,n] = |[m,n]| by A1;
hence thesis by A5,A6,A7,A8,A11,FUNCT_4:63;
end;
dom g = dom h by A2,FINSEQ_1:2,FUNCT_2:def 1;
hence thesis by A9,CARD_3:9;
end;
A13: h.2 = B by FUNCT_4:63;
let a be object;
assume a in product h;
then consider g being Function such that
A14: a = g and
A15: dom g = dom h and
A16: for x being object st x in dom h holds g.x in h.x by CARD_3:def 5;
2 in dom h by A2,TARSKI:def 2;
then
A17: g.2 in B by A13,A16;
A18: h.1 = A by FUNCT_4:63;
1 in dom h by A2,TARSKI:def 2;
then
A19: g.1 in A by A18,A16;
then
A20: f. [g.1,g.2] = <*g.1,g.2*> by A1,A17;
A21: now
let k be object;
assume k in dom g;
then k = 1 or k = 2 by A15,TARSKI:def 2;
hence g.k = <*g.1,g.2*>.k;
end;
A22: dom <*g.1,g.2*> = {1,2} by FINSEQ_1:2,89;
A23: [g.1,g.2] in [:A,B:] by A19,A17,ZFMISC_1:87;
the carrier of [:R^1,R^1:] = [:the carrier of R^1,the carrier of R^1 :]
by BORSUK_1:def 2;
then [g.1,g.2] in the carrier of [:R^1,R^1:] by A19,A17,TOPMETR:17
,ZFMISC_1:87;
hence thesis by A2,A14,A15,A23,A22,A21,A20,FUNCT_1:2,FUNCT_2:35;
end;
theorem Th69:
for f being Function of [:R^1,R^1:], TOP-REAL 2 st for x, y
being Real holds f. [x,y] = <*x,y*> holds f is being_homeomorphism
proof
reconsider f1 = proj1, f2 = proj2 as Function of TOP-REAL 2, R^1 by
TOPMETR:17;
let f be Function of [:R^1,R^1:], TOP-REAL 2 such that
A1: for x, y being Real holds f. [x,y] = <*x,y*>;
thus dom f = [#][:R^1,R^1:] by FUNCT_2:def 1;
A2: the carrier of [:R^1,R^1:] = [:the carrier of R^1,the carrier of R^1:]
by BORSUK_1:def 2;
then
A3: dom f = [:the carrier of R^1,the carrier of R^1:] by FUNCT_2:def 1;
thus
A4: rng f = [#]TOP-REAL 2
proof
thus rng f c= [#]TOP-REAL 2;
let y be object;
assume y in [#]TOP-REAL 2;
then consider a, b being Element of REAL such that
A5: y = <*a,b*> by EUCLID:51;
A6: f. [a,b] = <*a,b*> by A1;
reconsider a,b as Element of REAL;
[a,b] in dom f by A3,TOPMETR:17,ZFMISC_1:87;
hence thesis by A5,A6,FUNCT_1:def 3;
end;
thus
A7: f is one-to-one
proof
let x, y be object;
assume x in dom f;
then consider x1, x2 being object such that
A8: x1 in REAL and
A9: x2 in REAL and
A10: x = [x1,x2] by A2,TOPMETR:17,ZFMISC_1:def 2;
assume y in dom f;
then consider y1, y2 being object such that
A11: y1 in REAL and
A12: y2 in REAL and
A13: y = [y1,y2] by A2,TOPMETR:17,ZFMISC_1:def 2;
reconsider x1, x2, y1, y2 as Real by A8,A9,A11,A12;
assume
A14: f.x = f.y;
A15: f. [y1,y2] = <*y1,y2*> by A1;
A16: f. [x1,x2] = <*x1,x2*> by A1;
then x1 = y1 by A10,A13,A15,A14,FINSEQ_1:77;
hence thesis by A10,A13,A16,A15,A14,FINSEQ_1:77;
end;
A17: now
A18: dom f2 = the carrier of TOP-REAL 2 by FUNCT_2:def 1;
let x be object;
A19: dom f1 = the carrier of TOP-REAL 2 by FUNCT_2:def 1;
assume
A20: x in dom (f");
then consider a, b being Element of REAL such that
A21: x = <*a,b*> by EUCLID:51;
reconsider a,b as Element of REAL;
reconsider p = x as Point of TOP-REAL 2 by A20;
A22: [a,b] in dom f by A3,TOPMETR:17,ZFMISC_1:87;
A23: f. [a,b] = <*a,b*> by A1;
f is onto by A4,FUNCT_2:def 3;
hence f".x = (f qua Function)".x by A7,TOPS_2:def 4
.= [a,b] by A7,A21,A22,A23,FUNCT_1:32
.= [p`1,b] by A21
.= [p`1,p`2] by A21
.= [f1.x,p`2] by PSCOMP_1:def 5
.= [f1.x,f2.x] by PSCOMP_1:def 6
.= <:f1,f2:>.x by A20,A19,A18,FUNCT_3:49;
end;
thus f is continuous
proof
let w be Point of [:R^1,R^1:], G be a_neighborhood of f.w;
reconsider fw = f.w as Point of Euclid 2 by TOPREAL3:8;
consider x, y being object such that
A24: x in the carrier of R^1 and
A25: y in the carrier of R^1 and
A26: w = [x,y] by A2,ZFMISC_1:def 2;
reconsider x, y as Real by A24,A25;
fw in Int G by CONNSP_2:def 1;
then consider r being Real such that
A27: r > 0 and
A28: Ball(fw,r) c= G by GOBOARD6:5;
reconsider r as Real;
set A = ].(f.w)`1-r/sqrt 2,(f.w)`1+r/sqrt 2.[, B = ].(f.w)`2-r/sqrt 2,(f.w
)`2+r/sqrt 2.[;
reconsider A, B as Subset of R^1 by TOPMETR:17;
A29: f. [x,y] = <*x,y*> by A1;
then y = (f.w)`2 by A26;
then
A30: y in B by A27,Th14,SQUARE_1:19,XREAL_1:139;
x = (f.w)`1 by A26,A29;
then x in A by A27,Th14,SQUARE_1:19,XREAL_1:139;
then
A31: w in [:A,B:] by A26,A30,ZFMISC_1:87;
take [:A,B:];
A32: B is open by JORDAN6:35;
A is open by JORDAN6:35;
then [:A,B:] in Base-Appr [:A,B:] by A32;
then w in union Base-Appr [:A,B:] by A31,TARSKI:def 4;
then w in Int [:A,B:] by BORSUK_1:14;
hence [:A,B:] is a_neighborhood of w by CONNSP_2:def 1;
product ((1,2)-->(A,B)) c= Ball(fw,r) by Th39;
then f.:[:A,B:] c= Ball(fw,r) by A1,Th68;
hence thesis by A28;
end;
A33: f1 is continuous by JORDAN5A:27;
A34: f2 is continuous by JORDAN5A:27;
dom <:f1,f2:> = the carrier of TOP-REAL 2 by FUNCT_2:def 1;
then f" = <:f1,f2:> by A4,A7,A17,TOPS_2:49;
hence thesis by A33,A34,YELLOW12:41;
end;
theorem
[:R^1,R^1:], TOP-REAL 2 are_homeomorphic
proof
defpred P[Real,Real,set] means ex c being Element of
REAL 2 st c = $3 & $3 = <*$1,$2*>;
A1: the carrier of TOP-REAL 2 = REAL 2 by EUCLID:22;
A2: for x, y being Element of REAL ex u being Element of REAL 2 st P[x,y,u]
proof
let x, y be Element of REAL;
take <*x,y*>;
thus <*x,y*> is Element of REAL 2 by FINSEQ_2:137;
<*x,y*> in 2-tuples_on REAL by FINSEQ_2:137;
hence thesis;
end;
consider f being Function of [:REAL,REAL:],REAL 2 such that
A3: for x, y being Element of REAL holds P[x,y,f.(x,y)] from BINOP_1:sch
3(A2);
the carrier of [:R^1,R^1:] = [:the carrier of R^1,the carrier of R^1 :]
by BORSUK_1:def 2;
then reconsider f as Function of [:R^1,R^1:], TOP-REAL 2 by A1,TOPMETR:17;
take f;
for x, y being Real holds f. [x,y] = <*x,y*>
proof
let x, y be Real;
x in REAL & y in REAL by XREAL_0:def 1;
then P[x,y,f.(x,y)] by A3;
hence thesis;
end;
hence thesis by Th69;
end;
begin :: bounded subsets
theorem Th71:
for A, B being compact Subset of REAL holds product ((1,2) --> (
A,B)) is compact Subset of TOP-REAL 2
proof
defpred P[Real,Real,set] means ex c being Element of
REAL 2 st c = $3 & $3 = <*$1,$2*>;
let A, B be compact Subset of REAL;
reconsider X = product ((1,2) --> (A,B)) as Subset of TOP-REAL 2 by Th20;
reconsider A1 = A, B1 = B as Subset of R^1 by TOPMETR:17;
A1: the carrier of TOP-REAL 2 = REAL 2 by EUCLID:22;
A2: for x, y being Element of REAL ex u being Element of REAL 2 st P[x,y,u]
proof
let x, y be Element of REAL;
take <*x,y*>;
thus <*x,y*> is Element of REAL 2 by FINSEQ_2:137;
<*x,y*> in 2-tuples_on REAL by FINSEQ_2:137;
hence thesis;
end;
consider h being Function of [:REAL,REAL:],REAL 2 such that
A3: for x, y being Element of REAL holds P[x,y,h.(x,y)] from BINOP_1:sch
3(A2);
the carrier of [:R^1,R^1:] = [:the carrier of R^1,the carrier of R^1 :]
by BORSUK_1:def 2;
then reconsider h as Function of [:R^1,R^1:], TOP-REAL 2 by A1,TOPMETR:17;
A4: for x, y being Real holds h. [x,y] = <*x,y*>
proof
let x, y be Real;
x in REAL & y in REAL by XREAL_0:def 1;
then P[x,y,h.(x,y)] by A3;
hence thesis;
end;
then
A5: h is being_homeomorphism by Th69;
A6: B1 is compact by JORDAN5A:25;
A1 is compact by JORDAN5A:25;
then
A7: [:A1,B1:] is compact by A6,BORSUK_3:23;
h.:[:A1,B1:] = X by A4,Th68;
hence thesis by A7,A5,WEIERSTR:8;
end;
theorem Th72:
P is bounded closed implies P is compact
proof
assume
A1: P is bounded closed;
then reconsider C = P as bounded Subset of Euclid 2 by JORDAN2C:11;
consider r being Real, e such that
0 < r and
A2: C c= Ball(e,r) by METRIC_6:def 3;
reconsider p = e as Point of TOP-REAL 2 by TOPREAL3:8;
A3: ].p`2-r,p`2+r.[ c= [.p`2-r,p`2+r .] by XXREAL_1:25;
A4: Ball(e,r) c= product ((1,2)-->(].p`1-r,p`1+r.[,].p`2-r,p`2+r.[)) by Th40;
].p`1-r,p`1+r.[ c= [.p`1-r,p`1+r.] by XXREAL_1:25;
then
product ((1,2)-->(].p`1-r,p`1+r.[,].p`2-r,p`2+r.[)) c= product ((1,2)-->
([.p`1-r,p`1+r.],[.p`2-r,p`2+r.])) by A3,Th19;
then
A5: Ball(e,r) c= product ((1,2)-->([.p`1-r,p`1+r.],[.p`2-r,p`2+r.])) by A4;
product ((1,2)-->([.p`1-r,p`1+r.],[.p`2-r,p`2+r.])) is compact Subset of
TOP-REAL 2 by Th71;
hence thesis by A1,A2,A5,COMPTS_1:9,XBOOLE_1:1;
end;
theorem Th73:
P is bounded implies for g being continuous RealMap of TOP-REAL
2 holds Cl(g.:P) c= g.:Cl P
proof
assume P is bounded;
then
A1: Cl P is compact by Th72;
let g be continuous RealMap of TOP-REAL 2;
reconsider f = g as Function of TOP-REAL 2, R^1 by TOPMETR:17;
f is continuous by JORDAN5A:27;
then f.:Cl P is closed by A1,COMPTS_1:7,WEIERSTR:9;
then
A2: g.:Cl P is closed by JORDAN5A:23;
g.:P c= g.:Cl P by PRE_TOPC:18,RELAT_1:123;
hence thesis by A2,MEASURE6:57;
end;
theorem Th74:
proj1.:Cl P c= Cl(proj1.:P)
proof
let y be object;
assume y in proj1.:Cl P;
then consider x being object such that
A1: x in the carrier of TOP-REAL 2 and
A2: x in Cl P and
A3: y = proj1.x by FUNCT_2:64;
reconsider x as Point of TOP-REAL 2 by A1;
set r = proj1.x;
for O being open Subset of REAL st y in O holds O /\ proj1.:P is non empty
proof
reconsider e = x as Point of Euclid 2 by TOPREAL3:8;
let O be open Subset of REAL;
assume y in O;
then consider g being Real such that
A4: 0 < g and
A5: ].r-g,r+g.[ c= O by A3,RCOMP_1:19;
reconsider g as Real;
reconsider B = Ball(e,g/2) as Subset of TOP-REAL 2 by TOPREAL3:8;
A6: B is open by GOBOARD6:3;
e in B by A4,TBSP_1:11,XREAL_1:139;
then P meets B by A2,A6,TOPS_1:12;
then P /\ B <> {};
then consider d being Point of TOP-REAL 2 such that
A7: d in P /\ B by SUBSET_1:4;
A8: d in B by A7,XBOOLE_0:def 4;
then x`1-g/2 < d`1 by Th37;
then
A9: r-g/2 < d`1 by PSCOMP_1:def 5;
d`1 < x`1+g/2 by A8,Th37;
then
A10: d`1 < r+g/2 by PSCOMP_1:def 5;
d in P by A7,XBOOLE_0:def 4;
then proj1.d in proj1.:P by FUNCT_2:35;
then
A11: d`1 in proj1.:P by PSCOMP_1:def 5;
A12: g/2 < g/1 by A4,XREAL_1:76;
then r-g < r-g/2 by XREAL_1:15;
then
A13: r-g < d`1 by A9,XXREAL_0:2;
r+g/2 < r+g by A12,XREAL_1:6;
then
A14: d`1 < r+g by A10,XXREAL_0:2;
].r-g,r+g.[ = {t where t is Real: r-g < t & t < r+g}
by RCOMP_1:def 2;
then d`1 in ].r-g,r+g.[ by A13,A14;
hence thesis by A5,A11,XBOOLE_0:def 4;
end;
hence thesis by A3,MEASURE6:63;
end;
theorem Th75:
proj2.:Cl P c= Cl(proj2.:P)
proof
let y be object;
assume y in proj2.:Cl P;
then consider x being object such that
A1: x in the carrier of TOP-REAL 2 and
A2: x in Cl P and
A3: y = proj2.x by FUNCT_2:64;
reconsider x as Point of TOP-REAL 2 by A1;
set r = proj2.x;
for O being open Subset of REAL st y in O holds O /\ proj2.:P is non empty
proof
reconsider e = x as Point of Euclid 2 by TOPREAL3:8;
let O be open Subset of REAL;
assume y in O;
then consider g being Real such that
A4: 0 < g and
A5: ].r-g,r+g.[ c= O by A3,RCOMP_1:19;
reconsider g as Real;
reconsider B = Ball(e,g/2) as Subset of TOP-REAL 2 by TOPREAL3:8;
A6: B is open by GOBOARD6:3;
e in B by A4,TBSP_1:11,XREAL_1:139;
then P meets B by A2,A6,TOPS_1:12;
then P /\ B <> {};
then consider d being Point of TOP-REAL 2 such that
A7: d in P /\ B by SUBSET_1:4;
A8: d in B by A7,XBOOLE_0:def 4;
then x`2-g/2 < d`2 by Th38;
then
A9: r-g/2 < d`2 by PSCOMP_1:def 6;
d`2 < x`2+g/2 by A8,Th38;
then
A10: d`2 < r+g/2 by PSCOMP_1:def 6;
d in P by A7,XBOOLE_0:def 4;
then proj2.d in proj2.:P by FUNCT_2:35;
then
A11: d`2 in proj2.:P by PSCOMP_1:def 6;
A12: g/2 < g/1 by A4,XREAL_1:76;
then r-g < r-g/2 by XREAL_1:15;
then
A13: r-g < d`2 by A9,XXREAL_0:2;
r+g/2 < r+g by A12,XREAL_1:6;
then
A14: d`2 < r+g by A10,XXREAL_0:2;
].r-g,r+g.[ = {t where t is Real: r-g < t & t < r+g}
by RCOMP_1:def 2;
then d`2 in ].r-g,r+g.[ by A13,A14;
hence thesis by A5,A11,XBOOLE_0:def 4;
end;
hence thesis by A3,MEASURE6:63;
end;
theorem Th76:
P is bounded implies Cl(proj1.:P) = proj1.:Cl P
by Th73,Th74;
theorem Th77:
P is bounded implies Cl(proj2.:P) = proj2.:Cl P
by Th73,Th75;
theorem
D is bounded implies W-bound D = W-bound Cl D
proof
A1: D c= Cl D by PRE_TOPC:18;
assume
A2: D is bounded;
then Cl D is compact by Th72;
then proj1.:Cl D is bounded_below;
then proj1.:D is bounded_below by A1,RELAT_1:123,XXREAL_2:44;
then
A3: lower_bound (proj1.:D) = lower_bound Cl(proj1.:D) by Th66
.= lower_bound (proj1.:Cl D) by A2,Th76;
W-bound D = lower_bound (proj1.:D) by SPRECT_1:43;
hence thesis by A3,SPRECT_1:43;
end;
theorem
D is bounded implies E-bound D = E-bound Cl D
proof
A1: D c= Cl D by PRE_TOPC:18;
assume
A2: D is bounded;
then Cl D is compact by Th72;
then proj1.:Cl D is bounded_above;
then proj1.:D is bounded_above by A1,RELAT_1:123,XXREAL_2:43;
then
A3: upper_bound (proj1.:D) = upper_bound Cl(proj1.:D) by Th67
.= upper_bound (proj1.:Cl D) by A2,Th76;
E-bound D = upper_bound (proj1.:D) by SPRECT_1:46;
hence thesis by A3,SPRECT_1:46;
end;
theorem
D is bounded implies N-bound D = N-bound Cl D
proof
A1: D c= Cl D by PRE_TOPC:18;
assume
A2: D is bounded;
then Cl D is compact by Th72;
then proj2.:Cl D is bounded_above;
then proj2.:D is bounded_above by A1,RELAT_1:123,XXREAL_2:43;
then
A3: upper_bound (proj2.:D) = upper_bound Cl(proj2.:D) by Th67
.= upper_bound (proj2.:Cl D) by A2,Th77;
N-bound D = upper_bound (proj2.:D) by SPRECT_1:45;
hence thesis by A3,SPRECT_1:45;
end;
theorem
D is bounded implies S-bound D = S-bound Cl D
proof
A1: D c= Cl D by PRE_TOPC:18;
assume
A2: D is bounded;
then Cl D is compact by Th72;
then proj2.:Cl D is bounded_below;
then proj2.:D is bounded_below by A1,RELAT_1:123,XXREAL_2:44;
then
A3: lower_bound (proj2.:D) = lower_bound Cl(proj2.:D) by Th66
.= lower_bound (proj2.:Cl D) by A2,Th77;
S-bound D = lower_bound (proj2.:D) by SPRECT_1:44;
hence thesis by A3,SPRECT_1:44;
end;
:: Moved from JORDAN1I, AK, 23.02.2006
theorem Th82:
for A,B being Subset of TOP-REAL n holds A is bounded or B is
bounded implies A /\ B is bounded
proof
let A,B be Subset of TOP-REAL n;
assume
A1: A is bounded or B is bounded;
per cases by A1;
suppose
A is bounded;
hence thesis by RLTOPSP1:42,XBOOLE_1:17;
end;
suppose
B is bounded;
hence thesis by RLTOPSP1:42,XBOOLE_1:17;
end;
end;
theorem
for A,B being Subset of TOP-REAL n holds A is not bounded & B is
bounded implies A \ B is not bounded
proof
let A,B be Subset of TOP-REAL n;
assume that
A1: A is not bounded and
A2: B is bounded;
A3: (A \ B) \/ A /\ B = A \ (B \ B) by XBOOLE_1:52
.= A \ {} by XBOOLE_1:37
.= A;
A /\ B is bounded by A2,Th82;
hence thesis by A1,A3,Th65;
end;
begin :: Addenda
::form GOBRD14, 2006.03.26, A.T.
definition
let n be Nat, a, b be Point of TOP-REAL n;
func dist(a,b) -> Real means
:Def1:
ex p, q being Point of Euclid n st p = a & q = b & it = dist(p,q);
existence
proof
reconsider p = a, q = b as Point of Euclid n by TOPREAL3:8;
take dist(p,q);
thus thesis;
end;
uniqueness;
commutativity;
end;
reserve r1,r2,s1,s2 for Real;
theorem Th84:
for u,v being Point of Euclid 2 st u = |[r1,s1]| & v = |[r2,s2
]| holds dist(u,v) =sqrt ((r1 - r2)^2 + (s1 - s2)^2)
proof
let u,v be Point of Euclid 2 such that
A1: u = |[r1,s1]| and
A2: v = |[r2,s2]|;
A3: |[r1,s1]|`1 = r1;
A4: |[r2,s2]|`2 = s2;
A5: |[r2,s2]|`1 = r2;
A6: |[r1,s1]|`2 = s1;
thus dist(u,v) = (Pitag_dist 2).(u,v) by METRIC_1:def 1
.= sqrt ((r1 - r2)^2 + (s1 - s2)^2) by A1,A2,A3,A6,A5,A4,TOPREAL3:7;
end;
theorem Th85:
dist(p,q) = sqrt ((p`1-q`1)^2 + (p`2-q`2)^2)
proof
A1: p = |[p`1, p`2]| by EUCLID:53;
A2: q = |[q`1, q`2]| by EUCLID:53;
ex a, b being Point of Euclid 2 st p = a & q = b & dist(a,b) = dist(p,q)
by Def1;
hence thesis by A1,A2,Th84;
end;
theorem
for p being Point of TOP-REAL n holds dist(p,p) = 0
proof
let p be Point of TOP-REAL n;
ex a, b being Point of Euclid n st a = p & b = p & dist(a,b) = dist(p,p)
by Def1;
hence thesis by METRIC_1:1;
end;
theorem
for p, q, r being Point of TOP-REAL n holds dist(p,r) <= dist (p,q) +
dist(q,r)
proof
let p, q, r be Point of TOP-REAL n;
A1: ex a, b being Point of Euclid n st a = p & b = r & dist(a,b) = dist(p,r
) by Def1;
A2: ex a, b being Point of Euclid n st a = q & b = r & dist(a,b) = dist(q,r)
by Def1;
ex a, b being Point of Euclid n st a = p & b = q & dist(a,b) = dist(p,q
) by Def1;
hence thesis by A1,A2,METRIC_1:4;
end;
theorem
for x1, x2, y1, y2 being Real, a, b being Point of TOP-REAL 2
st x1 <= a`1 & a`1 <= x2 & y1 <= a`2 & a`2 <= y2 & x1 <= b`1 & b`1 <= x2 & y1
<= b`2 & b`2 <= y2 holds dist(a,b) <= (x2-x1) + (y2-y1)
proof
let x1, x2, y1, y2 be Real, a, b be Point of TOP-REAL 2 such that
A1: x1 <= a`1 and
A2: a`1 <= x2 and
A3: y1 <= a`2 and
A4: a`2 <= y2 and
A5: x1 <= b`1 and
A6: b`1 <= x2 and
A7: y1 <= b`2 and
A8: b`2 <= y2;
A9: |.a`2-b`2.| <= y2 - y1 by A3,A4,A7,A8,JGRAPH_1:27;
A10: (a`1-b`1)^2 >= 0 by XREAL_1:63;
A11: (a`2-b`2)^2 >= 0 by XREAL_1:63;
dist(a,b) = sqrt ((a`1-b`1)^2 + (a`2-b`2)^2) by Th85;
then dist(a,b) <= sqrt(a`1-b`1)^2 + sqrt(a`2-b`2)^2
by A10,A11,SQUARE_1:59;
then dist(a,b) <= |.a`1-b`1.| + sqrt(a`2-b`2)^2 by COMPLEX1:72;
then
A12: dist(a,b) <= |.a`1-b`1.| + |.a`2-b`2.| by COMPLEX1:72;
|.a`1-b`1.| <= x2 - x1 by A1,A2,A5,A6,JGRAPH_1:27;
then |.a`1-b`1.| + |.a`2-b`2.| <= (x2 - x1) + (y2 - y1) by A9,XREAL_1:7;
hence thesis by A12,XXREAL_0:2;
end;