Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Artur Kornilowicz
- Received February 19, 1999
- MML identifier: TOPREAL6
- [
Mizar article,
MML identifier index
]
environ
vocabulary ARYTM, METRIC_1, PRE_TOPC, EUCLID, SQUARE_1, ARYTM_1, ARYTM_3,
RELAT_1, ABSVALUE, FINSEQ_2, FINSEQ_1, FUNCT_1, GROUP_1, RVSUM_1,
RCOMP_1, ORDINAL2, SEQ_2, LATTICES, FINSET_1, PCOMPS_1, RELAT_2,
SUBSET_1, BOOLE, CONNSP_1, COMPTS_1, T_0TOPSP, TOPS_2, SETFAM_1, TARSKI,
CARD_3, FUNCOP_1, CAT_1, COMPLEX1, RLVECT_1, MCART_1, TOPREAL1, PSCOMP_1,
JORDAN1, SPPOL_1, TOPREAL4, TOPREAL2, SPRECT_1, FUNCT_5, JORDAN2C, SEQ_1,
TOPMETR, CONNSP_2, TOPS_1, BORSUK_1, PARTFUN1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
FUNCT_3, BINOP_1, FINSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1,
SQUARE_1, NAT_1, ABSVALUE, BINARITH, CQC_LANG, FUNCT_4, SEQ_1, SEQ_2,
SEQ_4, STRUCT_0, GROUP_1, METRIC_1, TBSP_1, FINSEQ_1, FINSEQ_2, RVSUM_1,
NEWTON, CARD_3, FINSEQ_4, RCOMP_1, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_1,
CONNSP_2, COMPTS_1, BORSUK_1, PCOMPS_1, EUCLID, WEIERSTR, TOPMETR,
TOPREAL1, TOPREAL2, T_0TOPSP, JORDAN1, TOPREAL4, PSCOMP_1, SPPOL_1,
JGRAPH_1, SPRECT_1, JORDAN2C;
constructors BINARITH, BORSUK_3, CARD_4, COMPTS_1, CONNSP_1, FINSEQOP,
FINSEQ_4, GOBOARD9, JORDAN1, JORDAN2C, LIMFUNC1, PSCOMP_1, RCOMP_1,
REAL_1, REALSET1, SPPOL_1, SPRECT_1, TBSP_1, TOPGRP_1, TOPREAL2,
TOPREAL4, TOPS_1, TOPS_2, WAYBEL_3, WEIERSTR, CQC_LANG, TOPRNS_1,
MEMBERED, PARTFUN1;
clusters SUBSET_1, XREAL_0, BORSUK_1, BORSUK_3, FUNCT_4, EUCLID, FINSET_1,
GOBOARD9, METRIC_1, PCOMPS_1, PRE_TOPC, PSCOMP_1, RCOMP_1, RELSET_1,
SPRECT_1, SPRECT_2, STRUCT_0, TEX_4, TOPGRP_1, TOPMETR, TOPS_1, WAYBEL_2,
WAYBEL12, YELLOW13, ARYTM_3, SQUARE_1, FINSEQ_5, MEMBERED, ZFMISC_1,
NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Real numbers
reserve a, b for real number,
r 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;
canceled 5;
theorem :: TOPREAL6:6
0 <= a & 0 <= b implies sqrt(a+b) <= sqrt a + sqrt b;
theorem :: TOPREAL6:7
0 <= a & a <= b implies abs(a) <= abs(b);
theorem :: TOPREAL6:8
b <= a & a <= 0 implies abs(a) <= abs(b);
theorem :: TOPREAL6:9
Product(0|->r) = 1;
theorem :: TOPREAL6:10
Product(1|->r) = r;
theorem :: TOPREAL6:11
Product(2|->r) = r * r;
theorem :: TOPREAL6:12
Product((n+1)|->r) = (Product(n|->r))*r;
theorem :: TOPREAL6:13
j <> 0 & r = 0 iff Product(j|->r) = 0;
theorem :: TOPREAL6:14
r <> 0 & j <= i implies Product((i-'j)|->r) = Product(i|->r) / Product(j|->r);
theorem :: TOPREAL6:15
r <> 0 & j <= i implies r|^(i-'j) = r|^i / r|^j;
reserve a, b for Real;
theorem :: TOPREAL6:16
sqr <*a,b*> = <*a^2,b^2*>;
theorem :: TOPREAL6:17
for F being FinSequence of REAL st i in dom abs F & a = F.i holds
(abs F).i = abs(a);
theorem :: TOPREAL6:18
abs <*a,b*> = <*abs(a),abs(b)*>;
theorem :: TOPREAL6:19
for a, b, c, d being real number st a <= b & c <= d holds
abs(b-a) + abs(d-c) = (b-a) + (d-c);
theorem :: TOPREAL6:20
for a, r being real number holds r > 0 implies a in ].a-r,a+r.[;
theorem :: TOPREAL6:21
for a, r being real number holds r >= 0 implies a in [.a-r,a+r.];
theorem :: TOPREAL6:22
for a, b being real number holds
a < b implies inf ].a,b.[ = a & sup ].a,b.[ = b;
canceled;
theorem :: TOPREAL6:24
for A being bounded Subset of REAL holds A c= [.inf A,sup A.];
begin :: Topological preliminaries
definition let T be TopStruct, A be finite Subset of T;
cluster T|A -> finite;
end;
definition
cluster finite non empty strict TopSpace;
end;
definition let T be TopStruct;
cluster empty -> connected Subset of T;
end;
definition let T be TopSpace;
cluster finite -> compact Subset of T;
end;
theorem :: TOPREAL6:25
for S, T being TopSpace st S, T are_homeomorphic & S is connected holds
T is connected;
theorem :: TOPREAL6:26
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;
begin
canceled 2;
theorem :: TOPREAL6:29
for A, B, C, D, a, b being set st A c= B & C c= D holds
product ((a,b) --> (A,C)) c= product ((a,b) --> (B,D));
theorem :: TOPREAL6:30
for A, B being Subset of REAL holds
product ((1,2) --> (A,B)) is Subset of TOP-REAL 2;
theorem :: TOPREAL6:31
|.|[0,a]|.| = abs(a) & |.|[a,0]|.| = abs(a);
theorem :: TOPREAL6:32
for p being Point of Euclid 2, q being Point of TOP-REAL 2 st
p = 0.REAL 2 & p = q holds q = <* 0,0 *> & q`1 = 0 & q`2 = 0;
theorem :: TOPREAL6:33
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.|;
theorem :: TOPREAL6:34
r*p = |[r*p`1,r*p`2]|;
theorem :: TOPREAL6:35
s = (1-r)*p + r*q & s <> p & 0 <= r implies 0 < r;
theorem :: TOPREAL6:36
s = (1-r)*p + r*q & s <> q & r <= 1 implies r < 1;
theorem :: TOPREAL6:37
s in LSeg(p,q) & s <> p & s <> q & p`1 < q`1 implies p`1 < s`1 & s`1 < q`1;
theorem :: TOPREAL6:38
s in LSeg(p,q) & s <> p & s <> q & p`2 < q`2 implies p`2 < s`2 & s`2 < q`2;
theorem :: TOPREAL6:39
for p being Point of TOP-REAL 2
ex q being Point of TOP-REAL 2 st q`1 < W-bound D & p <> q;
theorem :: TOPREAL6:40
for p being Point of TOP-REAL 2
ex q being Point of TOP-REAL 2 st q`1 > E-bound D & p <> q;
theorem :: TOPREAL6:41
for p being Point of TOP-REAL 2
ex q being Point of TOP-REAL 2 st q`2 > N-bound D & p <> q;
theorem :: TOPREAL6:42
for p being Point of TOP-REAL 2
ex q being Point of TOP-REAL 2 st q`2 < S-bound D & p <> q;
definition
cluster convex non empty -> connected Subset of TOP-REAL 2;
cluster non horizontal -> non empty Subset of TOP-REAL 2;
cluster non vertical -> non empty Subset of TOP-REAL 2;
cluster being_Region -> open connected Subset of TOP-REAL 2;
cluster open connected -> being_Region Subset of TOP-REAL 2;
end;
definition
cluster empty -> horizontal Subset of TOP-REAL 2;
cluster empty -> vertical Subset of TOP-REAL 2;
end;
definition
cluster non empty convex Subset of TOP-REAL 2;
end;
definition let a, b be Point of TOP-REAL 2;
cluster LSeg(a,b) -> convex connected;
end;
definition
cluster R^2-unit_square -> connected;
end;
definition
cluster being_simple_closed_curve -> connected compact Subset of TOP-REAL 2;
end;
theorem :: TOPREAL6:43 :: SPRECT_3:26
LSeg(NE-corner P,SE-corner P) c= L~SpStSeq P;
theorem :: TOPREAL6:44
LSeg(SW-corner P,SE-corner P) c= L~SpStSeq P;
theorem :: TOPREAL6:45
LSeg(SW-corner P,NW-corner P) c= L~SpStSeq P;
theorem :: TOPREAL6:46
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;
begin :: Balls as subsets of TOP-REAL n
theorem :: TOPREAL6:47
e = q & p in Ball(e,r) implies q`1-r < p`1 & p`1 < q`1+r;
theorem :: TOPREAL6:48
e = q & p in Ball(e,r) implies q`2-r < p`2 & p`2 < q`2+r;
theorem :: TOPREAL6:49
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);
theorem :: TOPREAL6:50
p = e implies Ball(e,r) c= product((1,2)-->(].p`1-r,p`1+r.[,].p`2-r,p`2+r.[));
theorem :: TOPREAL6:51
P = Ball(e,r) & p = e implies proj1.:P = ].p`1-r,p`1+r.[;
theorem :: TOPREAL6:52
P = Ball(e,r) & p = e implies proj2.:P = ].p`2-r,p`2+r.[;
theorem :: TOPREAL6:53
D = Ball(e,r) & p = e implies W-bound D = p`1 - r;
theorem :: TOPREAL6:54
D = Ball(e,r) & p = e implies E-bound D = p`1 + r;
theorem :: TOPREAL6:55
D = Ball(e,r) & p = e implies S-bound D = p`2 - r;
theorem :: TOPREAL6:56
D = Ball(e,r) & p = e implies N-bound D = p`2 + r;
theorem :: TOPREAL6:57
D = Ball(e,r) implies D is non horizontal;
theorem :: TOPREAL6:58
D = Ball(e,r) implies D is non vertical;
theorem :: TOPREAL6:59
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);
theorem :: TOPREAL6:60
for X being non empty compact Subset of TOP-REAL 2,
p being Point of Euclid 2 st p = 0.REAL 2 & a > 0 holds
X c= Ball(p, abs(E-bound X)+abs(N-bound X)+abs(W-bound X)+abs(S-bound X)+a);
theorem :: TOPREAL6:61
for M being Reflexive symmetric triangle (non empty MetrStruct),
z being Point of M holds
r < 0 implies Sphere(z,r) = {};
theorem :: TOPREAL6:62
for M being Reflexive discerning (non empty MetrStruct),
z being Point of M holds
Sphere(z,0) = {z};
theorem :: TOPREAL6:63
for M being Reflexive symmetric triangle (non empty MetrStruct),
z being Point of M holds
r < 0 implies cl_Ball(z,r) = {};
theorem :: TOPREAL6:64
cl_Ball(z,0) = {z};
theorem :: TOPREAL6:65
for A being Subset of TopSpaceMetr M st A = cl_Ball(z,r) holds
A is closed;
theorem :: TOPREAL6:66
A = cl_Ball(w,r) implies A is closed;
theorem :: TOPREAL6:67
cl_Ball(z,r) is bounded;
theorem :: TOPREAL6:68
for A being Subset of TopSpaceMetr M st A = Sphere(z,r) holds A is closed;
theorem :: TOPREAL6:69
A = Sphere(w,r) implies A is closed;
theorem :: TOPREAL6:70
Sphere(z,r) is bounded;
theorem :: TOPREAL6:71
A is Bounded implies Cl A is Bounded;
theorem :: TOPREAL6:72
for M being non empty MetrStruct holds
M is bounded iff
for X being Subset of M holds X is bounded;
theorem :: TOPREAL6:73
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;
theorem :: TOPREAL6:74
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;
canceled;
theorem :: TOPREAL6:76
A is Bounded & B is Bounded implies A \/ B is Bounded;
begin :: Topological properties of real numbers subsets
definition let X be non empty Subset of REAL;
cluster Cl X -> non empty;
end;
definition let D be bounded_below Subset of REAL;
cluster Cl D -> bounded_below;
end;
definition let D be bounded_above Subset of REAL;
cluster Cl D -> bounded_above;
end;
theorem :: TOPREAL6:77
for D being non empty bounded_below Subset of REAL holds inf D = inf Cl D;
theorem :: TOPREAL6:78
for D being non empty bounded_above Subset of REAL holds sup D = sup Cl D;
definition
cluster R^1 -> being_T2;
end;
theorem :: TOPREAL6:79
for A being Subset of REAL, B being Subset of R^1 st A = B holds
A is closed iff B is closed;
theorem :: TOPREAL6:80
for A being Subset of REAL, B being Subset of R^1 st A = B holds Cl A = Cl B
;
theorem :: TOPREAL6:81
for A being Subset of REAL, B being Subset of R^1 st A = B holds
A is compact iff B is compact;
definition
cluster finite -> compact Subset of REAL;
end;
definition let a, b be real number;
cluster [.a,b.] -> compact;
end;
theorem :: TOPREAL6:82
for a, b being real number holds a <> b iff Cl ].a,b.[ = [.a,b.];
definition
cluster non empty finite bounded Subset of REAL;
end;
theorem :: TOPREAL6:83
for T being TopStruct, f being RealMap of T, g being map of T, R^1 st f = g
holds
f is continuous iff g is continuous;
theorem :: TOPREAL6:84
for A, B being Subset of REAL,
f being map 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));
theorem :: TOPREAL6:85
for f being map of [:R^1,R^1:], TOP-REAL 2 st
for x, y being Real holds f. [x,y] = <*x,y*> holds
f is_homeomorphism;
theorem :: TOPREAL6:86
[:R^1,R^1:], TOP-REAL 2 are_homeomorphic;
begin :: Bounded subsets
theorem :: TOPREAL6:87
for A, B being compact Subset of REAL holds
product ((1,2) --> (A,B)) is compact Subset of TOP-REAL 2;
theorem :: TOPREAL6:88
P is Bounded closed implies P is compact;
theorem :: TOPREAL6:89
P is Bounded implies
for g being continuous RealMap of TOP-REAL 2 holds Cl(g.:P) c= g.:Cl P;
theorem :: TOPREAL6:90
proj1.:Cl P c= Cl(proj1.:P);
theorem :: TOPREAL6:91
proj2.:Cl P c= Cl(proj2.:P);
theorem :: TOPREAL6:92
P is Bounded implies Cl(proj1.:P) = proj1.:Cl P;
theorem :: TOPREAL6:93
P is Bounded implies Cl(proj2.:P) = proj2.:Cl P;
theorem :: TOPREAL6:94
D is Bounded implies W-bound D = W-bound Cl D;
theorem :: TOPREAL6:95
D is Bounded implies E-bound D = E-bound Cl D;
theorem :: TOPREAL6:96
D is Bounded implies N-bound D = N-bound Cl D;
theorem :: TOPREAL6:97
D is Bounded implies S-bound D = S-bound Cl D;
Back to top