Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Robert Milewski,
- Andrzej Trybulec,
- Artur Kornilowicz,
and
- Adam Naumowicz
- Received October 6, 2000
- MML identifier: JORDAN1B
- [
Mizar article,
MML identifier index
]
environ
vocabulary COMPTS_1, SPPOL_1, EUCLID, RELAT_2, GOBOARD1, PRE_TOPC, TOPREAL2,
RELAT_1, TOPREAL1, TOPS_2, SUBSET_1, BOOLE, MCART_1, CONNSP_3, CONNSP_1,
SETFAM_1, TARSKI, FINSEQ_1, JORDAN3, ARYTM_1, FINSEQ_5, FUNCT_1, GROUP_2,
PSCOMP_1, ORDINAL2, FUNCT_5, REALSET1, FINSEQ_4, SPRECT_2, FINSEQ_6,
JORDAN1A, NAT_1, INT_1, JORDAN8, GROUP_1, ARYTM_3, GOBOARD5, TREES_1,
JORDAN2C, JORDAN9, JORDAN6, COMPLEX1, SQUARE_1, ABSVALUE, ARYTM;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, REAL_1,
INT_1, NAT_1, ABSVALUE, SQUARE_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSEQ_4,
FINSEQ_5, MATRIX_1, REALSET1, FINSEQ_6, STRUCT_0, PRE_TOPC, TOPS_2,
JGRAPH_1, TOPREAL2, CARD_4, BINARITH, CONNSP_1, CONNSP_3, COMPTS_1,
EUCLID, PSCOMP_1, SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD5, SPPOL_1,
JORDAN3, JORDAN8, JORDAN2C, JORDAN6, JORDAN9, JORDAN1A;
constructors JORDAN8, REALSET1, JORDAN6, REAL_1, CARD_4, PSCOMP_1, BINARITH,
JORDAN2C, CONNSP_1, JORDAN9, JORDAN1A, WSIERP_1, SQUARE_1, ABSVALUE,
FINSEQ_4, JORDAN1, JORDAN3, RFINSEQ, TOPS_2, TOPREAL2, JORDAN5C,
CONNSP_3, TOPREAL4, SPRECT_1, FINSEQ_5, GOBOARD1, TOPRNS_1, INT_1;
clusters XREAL_0, TOPREAL6, JORDAN8, INT_1, RELSET_1, STRUCT_0, EUCLID,
SPRECT_3, FINSEQ_1, FINSEQ_5, JORDAN1A, PRE_TOPC, JORDAN3, MEMBERED;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
begin
reserve
E for compact non vertical non horizontal Subset of TOP-REAL 2,
C for compact connected non vertical non horizontal Subset of TOP-REAL 2,
G for Go-board,
i, j, m, n for Nat,
p for Point of TOP-REAL 2;
definition
cluster -> non vertical non horizontal Simple_closed_curve;
end;
definition
let T be non empty TopSpace;
cluster non empty a_union_of_components of T;
end;
theorem :: JORDAN1B:1
for T being non empty TopSpace
for A being non empty a_union_of_components of T st A is connected holds
A is_a_component_of T;
theorem :: JORDAN1B:2
for f being FinSequence holds
f is empty iff Rev f is empty;
theorem :: JORDAN1B:3
for D being non empty set, f being FinSequence of D
for i,j st 1 <= i & i <= len f & 1 <= j & j <= len f
holds mid(f,i,j) is non empty;
theorem :: JORDAN1B:4
for f be non empty FinSequence of TOP-REAL 2
for p be Point of TOP-REAL 2 st 1 <= len f & p in L~f holds
R_Cut(f,p).1 = f.1;
theorem :: JORDAN1B:5
for f be non empty FinSequence of TOP-REAL 2
for p be Point of TOP-REAL 2 st f is_S-Seq & p in L~f holds
L_Cut(f,p).(len L_Cut(f,p)) = f.(len f);
theorem :: JORDAN1B:6
for P be Simple_closed_curve holds W-max(P) <> E-max(P);
theorem :: JORDAN1B:7
for D be non empty set
for f be FinSequence of D st 1 <= i & i < len f holds
mid(f,i,len f-'1)^<*f/.(len f)*> = mid(f,i,len f);
theorem :: JORDAN1B:8
for p,q be Point of TOP-REAL 2 st p <> q & LSeg(p,q) is vertical holds
<*p,q*> is_S-Seq;
theorem :: JORDAN1B:9
for p,q be Point of TOP-REAL 2 st p <> q & LSeg(p,q) is horizontal holds
<*p,q*> is_S-Seq;
theorem :: JORDAN1B:10
for p,q be FinSequence of TOP-REAL 2
for v be Point of TOP-REAL 2 st p is_in_the_area_of q holds
Rotate(p,v) is_in_the_area_of q;
theorem :: JORDAN1B:11
for p be non trivial FinSequence of TOP-REAL 2
for v be Point of TOP-REAL 2 holds
Rotate(p,v) is_in_the_area_of p;
theorem :: JORDAN1B:12
for f be FinSequence holds
Center f >= 1;
theorem :: JORDAN1B:13
for f be FinSequence st len f >= 1 holds
Center f <= len f;
theorem :: JORDAN1B:14
Center G <= len G;
theorem :: JORDAN1B:15
for f be FinSequence st len f >= 2 holds
Center f > 1;
theorem :: JORDAN1B:16
for f be FinSequence st len f >= 3 holds
Center f < len f;
theorem :: JORDAN1B:17
Center Gauge(E,n) = 2|^(n-'1) + 2;
theorem :: JORDAN1B:18
E c= cell(Gauge(E,0),2,2);
theorem :: JORDAN1B:19
not cell(Gauge(E,0),2,2) c= BDD E;
theorem :: JORDAN1B:20
Gauge(C,1)*(Center Gauge(C,1),1)
= |[(W-bound C + E-bound C)/2,S-bound L~Cage(C,1)]|;
theorem :: JORDAN1B:21
Gauge(C,1)*(Center Gauge(C,1),len Gauge(C,1))
= |[(W-bound C + E-bound C)/2,N-bound L~Cage(C,1)]|;
theorem :: JORDAN1B:22
1 <= j & j < width G &
1 <= m & m <= len G & 1 <= n & n <= width G &
p in cell(G,len G,j) & p`1 = G*(m,n)`1
implies len G = m;
theorem :: JORDAN1B:23
1 <= i & i <= len G & 1 <= j & j < width G &
1 <= m & m <= len G & 1 <= n & n <= width G &
p in cell(G,i,j) & p`1 = G*(m,n)`1
implies i = m or i = m -' 1;
theorem :: JORDAN1B:24
1 <= i & i < len G &
1 <= m & m <= len G & 1 <= n & n <= width G &
p in cell(G,i,width G) & p`2 = G*(m,n)`2
implies width G = n;
theorem :: JORDAN1B:25
1 <= i & i < len G & 1 <= j & j <= width G &
1 <= m & m <= len G & 1 <= n & n <= width G &
p in cell(G,i,j) & p`2 = G*(m,n)`2
implies j = n or j = n -' 1;
theorem :: JORDAN1B:26
for C be Simple_closed_curve
for r be real number st W-bound C <= r & r <= E-bound C holds
LSeg(|[r,S-bound C]|,|[r,N-bound C]|) meets Upper_Arc C;
theorem :: JORDAN1B:27
for C be Simple_closed_curve
for r be real number st W-bound C <= r & r <= E-bound C holds
LSeg(|[r,S-bound C]|,|[r,N-bound C]|) meets Lower_Arc C;
theorem :: JORDAN1B:28
for C be Simple_closed_curve
for i be Nat st 1 < i & i < len Gauge(C,n) holds
LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n)))
meets Upper_Arc C;
theorem :: JORDAN1B:29
for C be Simple_closed_curve
for i be Nat st 1 < i & i < len Gauge(C,n) holds
LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n)))
meets Lower_Arc C;
theorem :: JORDAN1B:30
for C be Simple_closed_curve holds
LSeg(Gauge(C,n)*(Center Gauge(C,n),1),
Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n)))
meets Upper_Arc C;
theorem :: JORDAN1B:31
for C be Simple_closed_curve holds
LSeg(Gauge(C,n)*(Center Gauge(C,n),1),
Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n)))
meets Lower_Arc C;
theorem :: JORDAN1B:32
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for i be Nat st 1 <= i & i <= len Gauge(C,n) holds
LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n)))
meets Upper_Arc L~Cage(C,n);
theorem :: JORDAN1B:33
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for i be Nat st 1 <= i & i <= len Gauge(C,n) holds
LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n)))
meets Lower_Arc L~Cage(C,n);
theorem :: JORDAN1B:34
for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
holds
LSeg(Gauge(C,n)*(Center Gauge(C,n),1),
Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n)))
meets Upper_Arc L~Cage(C,n);
theorem :: JORDAN1B:35
for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
holds
LSeg(Gauge(C,n)*(Center Gauge(C,n),1),
Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n)))
meets Lower_Arc L~Cage(C,n);
theorem :: JORDAN1B:36
j <= width G implies cell(G,0,j) is not Bounded;
theorem :: JORDAN1B:37
i <= width G implies cell(G,len G,i) is not Bounded;
theorem :: JORDAN1B:38
j <= width Gauge(C,n) implies cell(Gauge(C,n),0,j) c= UBD C;
theorem :: JORDAN1B:39
j <= len Gauge(E,n) implies cell(Gauge(E,n),len Gauge(E,n),j) c= UBD E;
theorem :: JORDAN1B:40
i <= len Gauge(C,n) & j <= width Gauge(C,n) &
cell(Gauge(C,n),i,j) c= BDD C
implies j > 1;
theorem :: JORDAN1B:41
i <= len Gauge(C,n) & j <= width Gauge(C,n) &
cell(Gauge(C,n),i,j) c= BDD C
implies i > 1;
theorem :: JORDAN1B:42
i <= len Gauge(C,n) & j <= width Gauge(C,n) &
cell(Gauge(C,n),i,j) c= BDD C
implies j+1 < width Gauge(C,n);
theorem :: JORDAN1B:43
i <= len Gauge(C,n) & j <= width Gauge(C,n) &
cell(Gauge(C,n),i,j) c= BDD C
implies i+1 < len Gauge(C,n);
theorem :: JORDAN1B:44
(ex i,j st i <= len Gauge(C,n) & j <= width Gauge(C,n) &
cell(Gauge(C,n),i,j) c= BDD C)
implies n >= 1;
Back to top