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 August 1, 2002
- MML identifier: JORDAN15
- [
Mizar article,
MML identifier index
]
environ
vocabulary JORDAN8, PSCOMP_1, BOOLE, JORDAN1A, JORDAN9, GOBOARD1, GOBOARD5,
JORDAN6, SPRECT_2, JORDAN3, FINSEQ_5, JORDAN2C, GROUP_2, 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,
GOBOARD2, GRAPH_2, ORDINAL2, LATTICES, SEQ_2, FUNCT_5, ARYTM;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0,
REAL_1, NAT_1, SQUARE_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_4, FINSEQ_5,
SEQ_4, MATRIX_1, REALSET1, FINSEQ_6, GRAPH_2, STRUCT_0, PRE_TOPC,
RCOMP_1, TOPREAL2, BINARITH, CONNSP_1, COMPTS_1, EUCLID, PSCOMP_1,
SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD2, GOBOARD5, GOBOARD9, GOBRD13,
SPPOL_1, 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,
JORDAN1, JORDAN3, TOPREAL2, JORDAN5C, GRAPH_2, SPRECT_1, GOBOARD2,
JORDAN1E, RCOMP_1, WSIERP_1, JORDAN1H, ENUMSET1, INT_1;
clusters XREAL_0, SPRECT_1, TOPREAL6, JORDAN8, REVROT_1, INT_1, RELSET_1,
SPRECT_3, GOBOARD2, SPPOL_2, JORDAN1A, JORDAN1B, JORDAN1E, GOBRD11,
XBOOLE_0, SPRECT_4, BORSUK_2, PSCOMP_1, JORDAN1J, MEMBERED, NUMBERS,
ORDINAL2;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
begin
reserve n for Nat;
theorem :: JORDAN15:1
for A,B be Subset of TOP-REAL 2 st A meets B holds
proj1.:A meets proj1.:B;
theorem :: JORDAN15:2
for A,B be Subset of TOP-REAL 2
for s be real number st
A misses B & A c= Horizontal_Line s & B c= Horizontal_Line s holds
proj1.:A misses proj1.:B;
theorem :: JORDAN15:3
for S be closed Subset of TOP-REAL 2 st S is Bounded holds
proj1.:S is closed;
theorem :: JORDAN15:4
for S be compact Subset of TOP-REAL 2 holds proj1.:S is compact;
theorem :: JORDAN15:5
for p,q,p1,q1 be Point of TOP-REAL 2 st
LSeg(p,q) is vertical & LSeg(p1,q1) is vertical & p`1 = p1`1 &
p`2 <= p1`2 & p1`2 <= q1`2 & q1`2 <= q`2 holds
LSeg(p1,q1) c= LSeg(p,q);
theorem :: JORDAN15:6
for p,q,p1,q1 be Point of TOP-REAL 2 st
LSeg(p,q) is horizontal & LSeg(p1,q1) is horizontal & p`2 = p1`2 &
p`1 <= p1`1 & p1`1 <= q1`1 & q1`1 <= q`1 holds
LSeg(p1,q1) c= LSeg(p,q);
theorem :: JORDAN15:7
for G be Go-board
for i,j,k,j1,k1 be Nat st
1 <= i & i <= len G &
1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= width G holds
LSeg(G*(i,j1),G*(i,k1)) c= LSeg(G*(i,j),G*(i,k));
theorem :: JORDAN15:8
for G be Go-board
for i,j,k,j1,k1 be Nat st
1 <= i & i <= width G &
1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= len G holds
LSeg(G*(j1,i),G*(k1,i)) c= LSeg(G*(j,i),G*(k,i));
theorem :: JORDAN15:9
for G be Go-board
for j,k,j1,k1 be Nat st
1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= width G holds
LSeg(G*(Center G,j1),G*(Center G,k1)) c=
LSeg(G*(Center G,j),G*(Center G,k));
theorem :: JORDAN15:10
for G be Go-board st len G = width G
for j,k,j1,k1 be Nat st
1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= len G holds
LSeg(G*(j1,Center G),G*(k1,Center G)) c=
LSeg(G*(j,Center G),G*(k,Center G));
theorem :: JORDAN15:11
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 & j <= k & k <= width Gauge(C,n) &
Gauge(C,n)*(i,j) in L~Lower_Seq(C,n)
ex j1 be Nat st
j <= j1 & j1 <= k &
LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i,j1)};
theorem :: JORDAN15:12
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 & j <= k & k <= width Gauge(C,n) &
Gauge(C,n)*(i,k) in L~Upper_Seq(C,n)
ex k1 be Nat st
j <= k1 & k1 <= k &
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k1)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i,k1)};
theorem :: JORDAN15:13
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 & j <= k & k <= width Gauge(C,n) &
Gauge(C,n)*(i,j) in L~Lower_Seq(C,n) &
Gauge(C,n)*(i,k) in L~Upper_Seq(C,n)
ex j1,k1 be Nat st
j <= j1 & j1 <= k1 & k1 <= k &
LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i,j1)} &
LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i,k1)};
theorem :: JORDAN15:14
for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
for i,j,k be Nat st
1 <= j & j <= k & k <= len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
Gauge(C,n)*(j,i) in L~Lower_Seq(C,n)
ex j1 be Nat st
j <= j1 & j1 <= k &
LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k,i)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(j1,i)};
theorem :: JORDAN15:15
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for i,j,k be Nat st
1 <= j & j <= k & k <= len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
Gauge(C,n)*(k,i) in L~Upper_Seq(C,n)
ex k1 be Nat st
j <= k1 & k1 <= k &
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k1,i)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(k1,i)};
theorem :: JORDAN15:16
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for i,j,k be Nat st
1 <= j & j <= k & k <= len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
Gauge(C,n)*(j,i) in L~Lower_Seq(C,n) &
Gauge(C,n)*(k,i) in L~Upper_Seq(C,n)
ex j1,k1 be Nat st
j <= j1 & j1 <= k1 & k1 <= k &
LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k1,i)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(j1,i)} &
LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k1,i)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(k1,i)};
theorem :: JORDAN15:17
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 & j <= k & k <= width Gauge(C,n) &
Gauge(C,n)*(i,j) in L~Upper_Seq(C,n)
ex j1 be Nat st
j <= j1 & j1 <= k &
LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i,j1)};
theorem :: JORDAN15:18
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 & j <= k & k <= width Gauge(C,n) &
Gauge(C,n)*(i,k) in L~Lower_Seq(C,n)
ex k1 be Nat st
j <= k1 & k1 <= k &
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k1)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i,k1)};
theorem :: JORDAN15:19
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 & j <= k & k <= width Gauge(C,n) &
Gauge(C,n)*(i,j) in L~Upper_Seq(C,n) &
Gauge(C,n)*(i,k) in L~Lower_Seq(C,n)
ex j1,k1 be Nat st
j <= j1 & j1 <= k1 & k1 <= k &
LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i,j1)} &
LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i,k1)};
theorem :: JORDAN15:20
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for i,j,k be Nat st
1 <= j & j <= k & k <= len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
Gauge(C,n)*(j,i) in L~Upper_Seq(C,n)
ex j1 be Nat st
j <= j1 & j1 <= k &
LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k,i)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(j1,i)};
theorem :: JORDAN15:21
for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
for i,j,k be Nat st
1 <= j & j <= k & k <= len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
Gauge(C,n)*(k,i) in L~Lower_Seq(C,n)
ex k1 be Nat st
j <= k1 & k1 <= k &
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k1,i)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(k1,i)};
theorem :: JORDAN15:22
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for i,j,k be Nat st
1 <= j & j <= k & k <= len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
Gauge(C,n)*(j,i) in L~Upper_Seq(C,n) &
Gauge(C,n)*(k,i) in L~Lower_Seq(C,n)
ex j1,k1 be Nat st
j <= j1 & j1 <= k1 & k1 <= k &
LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k1,i)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(j1,i)} &
LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k1,i)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(k1,i)};
theorem :: JORDAN15:23
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) &
Gauge(C,n)*(i,k) in L~Upper_Seq(C,n) &
Gauge(C,n)*(i,j) in L~Lower_Seq(C,n) holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C;
theorem :: JORDAN15:24
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) &
Gauge(C,n)*(i,k) in L~Upper_Seq(C,n) &
Gauge(C,n)*(i,j) in L~Lower_Seq(C,n) holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C;
theorem :: JORDAN15:25
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 &
Gauge(C,n)*(i,k) in Upper_Arc L~Cage(C,n) &
Gauge(C,n)*(i,j) in Lower_Arc L~Cage(C,n) holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C;
theorem :: JORDAN15:26
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 &
Gauge(C,n)*(i,k) in Upper_Arc L~Cage(C,n) &
Gauge(C,n)*(i,j) in Lower_Arc L~Cage(C,n) holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C;
theorem :: JORDAN15:27
for C be Simple_closed_curve
for j,k be Nat holds
1 <= j & j <= k & k <= width Gauge(C,n+1) &
Gauge(C,n+1)*(Center Gauge(C,n+1),k) in Upper_Arc L~Cage(C,n+1) &
Gauge(C,n+1)*(Center Gauge(C,n+1),j) in Lower_Arc L~Cage(C,n+1) 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 :: JORDAN15:28
for C be Simple_closed_curve
for j,k be Nat holds
1 <= j & j <= k & k <= width Gauge(C,n+1) &
Gauge(C,n+1)*(Center Gauge(C,n+1),k) in Upper_Arc L~Cage(C,n+1) &
Gauge(C,n+1)*(Center Gauge(C,n+1),j) in Lower_Arc L~Cage(C,n+1) 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;
theorem :: JORDAN15:29
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for i,j,k be Nat st
1 < j & k < len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
Gauge(C,n)*(k,i) in L~Upper_Seq(C,n) &
Gauge(C,n)*(j,i) in L~Lower_Seq(C,n) holds j <> k;
theorem :: JORDAN15:30
for C be Simple_closed_curve
for i,j,k be Nat st
1 < j & j <= k & k < len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(k,i)} &
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(j,i)} holds
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Lower_Arc C;
theorem :: JORDAN15:31
for C be Simple_closed_curve
for i,j,k be Nat st
1 < j & j <= k & k < len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(k,i)} &
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(j,i)} holds
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Upper_Arc C;
theorem :: JORDAN15:32
for C be Simple_closed_curve
for i,j,k be Nat st
1 < j & j <= k & k < len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
Gauge(C,n)*(k,i) in L~Upper_Seq(C,n) &
Gauge(C,n)*(j,i) in L~Lower_Seq(C,n) holds
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Lower_Arc C;
theorem :: JORDAN15:33
for C be Simple_closed_curve
for i,j,k be Nat st
1 < j & j <= k & k < len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
Gauge(C,n)*(k,i) in L~Upper_Seq(C,n) &
Gauge(C,n)*(j,i) in L~Lower_Seq(C,n) holds
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Upper_Arc C;
theorem :: JORDAN15:34
for C be Simple_closed_curve
for i,j,k be Nat st
1 < j & j <= k & k < len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) & n > 0 &
Gauge(C,n)*(k,i) in Upper_Arc L~Cage(C,n) &
Gauge(C,n)*(j,i) in Lower_Arc L~Cage(C,n) holds
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Lower_Arc C;
theorem :: JORDAN15:35
for C be Simple_closed_curve
for i,j,k be Nat st
1 < j & j <= k & k < len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) & n > 0 &
Gauge(C,n)*(k,i) in Upper_Arc L~Cage(C,n) &
Gauge(C,n)*(j,i) in Lower_Arc L~Cage(C,n) holds
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Upper_Arc C;
theorem :: JORDAN15:36
for C be Simple_closed_curve
for j,k be Nat holds
1 < j & j <= k & k < len Gauge(C,n+1) &
Gauge(C,n+1)*(k,Center Gauge(C,n+1)) in Upper_Arc L~Cage(C,n+1) &
Gauge(C,n+1)*(j,Center Gauge(C,n+1)) in Lower_Arc L~Cage(C,n+1) implies
LSeg(Gauge(C,n+1)*(j,Center Gauge(C,n+1)),
Gauge(C,n+1)*(k,Center Gauge(C,n+1))) meets Lower_Arc C;
theorem :: JORDAN15:37
for C be Simple_closed_curve
for j,k be Nat holds
1 < j & j <= k & k < len Gauge(C,n+1) &
Gauge(C,n+1)*(k,Center Gauge(C,n+1)) in Upper_Arc L~Cage(C,n+1) &
Gauge(C,n+1)*(j,Center Gauge(C,n+1)) in Lower_Arc L~Cage(C,n+1) implies
LSeg(Gauge(C,n+1)*(j,Center Gauge(C,n+1)),
Gauge(C,n+1)*(k,Center Gauge(C,n+1))) meets Upper_Arc C;
theorem :: JORDAN15:38
for C be Simple_closed_curve
for i,j,k be Nat st
1 < j & j <= k & k < len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(j,i)} &
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(k,i)} holds
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Lower_Arc C;
theorem :: JORDAN15:39
for C be Simple_closed_curve
for i,j,k be Nat st
1 < j & j <= k & k < len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(j,i)} &
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(k,i)} holds
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Upper_Arc C;
theorem :: JORDAN15:40
for C be Simple_closed_curve
for i,j,k be Nat st
1 < j & j <= k & k < len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
Gauge(C,n)*(j,i) in L~Upper_Seq(C,n) &
Gauge(C,n)*(k,i) in L~Lower_Seq(C,n) holds
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Lower_Arc C;
theorem :: JORDAN15:41
for C be Simple_closed_curve
for i,j,k be Nat st
1 < j & j <= k & k < len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) &
Gauge(C,n)*(j,i) in L~Upper_Seq(C,n) &
Gauge(C,n)*(k,i) in L~Lower_Seq(C,n) holds
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Upper_Arc C;
theorem :: JORDAN15:42
for C be Simple_closed_curve
for i,j,k be Nat st
1 < j & j <= k & k < len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) & n > 0 &
Gauge(C,n)*(j,i) in Upper_Arc L~Cage(C,n) &
Gauge(C,n)*(k,i) in Lower_Arc L~Cage(C,n) holds
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Lower_Arc C;
theorem :: JORDAN15:43
for C be Simple_closed_curve
for i,j,k be Nat st
1 < j & j <= k & k < len Gauge(C,n) &
1 <= i & i <= width Gauge(C,n) & n > 0 &
Gauge(C,n)*(j,i) in Upper_Arc L~Cage(C,n) &
Gauge(C,n)*(k,i) in Lower_Arc L~Cage(C,n) holds
LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Upper_Arc C;
theorem :: JORDAN15:44
for C be Simple_closed_curve
for j,k be Nat holds
1 < j & j <= k & k < len Gauge(C,n+1) &
Gauge(C,n+1)*(j,Center Gauge(C,n+1)) in Upper_Arc L~Cage(C,n+1) &
Gauge(C,n+1)*(k,Center Gauge(C,n+1)) in Lower_Arc L~Cage(C,n+1) implies
LSeg(Gauge(C,n+1)*(j,Center Gauge(C,n+1)),
Gauge(C,n+1)*(k,Center Gauge(C,n+1))) meets Lower_Arc C;
theorem :: JORDAN15:45
for C be Simple_closed_curve
for j,k be Nat holds
1 < j & j <= k & k < len Gauge(C,n+1) &
Gauge(C,n+1)*(j,Center Gauge(C,n+1)) in Upper_Arc L~Cage(C,n+1) &
Gauge(C,n+1)*(k,Center Gauge(C,n+1)) in Lower_Arc L~Cage(C,n+1) implies
LSeg(Gauge(C,n+1)*(j,Center Gauge(C,n+1)),
Gauge(C,n+1)*(k,Center Gauge(C,n+1))) meets Upper_Arc C;
theorem :: JORDAN15:46
for C be Simple_closed_curve
for i1,i2,j,k be Nat st
1 < i1 & i1 <= i2 & i2 < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i2,k)} &
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i1,j)} holds
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) meets Upper_Arc C;
theorem :: JORDAN15:47
for C be Simple_closed_curve
for i1,i2,j,k be Nat st
1 < i1 & i1 <= i2 & i2 < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i2,k)} &
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i1,j)} holds
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) meets Lower_Arc C;
theorem :: JORDAN15:48
for C be Simple_closed_curve
for i1,i2,j,k be Nat st
1 < i2 & i2 <= i1 & i1 < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i2,k)} &
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i1,j)} holds
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) meets Upper_Arc C;
theorem :: JORDAN15:49
for C be Simple_closed_curve
for i1,i2,j,k be Nat st
1 < i2 & i2 <= i1 & i1 < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i2,k)} &
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i1,j)} holds
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) meets Lower_Arc C;
theorem :: JORDAN15:50
for C be Simple_closed_curve
for i1,i2,j,k be Nat holds
1 < i1 & i1 < len Gauge(C,n+1) & 1 < i2 & i2 < len Gauge(C,n+1) &
1 <= j & j <= k & k <= width Gauge(C,n+1) &
Gauge(C,n+1)*(i1,k) in Upper_Arc L~Cage(C,n+1) &
Gauge(C,n+1)*(i2,j) in Lower_Arc L~Cage(C,n+1) implies
LSeg(Gauge(C,n+1)*(i2,j),Gauge(C,n+1)*(i2,k)) \/
LSeg(Gauge(C,n+1)*(i2,k),Gauge(C,n+1)*(i1,k)) meets Upper_Arc C;
theorem :: JORDAN15:51
for C be Simple_closed_curve
for i1,i2,j,k be Nat holds
1 < i1 & i1 < len Gauge(C,n+1) & 1 < i2 & i2 < len Gauge(C,n+1) &
1 <= j & j <= k & k <= width Gauge(C,n+1) &
Gauge(C,n+1)*(i1,k) in Upper_Arc L~Cage(C,n+1) &
Gauge(C,n+1)*(i2,j) in Lower_Arc L~Cage(C,n+1) implies
LSeg(Gauge(C,n+1)*(i2,j),Gauge(C,n+1)*(i2,k)) \/
LSeg(Gauge(C,n+1)*(i2,k),Gauge(C,n+1)*(i1,k)) meets Lower_Arc C;
theorem :: JORDAN15:52
for C be Simple_closed_curve
for i,j,k be Nat holds
1 < i & i < len Gauge(C,n+1) &
1 <= j & j <= k & k <= width Gauge(C,n+1) &
Gauge(C,n+1)*(i,k) in Upper_Arc L~Cage(C,n+1) &
Gauge(C,n+1)*(Center Gauge(C,n+1),j) in Lower_Arc L~Cage(C,n+1) implies
LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j),
Gauge(C,n+1)*(Center Gauge(C,n+1),k)) \/
LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),k),Gauge(C,n+1)*(i,k)) meets
Upper_Arc C;
theorem :: JORDAN15:53
for C be Simple_closed_curve
for i,j,k be Nat holds
1 < i & i < len Gauge(C,n+1) &
1 <= j & j <= k & k <= width Gauge(C,n+1) &
Gauge(C,n+1)*(i,k) in Upper_Arc L~Cage(C,n+1) &
Gauge(C,n+1)*(Center Gauge(C,n+1),j) in Lower_Arc L~Cage(C,n+1) implies
LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j),
Gauge(C,n+1)*(Center Gauge(C,n+1),k)) \/
LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),k),Gauge(C,n+1)*(i,k)) meets
Lower_Arc C;
Back to top