Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Czeslaw Bylinski,
and
- Mariusz Zynel
- Received June 22, 1999
- MML identifier: JORDAN9
- [
Mizar article,
MML identifier index
]
environ
vocabulary FINSEQ_1, BOOLE, PRE_TOPC, RELAT_2, CONNSP_1, RELAT_1, FINSEQ_5,
ARYTM_1, GOBOARD1, EUCLID, MATRIX_1, ABSVALUE, GOBRD13, FUNCT_1,
TOPREAL1, RFINSEQ, GOBOARD5, TOPS_1, TREES_1, SPPOL_1, MCART_1, TARSKI,
SUBSET_1, SEQM_3, GOBOARD9, COMPTS_1, JORDAN8, PSCOMP_1, GROUP_1,
ARYTM_3, SPRECT_2, CARD_1, PCOMPS_1, METRIC_1, JORDAN9, FINSEQ_4, ARYTM;
notation TARSKI, XBOOLE_0, SUBSET_1, GOBOARD5, STRUCT_0, ORDINAL1, NUMBERS,
XREAL_0, REAL_1, NAT_1, BINARITH, ABSVALUE, RELAT_1, FUNCT_1, FUNCT_2,
CARD_1, CARD_4, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSEQ_5, RFINSEQ,
MATRIX_1, METRIC_1, PRE_TOPC, TOPS_1, COMPTS_1, CONNSP_1, PCOMPS_1,
EUCLID, TOPREAL1, GOBOARD1, SPPOL_1, PSCOMP_1, SPRECT_2, GOBOARD9,
JORDAN8, GOBRD13;
constructors REAL_1, FINSEQ_4, CARD_4, RFINSEQ, BINARITH, TOPS_1, CONNSP_1,
COMPTS_1, SPPOL_1, PSCOMP_1, REALSET1, SPRECT_2, GOBOARD9, JORDAN8,
GOBRD13, GROUP_1, MEMBERED;
clusters PSCOMP_1, RELSET_1, FINSEQ_1, SPPOL_2, REVROT_1, SPRECT_1, SPRECT_2,
XREAL_0, GOBOARD9, JORDAN8, GOBRD13, EUCLID, TOPREAL1, NAT_1, MEMBERED,
ZFMISC_1, NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Generalities
reserve i,j,k,n for Nat,
D for non empty set,
f, g for FinSequence of D;
canceled 2;
theorem :: JORDAN9:3
for T being non empty TopSpace
for B,C1,C2,D being Subset of T st B is connected & C1 is_a_component_of D &
C2 is_a_component_of D & B meets C1 & B meets C2 & B c= D
holds C1 = C2;
theorem :: JORDAN9:4
(for n holds f|n = g|n) implies f = g;
theorem :: JORDAN9:5
n in dom f implies
ex k st k in dom Rev f & n+k = len f+1 & f/.n = (Rev f)/.k;
theorem :: JORDAN9:6
n in dom Rev f implies
ex k st k in dom f & n+k = len f+1 & (Rev f)/.n = f/.k;
begin :: Go-board preliminaries
reserve G for Go-board,
f, g for FinSequence of TOP-REAL 2,
p for Point of TOP-REAL 2,
r, s for Real,
x for set;
theorem :: JORDAN9:7
for D being non empty set
for G being Matrix of D
for f being FinSequence of D holds
f is_sequence_on G iff Rev f is_sequence_on G;
theorem :: JORDAN9:8
for G being Matrix of TOP-REAL 2
for f being FinSequence of TOP-REAL 2 holds
f is_sequence_on G & 1 <= k & k <= len f implies f/.k in Values G;
theorem :: JORDAN9:9
n <= len f & x in L~(f/^n)
implies
ex i being Nat st n+1 <= i & i+1 <= len f & x in LSeg(f,i);
theorem :: JORDAN9:10
f is_sequence_on G & 1 <= k & k+1 <= len f
implies
f/.k in left_cell(f,k,G) & f/.k in right_cell(f,k,G);
theorem :: JORDAN9:11
f is_sequence_on G & 1 <= k & k+1 <= len f
implies
Int left_cell(f,k,G) <> {} & Int right_cell(f,k,G) <> {};
theorem :: JORDAN9:12
f is_sequence_on G & 1 <= k & k+1 <= len f
implies
Int left_cell(f,k,G) is connected & Int right_cell(f,k,G) is connected;
theorem :: JORDAN9:13
f is_sequence_on G & 1 <= k & k+1 <= len f
implies
Cl Int left_cell(f,k,G) = left_cell(f,k,G) &
Cl Int right_cell(f,k,G) = right_cell(f,k,G);
theorem :: JORDAN9:14
f is_sequence_on G & LSeg(f,k) is horizontal
implies
ex j st 1 <= j & j <= width G & for p st p in
LSeg(f,k) holds p`2 = G*(1,j)`2;
theorem :: JORDAN9:15
f is_sequence_on G & LSeg(f,k) is vertical
implies
ex i st 1 <= i & i <= len G & for p st p in LSeg(f,k) holds p`1 = G*(i,1)`1;
theorem :: JORDAN9:16
f is_sequence_on G & f is special & i <= len G & j <= width G
implies
Int cell(G,i,j) misses L~f;
theorem :: JORDAN9:17
f is_sequence_on G & f is special & 1 <= k & k+1 <= len f
implies
Int left_cell(f,k,G) misses L~f & Int right_cell(f,k,G) misses L~f;
theorem :: JORDAN9:18
1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G
implies
G*(i,j)`1 = G*(i,j+1)`1 & G*(i,j)`2 = G*(i+1,j)`2 &
G*(i+1,j+1)`1 = G*(i+1,j)`1 & G*(i+1,j+1)`2 = G*(i,j+1)`2;
theorem :: JORDAN9:19
for i,j being Nat st 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G
holds
p in cell(G,i,j) iff
G*(i,j)`1 <= p`1 & p`1 <= G*(i+1,j)`1 & G*(i,j)`2 <= p`2 & p`2 <=
G*(i,j+1)`2;
theorem :: JORDAN9:20
1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G
implies
cell(G,i,j) = { |[r,s]| : G*(i,j)`1 <= r & r <= G*(i+1,j)`1 &
G*(i,j)`2 <= s & s <= G*(i,j+1)`2 };
theorem :: JORDAN9:21
1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G &
p in Values G & p in cell(G,i,j)
implies
p = G*(i,j) or p = G*(i,j+1) or p = G*(i+1,j+1) or p = G*(i+1,j);
theorem :: JORDAN9:22
1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G
implies
G*(i,j) in cell(G,i,j) & G*(i,j+1) in cell(G,i,j) &
G*(i+1,j+1) in cell(G,i,j) & G*(i+1,j) in cell(G,i,j);
theorem :: JORDAN9:23
1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G &
p in Values G & p in cell(G,i,j)
implies
p is_extremal_in cell(G,i,j);
theorem :: JORDAN9:24
2 <= len G & 2 <= width G & f is_sequence_on G & 1 <= k & k+1 <= len f
implies
ex i,j st 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G &
LSeg(f,k) c= cell(G,i,j);
theorem :: JORDAN9:25
2 <= len G & 2 <= width G & f is_sequence_on G & 1 <= k & k+1 <= len f &
p in Values G & p in LSeg(f,k)
implies
p = f/.k or p = f/.(k+1);
theorem :: JORDAN9:26
[i,j] in Indices G & 1 <= k & k <= width G implies G*(i,j)`1 <= G*
(len G,k)`1;
theorem :: JORDAN9:27
[i,j] in Indices G & 1 <= k & k <= len G implies G*(i,j)`2 <= G*
(k,width G)`2;
theorem :: JORDAN9:28
f is_sequence_on G & f is special & L~g c= L~f & 1 <= k & k+1 <= len f
implies
for A being Subset of TOP-REAL 2 st
A = right_cell(f,k,G)\L~g or A = left_cell(f,k,G)\L~g holds A is connected;
theorem :: JORDAN9:29
for f being non constant standard special_circular_sequence st
f is_sequence_on G
for k st 1 <= k & k+1 <= len f
holds
right_cell(f,k,G)\L~f c= RightComp f & left_cell(f,k,G)\L~f c= LeftComp f;
begin :: Cages
reserve
C for compact non vertical non horizontal non empty Subset of TOP-REAL 2,
l, m, i1, i2, j1, j2 for Nat;
theorem :: JORDAN9:30
ex i st 1 <= i & i+1 <= len Gauge(C,n) &
N-min C in cell(Gauge(C,n),i,width Gauge(C,n)-'1) &
N-min C <> Gauge(C,n)*(i,width Gauge(C,n)-'1);
theorem :: JORDAN9:31
1 <= i1 & i1+1 <= len Gauge(C,n) &
N-min C in cell(Gauge(C,n),i1,width Gauge(C,n)-'1) &
N-min C <> Gauge(C,n)*(i1,width Gauge(C,n)-'1) &
1 <= i2 & i2+1 <= len Gauge(C,n) &
N-min C in cell(Gauge(C,n),i2,width Gauge(C,n)-'1) &
N-min C <> Gauge(C,n)*(i2,width Gauge(C,n)-'1)
implies
i1 = i2;
theorem :: JORDAN9:32
for f being standard non constant special_circular_sequence
st f is_sequence_on Gauge(C,n) &
(for k st 1 <= k & k+1 <= len f
holds
left_cell(f,k,Gauge(C,n)) misses C &
right_cell(f,k,Gauge(C,n)) meets C) &
(ex i st 1 <= i & i+1 <= len Gauge(C,n) &
f/.1 = Gauge(C,n)*(i,width Gauge(C,n)) &
f/.2 = Gauge(C,n)*(i+1,width Gauge(C,n)) &
N-min C in cell(Gauge(C,n),i,width Gauge(C,n)-'1) &
N-min C <> Gauge(C,n)*(i,width Gauge(C,n)-'1))
holds
N-min L~f = f/.1;
definition
let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2;
let n be Nat;
assume
C is connected;
func Cage(C,n) -> clockwise_oriented
(standard non constant special_circular_sequence) means
:: JORDAN9:def 1
it is_sequence_on Gauge(C,n) &
(ex i st 1 <= i & i+1 <= len Gauge(C,n) &
it/.1 = Gauge(C,n)*(i,width Gauge(C,n)) &
it/.2 = Gauge(C,n)*(i+1,width Gauge(C,n)) &
N-min C in cell(Gauge(C,n),i,width Gauge(C,n)-'1) &
N-min C <> Gauge(C,n)*(i,width Gauge(C,n)-'1)) &
for k st 1 <= k & k+2 <= len it holds
(front_left_cell(it,k,Gauge(C,n)) misses C &
front_right_cell(it,k,Gauge(C,n)) misses C
implies
it turns_right k,Gauge(C,n)) &
(front_left_cell(it,k,Gauge(C,n)) misses C &
front_right_cell(it,k,Gauge(C,n)) meets C
implies
it goes_straight k,Gauge(C,n)) &
(front_left_cell(it,k,Gauge(C,n)) meets C
implies
it turns_left k,Gauge(C,n));
end;
theorem :: JORDAN9:33
C is connected & 1 <= k & k+1 <= len Cage(C,n)
implies
left_cell(Cage(C,n),k,Gauge(C,n)) misses C &
right_cell(Cage(C,n),k,Gauge(C,n)) meets C;
theorem :: JORDAN9:34
C is connected implies N-min L~Cage(C,n) = (Cage(C,n))/.1;
Back to top