Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Mariusz Giero
- Received May 27, 2002
- MML identifier: JORDAN12
- [
Mizar article,
MML identifier index
]
environ
vocabulary JORDAN12, FINSEQ_1, EUCLID, TOPREAL1, BOOLE, RELAT_1, REALSET1,
PRE_TOPC, FUNCT_1, GRAPH_2, GOBOARD5, CONNSP_1, SUBSET_1, CARD_1,
MATRIX_2, INT_1, FINSET_1, TARSKI, SETFAM_1, ARYTM_1, SEQM_3, RELAT_2,
GOBOARD9, MCART_1, MATRIX_1, GOBOARD2, FINSEQ_4, GOBOARD1, JORDAN1,
TOPS_1, TREES_1, SPPOL_1, FINSEQ_5;
notation TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, XCMPLX_0, XREAL_0, REAL_1,
NAT_1, BINARITH, ABIAN, INT_1, GRAPH_2, RELAT_1, CARD_1, FINSET_1,
FUNCT_1, FINSEQ_1, FINSEQ_4, MATRIX_1, STRUCT_0, REALSET1, PRE_TOPC,
TOPS_1, CONNSP_1, EUCLID, TOPREAL1, SPPOL_1, JORDAN1, GOBOARD1, GOBOARD2,
GOBOARD5, GOBOARD9, GOBRD13;
constructors REALSET1, FINSEQ_4, GRAPH_2, CONNSP_1, ABIAN, INT_1, GOBOARD9,
TOPS_1, GOBOARD2, BINARITH, GOBRD13, JORDAN1, SPPOL_1, COMPTS_1,
MEMBERED;
clusters RELSET_1, SPPOL_2, EUCLID, GOBOARD5, ABIAN, YELLOW13, SUBSET_1,
INT_1, GOBOARD2, GOBOARD9, JORDAN10, TEX_2, MEMBERED;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin
reserve i,j,k,n for Nat,
X,Y,a,b,c,x for set,
r,s for Real;
theorem :: JORDAN12:1
1 < i implies 0 < i-'1;
canceled;
theorem :: JORDAN12:3
1 is odd;
theorem :: JORDAN12:4
for f be FinSequence of TOP-REAL n
for i st 1 <= i & i + 1 <= len f holds
f/.i in rng f & f/.(i+1) in rng f;
definition
cluster s.n.c. -> s.c.c. FinSequence of TOP-REAL 2;
end;
theorem :: JORDAN12:5
for f,g be FinSequence of TOP-REAL 2 st
f ^' g is unfolded s.c.c. & len g >= 2 holds f is unfolded s.n.c.;
theorem :: JORDAN12:6
for g1,g2 be FinSequence of TOP-REAL 2 holds L~g1 c= L~(g1^'g2);
begin
definition let n; let f1,f2 be FinSequence of TOP-REAL n;
pred f1 is_in_general_position_wrt f2 means
:: JORDAN12:def 1
L~f1 misses rng f2 &
for i st 1<=i & i < len f2 holds L~f1 /\ LSeg(f2,i) is trivial;
end;
definition let n; let f1,f2 be FinSequence of TOP-REAL n;
pred f1,f2 are_in_general_position means
:: JORDAN12:def 2
f1 is_in_general_position_wrt f2 &
f2 is_in_general_position_wrt f1;
symmetry;
end;
theorem :: JORDAN12:7
for f1,f2 being FinSequence of TOP-REAL 2 st
f1,f2 are_in_general_position holds
for f being FinSequence of TOP-REAL 2 st f = f2|(Seg k)
holds f1,f are_in_general_position;
theorem :: JORDAN12:8
for f1,f2,g1,g2 be FinSequence of TOP-REAL 2 st
f1^'f2,g1^'g2 are_in_general_position holds
f1^'f2,g1 are_in_general_position;
reserve f,g for FinSequence of TOP-REAL 2;
theorem :: JORDAN12:9
for k,f,g st 1<=k & k+1<=len g &
f,g are_in_general_position holds g.k in (L~f)` & g.(k+1) in (L~f)`;
theorem :: JORDAN12:10
for f1,f2 be FinSequence of TOP-REAL 2
st f1,f2 are_in_general_position
for i,j st (1 <= i & i + 1 <= len f1 & 1 <= j & j + 1 <= len f2)
holds LSeg(f1,i) /\ LSeg(f2,j) is trivial;
theorem :: JORDAN12:11
for f,g holds
INTERSECTION({ LSeg(f,i) : 1 <= i & i+1 <= len f },
{ LSeg(g,j) : 1 <= j & j+1 <= len g }) is finite;
theorem :: JORDAN12:12
for f,g st f,g are_in_general_position holds
L~f /\ L~g is finite;
theorem :: JORDAN12:13
for f,g st f,g are_in_general_position
for k holds L~f /\ LSeg(g,k) is finite;
begin
reserve f for non constant standard special_circular_sequence,
p,p1,p2,q for Point of TOP-REAL 2;
theorem :: JORDAN12:14
for f,p1,p2 st LSeg(p1,p2) misses L~f
holds (ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
& p1 in C & p2 in C));
theorem :: JORDAN12:15
(ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)` &
a in C & b in C))
iff ((a in RightComp f & b in RightComp f) or
(a in LeftComp f & b in LeftComp f));
theorem :: JORDAN12:16
a in (L~f)` & b in (L~f)` & (not ex C be Subset of TOP-REAL 2 st
(C is_a_component_of (L~f)` & a in C & b in C))
iff ((a in LeftComp f & b in RightComp f) or
(a in RightComp f & b in LeftComp f));
theorem :: JORDAN12:17
for f,a,b,c st
((ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
& a in C & b in C)) &
(ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
& b in C & c in C))) holds
ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
& a in C & c in C);
theorem :: JORDAN12:18
for f,a,b,c st
a in (L~f)` & b in (L~f)` & c in (L~f)` &
((not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
& a in C & b in C)) &
(not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
& b in C & c in C))) holds
ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
& a in C & c in C);
begin
reserve G for Go-board;
theorem :: JORDAN12:19
i <= len G implies v_strip(G,i) is convex;
theorem :: JORDAN12:20
j <= width G implies h_strip(G,j) is convex;
theorem :: JORDAN12:21
i <= len G & j <= width G implies cell(G,i,j) is convex;
theorem :: JORDAN12:22
for f,k st 1<=k & k+1<=len f holds left_cell(f,k) is convex;
theorem :: JORDAN12:23
for f,k st 1<=k & k+1<=len f holds
left_cell(f,k,GoB f) is convex & right_cell(f,k,GoB f) is convex;
begin
theorem :: JORDAN12:24
for p1,p2,f
for r be Point of TOP-REAL 2 st
(r in LSeg(p1,p2) &
(ex x st (L~f) /\ LSeg(p1,p2) = {x}) &
not r in L~f)
holds L~f misses LSeg(p1,r) or L~f misses LSeg(r,p2);
theorem :: JORDAN12:25
for p,q,r,s being Point of TOP-REAL 2
st LSeg(p,q) is vertical & LSeg(r,s) is vertical &
LSeg(p,q) meets LSeg(r,s)
holds p`1 = r`1;
theorem :: JORDAN12:26
for p,p1,p2 st not p in LSeg(p1,p2) & p1`2 = p2`2 & p2`2 = p`2
holds p1 in LSeg(p,p2) or p2 in LSeg(p,p1);
theorem :: JORDAN12:27
for p,p1,p2 st not p in LSeg(p1,p2) & p1`1 = p2`1 & p2`1 = p`1
holds p1 in LSeg(p,p2) or p2 in LSeg(p,p1);
theorem :: JORDAN12:28
p <> p1 & p <> p2 & p in LSeg(p1,p2) implies not p1 in LSeg(p,p2);
theorem :: JORDAN12:29
for p,p1,p2,q st not q in LSeg(p1,p2) &
p in LSeg(p1,p2) & p <> p1 & p <> p2 &
(p1`1 = p2`1 & p2`1 = q`1 or p1`2 = p2`2 & p2`2 = q`2)
holds p1 in LSeg(q,p) or p2 in LSeg(q,p);
theorem :: JORDAN12:30
for p1,p2,p3,p4,p be Point of TOP-REAL 2 st
(p1`1 = p2`1 & p3`1 = p4`1 or p1`2 = p2`2 & p3`2 = p4`2)
& LSeg(p1,p2) /\ LSeg(p3,p4) = {p}
holds p=p1 or p=p2 or p=p3;
begin
theorem :: JORDAN12:31
for p,p1,p2,f st (L~f) /\ LSeg(p1,p2) = {p}
for r be Point of TOP-REAL 2 st not r in LSeg(p1,p2) &
not p1 in L~f & not p2 in L~f &
((p1`1 = p2`1 & p1`1 = r`1) or (p1`2 = p2`2 & p1`2 = r`2)) &
(ex i st (1<=i & i+1<= len f & (r in right_cell(f,i,GoB f) or
r in left_cell(f,i,GoB f)) & p in LSeg(f,i))) &
not r in L~f holds
(ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
& r in C & p1 in C)) or
(ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
& r in C & p2 in C));
theorem :: JORDAN12:32
for f,p1,p2,p st (L~f) /\ LSeg(p1,p2) = {p}
for rl,rp be Point of TOP-REAL 2 st
not p1 in L~f & not p2 in L~f &
((p1`1 = p2`1 & p1`1 = rl`1 & rl`1 = rp`1) or
(p1`2 = p2`2 & p1`2 = rl`2 & rl`2 = rp`2)) &
(ex i st (1<=i & i+1<= len f & rl in left_cell(f,i,GoB f) &
rp in right_cell(f,i,GoB f) & p in LSeg(f,i))) &
not rl in L~f &
not rp in L~f holds
not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
& p1 in C & p2 in C);
theorem :: JORDAN12:33
for p,f,p1,p2 st L~f /\ LSeg(p1,p2) = {p} &
(p1`1=p2`1 or p1`2=p2`2) &
not p1 in L~f & not p2 in L~f &
rng f misses LSeg(p1,p2) holds
not ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
& p1 in C & p2 in C);
theorem :: JORDAN12:34
for f being non constant standard special_circular_sequence,
g being special FinSequence of TOP-REAL 2 st f,g are_in_general_position
for k st 1<=k & k+1<= len g holds
Card (L~f /\ LSeg(g,k)) is even Nat iff
ex C be Subset of TOP-REAL 2 st (C is_a_component_of (L~f)`
& g.k in C & g.(k+1) in C);
theorem :: JORDAN12:35
for f1,f2,g1 being special FinSequence of TOP-REAL 2
st f1 ^' f2 is non constant standard special_circular_sequence &
f1 ^' f2, g1 are_in_general_position & len g1 >= 2 &
g1 is unfolded s.n.c. holds
Card (L~(f1 ^' f2) /\ L~g1) is even Nat iff
ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~(f1 ^' f2))`
& g1.1 in C & g1.len g1 in C;
theorem :: JORDAN12:36
for f1,f2,g1,g2 being special FinSequence of TOP-REAL 2
st f1 ^' f2 is non constant standard special_circular_sequence &
g1 ^' g2 is non constant standard special_circular_sequence &
L~f1 misses L~g2 & L~f2 misses L~g1 &
f1 ^' f2 , g1 ^' g2 are_in_general_position
for p1,p2,q1,q2 being Point of TOP-REAL 2
st f1.1 = p1 & f1.len f1 = p2 & g1.1 = q1 & g1.len g1 = q2 &
f1/.len f1 = f2/.1 & g1/.len g1 = g2/.1 &
p1 in L~f1 /\ L~f2 & q1 in L~g1 /\ L~g2 &
ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~(f1 ^' f2))`
& q1 in C & q2 in C
ex C be Subset of TOP-REAL 2 st C is_a_component_of (L~(g1 ^' g2))`
& p1 in C & p2 in C;
Back to top