Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Robert Milewski
- Received April 5, 2002
- MML identifier: JORDAN1J
- [
Mizar article,
MML identifier index
]
environ
vocabulary JORDAN8, PSCOMP_1, BOOLE, JORDAN1A, JORDAN9, GOBOARD1, GOBOARD5,
JORDAN6, SPRECT_2, JORDAN3, FINSEQ_5, JORDAN2C, SPPOL_2, GROUP_2,
RFINSEQ, REALSET1, JORDAN1E, SQUARE_1, FINSEQ_4, TOPREAL2, CONNSP_1,
COMPTS_1, TOPREAL1, SPPOL_1, FINSEQ_1, TREES_1, EUCLID, RELAT_1, MCART_1,
MATRIX_1, GOBOARD9, PRE_TOPC, RELAT_2, SEQM_3, SUBSET_1, FUNCT_1,
ARYTM_1, FINSEQ_6, CARD_1, GOBOARD2, GROUP_1, GRAPH_2;
notation TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1, SQUARE_1,
FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, RFINSEQ, MATRIX_1,
FINSEQ_6, REALSET1, GRAPH_2, STRUCT_0, PRE_TOPC, TOPREAL2, CARD_1,
CARD_4, BINARITH, CONNSP_1, COMPTS_1, EUCLID, PSCOMP_1, SPRECT_2,
GOBOARD1, TOPREAL1, GOBOARD2, GOBOARD5, GOBOARD9, GOBRD13, SPPOL_1,
SPPOL_2, JORDAN3, JORDAN8, JORDAN2C, JORDAN6, JORDAN9, JORDAN1A,
JORDAN1E;
constructors JORDAN8, REALSET1, GOBOARD9, JORDAN6, REAL_1, CARD_4, PSCOMP_1,
BINARITH, JORDAN2C, CONNSP_1, JORDAN9, JORDAN1A, SQUARE_1, FINSEQ_4,
GOBRD13, JORDAN1, JORDAN3, RFINSEQ, MATRIX_2, TOPREAL2, JORDAN5C,
PARTFUN1, GRAPH_2, SPRECT_1, GOBOARD2, INT_1, TOPS_1, FINSOP_1, JORDAN1E,
MEMBERED;
clusters SPRECT_1, TOPREAL6, JORDAN8, REVROT_1, INT_1, RELSET_1, SUBSET_1,
PRE_TOPC, SPRECT_3, GOBOARD2, FINSEQ_1, FINSEQ_5, SPPOL_2, JORDAN1A,
JORDAN1B, JORDAN1E, JORDAN1G, GOBRD11, FUNCT_7, XBOOLE_0, XREAL_0,
MEMBERED, ZFMISC_1, NUMBERS, ORDINAL2;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
begin
reserve n for Nat;
theorem :: JORDAN1J:1
for G be Go-board
for i1,i2,j1,j2 be Nat st
1 <= j1 & j1 <= width G & 1 <= j2 & j2 <= width G &
1 <= i1 & i1 < i2 & i2 <= len G holds
G*(i1,j1)`1 < G*(i2,j2)`1;
theorem :: JORDAN1J:2
for G be Go-board
for i1,i2,j1,j2 be Nat st
1 <= i1 & i1 <= len G & 1 <= i2 & i2 <= len G &
1 <= j1 & j1 < j2 & j2 <= width G holds
G*(i1,j1)`2 < G*(i2,j2)`2;
definition
let f be non empty FinSequence;
let g be FinSequence;
cluster f^'g -> non empty;
end;
theorem :: JORDAN1J:3
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for n be Nat holds
L~(Cage(C,n)-:E-max L~Cage(C,n)) /\ L~(Cage(C,n):-E-max L~Cage(C,n)) =
{N-min L~Cage(C,n),E-max L~Cage(C,n)};
theorem :: JORDAN1J:4
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
Upper_Seq(C,n) = Rotate(Cage(C,n),E-max L~Cage(C,n)):-W-min L~Cage(C,n);
theorem :: JORDAN1J:5
for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
W-min L~Cage(C,n) in rng Upper_Seq(C,n) &
W-min L~Cage(C,n) in L~Upper_Seq(C,n);
theorem :: JORDAN1J:6
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
W-max L~Cage(C,n) in rng Upper_Seq(C,n) &
W-max L~Cage(C,n) in L~Upper_Seq(C,n);
theorem :: JORDAN1J:7
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
N-min L~Cage(C,n) in rng Upper_Seq(C,n) &
N-min L~Cage(C,n) in L~Upper_Seq(C,n);
theorem :: JORDAN1J:8
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
N-max L~Cage(C,n) in rng Upper_Seq(C,n) &
N-max L~Cage(C,n) in L~Upper_Seq(C,n);
theorem :: JORDAN1J:9
for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
E-max L~Cage(C,n) in rng Upper_Seq(C,n) &
E-max L~Cage(C,n) in L~Upper_Seq(C,n);
theorem :: JORDAN1J:10
for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
E-max L~Cage(C,n) in rng Lower_Seq(C,n) &
E-max L~Cage(C,n) in L~Lower_Seq(C,n);
theorem :: JORDAN1J:11
for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
E-min L~Cage(C,n) in rng Lower_Seq(C,n) &
E-min L~Cage(C,n) in L~Lower_Seq(C,n);
theorem :: JORDAN1J:12
for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
S-max L~Cage(C,n) in rng Lower_Seq(C,n) &
S-max L~Cage(C,n) in L~Lower_Seq(C,n);
theorem :: JORDAN1J:13
for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
S-min L~Cage(C,n) in rng Lower_Seq(C,n) &
S-min L~Cage(C,n) in L~Lower_Seq(C,n);
theorem :: JORDAN1J:14
for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
W-min L~Cage(C,n) in rng Lower_Seq(C,n) &
W-min L~Cage(C,n) in L~Lower_Seq(C,n);
theorem :: JORDAN1J:15
for X,Y be non empty compact Subset of TOP-REAL 2 st
X c= Y & N-min Y in X holds
N-min X = N-min Y;
theorem :: JORDAN1J:16
for X,Y be non empty compact Subset of TOP-REAL 2 st
X c= Y & N-max Y in X holds
N-max X = N-max Y;
theorem :: JORDAN1J:17
for X,Y be non empty compact Subset of TOP-REAL 2 st
X c= Y & E-min Y in X holds
E-min X = E-min Y;
theorem :: JORDAN1J:18
for X,Y be non empty compact Subset of TOP-REAL 2 st
X c= Y & E-max Y in X holds
E-max X = E-max Y;
theorem :: JORDAN1J:19
for X,Y be non empty compact Subset of TOP-REAL 2 st
X c= Y & S-min Y in X holds
S-min X = S-min Y;
theorem :: JORDAN1J:20
for X,Y be non empty compact Subset of TOP-REAL 2 st
X c= Y & S-max Y in X holds
S-max X = S-max Y;
theorem :: JORDAN1J:21
for X,Y be non empty compact Subset of TOP-REAL 2 st
X c= Y & W-min Y in X holds
W-min X = W-min Y;
theorem :: JORDAN1J:22
for X,Y be non empty compact Subset of TOP-REAL 2 st
X c= Y & W-max Y in X holds
W-max X = W-max Y;
theorem :: JORDAN1J:23
for X,Y be non empty compact Subset of TOP-REAL 2 st
N-bound X < N-bound Y holds
N-bound (X\/Y) = N-bound Y;
theorem :: JORDAN1J:24
for X,Y be non empty compact Subset of TOP-REAL 2 st
E-bound X < E-bound Y holds
E-bound (X\/Y) = E-bound Y;
theorem :: JORDAN1J:25
for X,Y be non empty compact Subset of TOP-REAL 2 st
S-bound X < S-bound Y holds
S-bound (X\/Y) = S-bound X;
theorem :: JORDAN1J:26
for X,Y be non empty compact Subset of TOP-REAL 2 st
W-bound X < W-bound Y holds
W-bound (X\/Y) = W-bound X;
theorem :: JORDAN1J:27
for X,Y be non empty compact Subset of TOP-REAL 2 st
N-bound X < N-bound Y holds
N-min (X\/Y) = N-min Y;
theorem :: JORDAN1J:28
for X,Y be non empty compact Subset of TOP-REAL 2 st
N-bound X < N-bound Y holds
N-max (X\/Y) = N-max Y;
theorem :: JORDAN1J:29
for X,Y be non empty compact Subset of TOP-REAL 2 st
E-bound X < E-bound Y holds
E-min (X\/Y) = E-min Y;
theorem :: JORDAN1J:30
for X,Y be non empty compact Subset of TOP-REAL 2 st
E-bound X < E-bound Y holds
E-max (X\/Y) = E-max Y;
theorem :: JORDAN1J:31
for X,Y be non empty compact Subset of TOP-REAL 2 st
S-bound X < S-bound Y holds
S-min (X\/Y) = S-min X;
theorem :: JORDAN1J:32
for X,Y be non empty compact Subset of TOP-REAL 2 st
S-bound X < S-bound Y holds
S-max (X\/Y) = S-max X;
theorem :: JORDAN1J:33
for X,Y be non empty compact Subset of TOP-REAL 2 st
W-bound X < W-bound Y holds
W-min (X\/Y) = W-min X;
theorem :: JORDAN1J:34
for X,Y be non empty compact Subset of TOP-REAL 2 st
W-bound X < W-bound Y holds
W-max (X\/Y) = W-max X;
theorem :: JORDAN1J:35
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 :: JORDAN1J:36
for f be non constant standard special_circular_sequence
for p,q be Point of TOP-REAL 2
for g be connected Subset of TOP-REAL 2 st
p in RightComp f & q in LeftComp f & p in g & q in g holds
g meets L~f;
definition
cluster non constant standard s.c.c.
(being_S-Seq FinSequence of TOP-REAL 2);
end;
theorem :: JORDAN1J:37
for f be S-Sequence_in_R2
for p be Point of TOP-REAL 2 st p in rng f holds
L_Cut(f,p) = mid(f,p..f,len f);
theorem :: JORDAN1J:38
for M be Go-board
for f be S-Sequence_in_R2 st f is_sequence_on M
for p be Point of TOP-REAL 2 st p in rng f holds
R_Cut(f,p) is_sequence_on M;
theorem :: JORDAN1J:39
for M be Go-board
for f be S-Sequence_in_R2 st f is_sequence_on M
for p be Point of TOP-REAL 2 st p in rng f holds
L_Cut(f,p) is_sequence_on M;
theorem :: JORDAN1J:40
for G be Go-board
for f be FinSequence of TOP-REAL 2 st f is_sequence_on G
for i,j be Nat st 1 <= i & i <= len G & 1 <= j & j <= width G holds
G*(i,j) in L~f implies G*(i,j) in rng f;
theorem :: JORDAN1J:41
for f be S-Sequence_in_R2
for g be FinSequence of TOP-REAL 2 holds
g is unfolded s.n.c. one-to-one & L~f /\ L~g = {f/.1} & f/.1 = g/.len g &
(for i be Nat st 1<=i & i+2 <= len f holds
LSeg(f,i) /\ LSeg(f/.len f,g/.1) = {}) &
(for i be Nat st 2<=i & i+1 <= len g holds
LSeg(g,i) /\ LSeg(f/.len f,g/.1) = {}) implies f^g is s.c.c.;
theorem :: JORDAN1J:42
for C be compact non vertical non horizontal non empty Subset of TOP-REAL
2
ex i be Nat st 1 <= i & i+1 <= len Gauge(C,n) &
W-min C in cell(Gauge(C,n),1,i) & W-min C <> Gauge(C,n)*(2,i);
theorem :: JORDAN1J:43
for f be S-Sequence_in_R2
for p be Point of TOP-REAL 2 st p in L~f & f.len f in L~R_Cut(f,p) holds
f.len f = p;
theorem :: JORDAN1J:44
for f be non empty FinSequence of TOP-REAL 2
for p be Point of TOP-REAL 2 holds
R_Cut (f,p) <> {};
theorem :: JORDAN1J:45
for f be S-Sequence_in_R2
for p be Point of TOP-REAL 2 st p in L~f holds
R_Cut(f,p)/.(len R_Cut(f,p)) = p;
theorem :: JORDAN1J:46
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for p be Point of TOP-REAL 2 holds
p in L~Upper_Seq(C,n) & p`1 = E-bound L~Cage(C,n) implies
p = E-max L~Cage(C,n);
theorem :: JORDAN1J:47
for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
for p be Point of TOP-REAL 2 holds
p in L~Lower_Seq(C,n) & p`1 = W-bound L~Cage(C,n) implies
p = W-min L~Cage(C,n);
theorem :: JORDAN1J:48
for G be Go-board
for f,g be FinSequence of TOP-REAL 2
for k be Nat holds
1 <= k & k < len f & f^g is_sequence_on G implies
left_cell(f^g,k,G) = left_cell(f,k,G) &
right_cell(f^g,k,G) = right_cell(f,k,G);
theorem :: JORDAN1J:49
for D be set
for f,g be FinSequence of D
for i be Nat st i <= len f holds
(f^'g)|i = f|i;
theorem :: JORDAN1J:50
for D be set
for f,g be FinSequence of D holds
(f^'g)|(len f) = f;
theorem :: JORDAN1J:51
for G be Go-board
for f,g be FinSequence of TOP-REAL 2
for k be Nat holds
1 <= k & k < len f & f^'g is_sequence_on G implies
left_cell(f^'g,k,G) = left_cell(f,k,G) &
right_cell(f^'g,k,G) = right_cell(f,k,G);
theorem :: JORDAN1J:52
for G be Go-board
for f be S-Sequence_in_R2
for p be Point of TOP-REAL 2
for k be Nat st 1 <= k & k < p..f & f is_sequence_on G & p in rng f holds
left_cell(R_Cut(f,p),k,G) = left_cell(f,k,G) &
right_cell(R_Cut(f,p),k,G) = right_cell(f,k,G);
theorem :: JORDAN1J:53
for G be Go-board
for f be FinSequence of TOP-REAL 2
for p be Point of TOP-REAL 2
for k be Nat st 1 <= k & k < p..f & f is_sequence_on G holds
left_cell(f-:p,k,G) = left_cell(f,k,G) &
right_cell(f-:p,k,G) = right_cell(f,k,G);
theorem :: JORDAN1J:54
for f,g be FinSequence of TOP-REAL 2 st
f is unfolded s.n.c. one-to-one & g is unfolded s.n.c. one-to-one &
f/.len f = g/.1 & L~f /\ L~g = {g/.1} holds
f^'g is s.n.c.;
theorem :: JORDAN1J:55
for f,g be FinSequence of TOP-REAL 2 st
f is one-to-one & g is one-to-one & rng f /\ rng g c= {g/.1} holds
f^'g is one-to-one;
theorem :: JORDAN1J:56
for f be FinSequence of TOP-REAL 2
for p be Point of TOP-REAL 2 st f is_S-Seq & p in rng f & p <> f.1 holds
Index(p,f)+1 = p..f;
theorem :: JORDAN1J:57
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= j & k <= width Gauge(C,n) &
Gauge(C,n)*(i,k) in L~Upper_Seq(C,n) &
Gauge(C,n)*(i,j) in L~Lower_Seq(C,n) holds j <> k;
theorem :: JORDAN1J:58
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i,k)} &
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i,j)} holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C;
theorem :: JORDAN1J:59
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i,k)} &
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i,j)} holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C;
theorem :: JORDAN1J:60
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) & n > 0 &
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Upper_Arc L~Cage(C,n) =
{Gauge(C,n)*(i,k)} &
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Lower_Arc L~Cage(C,n) =
{Gauge(C,n)*(i,j)} holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C;
theorem :: JORDAN1J:61
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) & n > 0 &
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Upper_Arc L~Cage(C,n) =
{Gauge(C,n)*(i,k)} &
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Lower_Arc L~Cage(C,n) =
{Gauge(C,n)*(i,j)} holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C;
theorem :: JORDAN1J:62
for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
for j be Nat holds
Gauge(C,n+1)*(Center Gauge(C,n+1),j) in Upper_Arc L~Cage(C,n+1) &
1 <= j & j <= width Gauge(C,n+1) implies
LSeg(Gauge(C,1)*(Center Gauge(C,1),1),Gauge(C,n+1)*(Center Gauge(C,n+1),j))
meets Lower_Arc L~Cage(C,n+1);
theorem :: JORDAN1J:63
for C be Simple_closed_curve
for j,k be Nat holds
1 <= j & j <= k & k <= width Gauge(C,n+1) &
LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j),
Gauge(C,n+1)*(Center Gauge(C,n+1),k)) /\ Upper_Arc L~Cage(C,n+1) =
{Gauge(C,n+1)*(Center Gauge(C,n+1),k)} &
LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j),
Gauge(C,n+1)*(Center Gauge(C,n+1),k)) /\ Lower_Arc L~Cage(C,n+1) =
{Gauge(C,n+1)*(Center Gauge(C,n+1),j)} implies
LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j),
Gauge(C,n+1)*(Center Gauge(C,n+1),k)) meets Lower_Arc C;
theorem :: JORDAN1J:64
for C be Simple_closed_curve
for j,k be Nat holds
1 <= j & j <= k & k <= width Gauge(C,n+1) &
LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j),
Gauge(C,n+1)*(Center Gauge(C,n+1),k)) /\ Upper_Arc L~Cage(C,n+1) =
{Gauge(C,n+1)*(Center Gauge(C,n+1),k)} &
LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j),
Gauge(C,n+1)*(Center Gauge(C,n+1),k)) /\ Lower_Arc L~Cage(C,n+1) =
{Gauge(C,n+1)*(Center Gauge(C,n+1),j)} implies
LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j),
Gauge(C,n+1)*(Center Gauge(C,n+1),k)) meets Upper_Arc C;
Back to top