Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Artur Kornilowicz,
- Robert Milewski,
- Adam Naumowicz,
and
- Andrzej Trybulec
- Received September 12, 2000
- MML identifier: JORDAN1A
- [
Mizar article,
MML identifier index
]
environ
vocabulary EUCLID, COMPTS_1, SPPOL_1, RELAT_2, GOBOARD1, PRE_TOPC, ARYTM,
NAT_1, ARYTM_1, GROUP_1, ARYTM_3, CONNSP_1, BOOLE, RELAT_1, FINSEQ_1,
MATRIX_2, TOPREAL2, SEQM_3, GOBOARD5, TOPREAL1, MCART_1, PSCOMP_1,
JORDAN2C, SUBSET_1, JORDAN6, FUNCT_5, FUNCT_1, RCOMP_1, LATTICES,
METRIC_1, SQUARE_1, ABSVALUE, JORDAN1, TREES_1, MATRIX_1, FINSEQ_4,
TOPS_1, COMPLEX1, JORDAN8, INT_1, JORDAN9, GOBOARD9, JORDAN1A;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, INT_1, NAT_1, SQUARE_1, ABSVALUE, FUNCT_1, FUNCT_2, STRUCT_0,
FINSEQ_1, FINSEQ_4, BINARITH, NEWTON, PRE_TOPC, TOPS_1, CONNSP_1,
COMPTS_1, GOBOARD1, MATRIX_1, RCOMP_1, SEQ_4, METRIC_1, EUCLID, WSIERP_1,
TOPREAL1, TOPREAL2, PSCOMP_1, SPPOL_1, ABIAN, GOBOARD5, GOBOARD9,
JORDAN1, JGRAPH_1, JORDAN6, JORDAN8, JORDAN9, JORDAN2C, METRIC_6;
constructors ABSVALUE, CARD_4, CONNSP_1, FINSEQ_4, JORDAN8, JORDAN9, PSCOMP_1,
REAL_1, GOBRD13, BINARITH, WSIERP_1, RCOMP_1, JORDAN1, JORDAN2C,
SQUARE_1, GOBOARD9, TOPREAL2, TOPS_1, JORDAN6, TBSP_1, ABIAN, JORDAN5C,
REALSET1, TOPRNS_1, INT_1;
clusters XREAL_0, EUCLID, PSCOMP_1, RELSET_1, STRUCT_0, TOPREAL6, JORDAN8,
JORDAN10, INT_1, GOBOARD5, PRE_TOPC, SPRECT_3, BORSUK_2, NEWTON,
SPRECT_4, SPRECT_1, MEMBERED, ORDINAL2, NUMBERS;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
reserve
i, i1, i2, j, j1, j2, k, m, n, t for Nat,
D for non empty Subset of TOP-REAL 2,
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,
p, q, x for Point of TOP-REAL 2,
r, s for real number;
theorem :: JORDAN1A:1
for s1,s3,s4,l being real number st s1<=s3 & s1<=s4 & 0<=l & l<=1 holds
s1<=(1-l)*s3+l*s4;
theorem :: JORDAN1A:2
for s1,s3,s4,l being real number st s3<=s1 & s4<=s1 & 0<=l & l<=1 holds
(1-l)*s3+l*s4<=s1;
theorem :: JORDAN1A:3
n > 0 implies m |^ n mod m = 0;
theorem :: JORDAN1A:4
j > 0 & i mod j = 0 implies i div j = i / j;
theorem :: JORDAN1A:5
n > 0 implies i |^ n div i = i |^ n / i;
theorem :: JORDAN1A:6
0 < n & 1 < r implies 1 < r|^n;
theorem :: JORDAN1A:7
r > 1 & m > n implies r|^m > r|^n;
theorem :: JORDAN1A:8
for T being non empty TopSpace,
A being Subset of T,
B, C being Subset of T st
A is connected & C is_a_component_of B & A meets C & A c= B holds A c= C;
definition let f be FinSequence;
func Center f -> Nat equals
:: JORDAN1A:def 1
len f div 2 + 1;
end;
theorem :: JORDAN1A:9
for f being FinSequence st len f is odd holds len f = 2 * Center f - 1;
theorem :: JORDAN1A:10
for f being FinSequence st len f is even holds len f = 2 * Center f - 2;
begin :: Some subsets of the plane
definition
cluster compact non vertical non horizontal
being_simple_closed_curve non empty Subset of TOP-REAL 2;
cluster compact non empty horizontal Subset of TOP-REAL 2;
cluster compact non empty vertical Subset of TOP-REAL 2;
end;
theorem :: JORDAN1A:11
p in N-most D implies p`2 = N-bound D;
theorem :: JORDAN1A:12
p in E-most D implies p`1 = E-bound D;
theorem :: JORDAN1A:13
p in S-most D implies p`2 = S-bound D;
theorem :: JORDAN1A:14
p in W-most D implies p`1 = W-bound D;
theorem :: JORDAN1A:15
for D being Subset of TOP-REAL 2 holds BDD D misses D;
theorem :: JORDAN1A:16
for S being being_simple_closed_curve non empty Subset of TOP-REAL 2
holds Lower_Arc S c= S & Upper_Arc S c= S;
theorem :: JORDAN1A:17
p in Vertical_Line(p`1);
theorem :: JORDAN1A:18
|[r,s]| in Vertical_Line r;
theorem :: JORDAN1A:19
for A being Subset of TOP-REAL 2 st A c= Vertical_Line s
holds A is vertical;
theorem :: JORDAN1A:20
proj2. |[r,s]| = s & proj1. |[r,s]| = r;
theorem :: JORDAN1A:21
p`1 = q`1 & r in [. proj2.p,proj2.q .] implies |[p`1,r]| in LSeg(p,q);
theorem :: JORDAN1A:22
p`2 = q`2 & r in [. proj1.p,proj1.q .] implies |[r,p`2]| in LSeg(p,q);
theorem :: JORDAN1A:23
p in Vertical_Line s & q in Vertical_Line s
implies LSeg(p,q) c= Vertical_Line s;
definition
let S be non empty being_simple_closed_curve Subset of TOP-REAL 2;
cluster Lower_Arc S -> non empty compact;
cluster Upper_Arc S -> non empty compact;
end;
theorem :: JORDAN1A:24
for A,B being Subset of TOP-REAL 2 st A meets B
holds proj2.:A meets proj2.:B;
theorem :: JORDAN1A:25
for A,B being Subset of TOP-REAL 2
st A misses B & A c= Vertical_Line s & B c= Vertical_Line s
holds proj2.:A misses proj2.:B;
theorem :: JORDAN1A:26
for S being closed Subset of TOP-REAL 2 st S is Bounded
holds proj2.:S is closed;
theorem :: JORDAN1A:27
for S being Subset of TOP-REAL 2 st S is Bounded
holds proj2.:S is bounded;
theorem :: JORDAN1A:28
for S being compact Subset of TOP-REAL 2
holds proj2.:S is compact;
scheme TRSubsetEx { n() -> Nat, P[set] } :
ex A being Subset of TOP-REAL n() st
for p being Point of TOP-REAL n() holds p in A iff P[p];
scheme TRSubsetUniq { n() -> Nat, P[set] } :
for A, B being Subset of TOP-REAL n() st
(for p being Point of TOP-REAL n() holds p in A iff P[p]) &
(for p being Point of TOP-REAL n() holds p in B iff P[p])
holds A = B;
definition let p be Point of TOP-REAL 2;
func north_halfline p -> Subset of TOP-REAL 2 means
:: JORDAN1A:def 2
for x being Point of TOP-REAL 2 holds
x in it iff x`1 = p`1 & x`2 >= p`2;
func east_halfline p -> Subset of TOP-REAL 2 means
:: JORDAN1A:def 3
for x being Point of TOP-REAL 2 holds
x in it iff x`1 >= p`1 & x`2 = p`2;
func south_halfline p -> Subset of TOP-REAL 2 means
:: JORDAN1A:def 4
for x being Point of TOP-REAL 2 holds
x in it iff x`1 = p`1 & x`2 <= p`2;
func west_halfline p -> Subset of TOP-REAL 2 means
:: JORDAN1A:def 5
for x being Point of TOP-REAL 2 holds
x in it iff x`1 <= p`1 & x`2 = p`2;
end;
theorem :: JORDAN1A:29
north_halfline p =
{q where q is Point of TOP-REAL 2: q`1 = p`1 & q`2 >= p`2};
theorem :: JORDAN1A:30
north_halfline p =
{ |[ p`1,r ]| where r is Element of REAL: r >= p`2 };
theorem :: JORDAN1A:31
east_halfline p =
{q where q is Point of TOP-REAL 2: q`1 >= p`1 & q`2 = p`2};
theorem :: JORDAN1A:32
east_halfline p =
{ |[ r,p`2 ]| where r is Element of REAL: r >= p`1 };
theorem :: JORDAN1A:33
south_halfline p =
{q where q is Point of TOP-REAL 2: q`1 = p`1 & q`2 <= p`2};
theorem :: JORDAN1A:34
south_halfline p =
{ |[ p`1,r ]| where r is Element of REAL: r <= p`2 };
theorem :: JORDAN1A:35
west_halfline p =
{q where q is Point of TOP-REAL 2: q`1 <= p`1 & q`2 = p`2};
theorem :: JORDAN1A:36
west_halfline p =
{ |[ r,p`2 ]| where r is Element of REAL: r <= p`1 };
definition let p be Point of TOP-REAL 2;
cluster north_halfline p -> non empty convex;
cluster east_halfline p -> non empty convex;
cluster south_halfline p -> non empty convex;
cluster west_halfline p -> non empty convex;
end;
begin :: Goboards
theorem :: JORDAN1A:37
1 <= i & i <= len G & 1 <= j & j <= width G implies
G*(i,j) in LSeg(G*(i,1),G*(i,width G));
theorem :: JORDAN1A:38
1 <= i & i <= len G & 1 <= j & j <= width G implies
G*(i,j) in LSeg(G*(1,j),G*(len G,j));
theorem :: JORDAN1A:39
1 <= j1 & j1 <= width G & 1 <= j2 & j2 <= width G &
1 <= i1 & i1 <= i2 & i2 <= len G implies
G*(i1,j1)`1 <= G*(i2,j2)`1;
theorem :: JORDAN1A:40
1 <= i1 & i1 <= len G & 1 <= i2 & i2 <= len G &
1 <= j1 & j1 <= j2 & j2 <= width G implies
G*(i1,j1)`2 <= G*(i2,j2)`2;
theorem :: JORDAN1A:41
for f being non constant standard special_circular_sequence st
f is_sequence_on G & 1 <= t & t <= len G holds
G*(t,width G)`2 >= N-bound L~f;
theorem :: JORDAN1A:42
for f being non constant standard special_circular_sequence st
f is_sequence_on G & 1 <= t & t <= width G holds
G*(1,t)`1 <= W-bound L~f;
theorem :: JORDAN1A:43
for f being non constant standard special_circular_sequence st
f is_sequence_on G & 1 <= t & t <= len G holds
G*(t,1)`2 <= S-bound L~f;
theorem :: JORDAN1A:44
for f being non constant standard special_circular_sequence st
f is_sequence_on G & 1 <= t & t <= width G holds
G*(len G,t)`1 >= E-bound L~f;
theorem :: JORDAN1A:45
i<=len G & j<=width G implies cell(G,i,j) is non empty;
theorem :: JORDAN1A:46
i<=len G & j<=width G implies cell(G,i,j) is connected;
theorem :: JORDAN1A:47
i <= len G implies cell(G,i,0) is not Bounded;
theorem :: JORDAN1A:48
i <= len G implies cell(G,i,width G) is not Bounded;
begin :: Gauges
theorem :: JORDAN1A:49
width Gauge(D,n) = 2|^n + 3;
theorem :: JORDAN1A:50
i < j implies len Gauge(D,i) < len Gauge(D,j);
theorem :: JORDAN1A:51
i <= j implies len Gauge(D,i) <= len Gauge(D,j);
theorem :: JORDAN1A:52
m <= n & 1 < i & i < len Gauge(D,m)
implies 1 < 2|^(n-'m)*(i-2)+2 & 2|^(n-'m)*(i-2)+2 < len Gauge(D,n);
theorem :: JORDAN1A:53
m <= n & 1 < i & i < width Gauge(D,m)
implies 1 < 2|^(n-'m)*(i-2)+2 & 2|^(n-'m)*(i-2)+2 < width Gauge(D,n);
theorem :: JORDAN1A:54
m <= n & 1 < i & i < len Gauge(D,m) & 1 < j & j < width Gauge(D,m)
implies
for i1,j1 being Nat st
i1 = 2|^(n-'m)*(i-2)+2 & j1 = 2|^(n-'m)*(j-2)+2
holds Gauge(D,m)*(i,j) = Gauge(D,n)*(i1,j1);
theorem :: JORDAN1A:55
m <= n & 1 < i & i+1 < len Gauge(D,m)
implies 1 < 2|^(n-'m)*(i-1)+2 & 2|^(n-'m)*(i-1)+2 <= len Gauge(D,n);
theorem :: JORDAN1A:56
m <= n & 1 < i & i+1 < width Gauge(D,m)
implies 1 < 2|^(n-'m)*(i-1)+2 & 2|^(n-'m)*(i-1)+2 <= width Gauge(D,n);
theorem :: JORDAN1A:57
1 <= i & i <= len Gauge (D,n) &
1 <= j & j <= len Gauge (D,m) &
(n > 0 & m > 0 or n = 0 & m = 0) implies
Gauge(D,n)*(Center Gauge(D,n), i)`1 =
Gauge(D,m)*(Center Gauge(D,m), j)`1;
theorem :: JORDAN1A:58
1 <= i & i <= len Gauge (D,n) &
1 <= j & j <= len Gauge (D,m) &
(n > 0 & m > 0 or n = 0 & m = 0) implies
Gauge(D,n)*(i, Center Gauge(D,n))`2 =
Gauge(D,m)*(j, Center Gauge(D,m))`2;
theorem :: JORDAN1A:59
1 <= i & i <= len Gauge(C,1) implies
Gauge(C,1)*(Center Gauge(C,1),i)`1 = (W-bound C + E-bound C) / 2;
theorem :: JORDAN1A:60
1 <= i & i <= len Gauge(C,1) implies
Gauge(C,1)*(i,Center Gauge(C,1))`2 = (S-bound C + N-bound C) / 2;
theorem :: JORDAN1A:61
1 <= i & i <= len Gauge(E,n) & 1 <= j & j <= len Gauge(E,m) &
m <= n implies
Gauge(E,n)*(i,len Gauge(E,n))`2 <= Gauge(E,m)*(j,len Gauge(E,m))`2;
theorem :: JORDAN1A:62
1 <= i & i <= len Gauge(E,n) & 1 <= j & j <= len Gauge(E,m) &
m <= n implies
Gauge(E,n)*(len Gauge(E,n),i)`1 <= Gauge(E,m)*(len Gauge(E,m),j)`1;
theorem :: JORDAN1A:63
1 <= i & i <= len Gauge(E,n) & 1 <= j & j <= len Gauge(E,m) &
m <= n implies
Gauge(E,m)*(1,j)`1 <= Gauge(E,n)*(1,i)`1;
theorem :: JORDAN1A:64
1 <= i & i <= len Gauge(E,n) & 1 <= j & j <= len Gauge(E,m) &
m <= n implies
Gauge(E,m)*(j,1)`2 <= Gauge(E,n)*(i,1)`2;
theorem :: JORDAN1A:65
1 <= m & m <= n implies
LSeg(Gauge(E,n)*(Center Gauge(E,n),1),
Gauge(E,n)*(Center Gauge(E,n),len Gauge(E,n))) c=
LSeg(Gauge(E,m)*(Center Gauge(E,m),1),
Gauge(E,m)*(Center Gauge(E,m),len Gauge(E,m)));
theorem :: JORDAN1A:66
1 <= m & m <= n & 1 <= j & j <= width Gauge(E,n) implies
LSeg(Gauge(E,n)*(Center Gauge(E,n),1),
Gauge(E,n)*(Center Gauge(E,n),j)) c=
LSeg(Gauge(E,m)*(Center Gauge(E,m),1),
Gauge(E,n)*(Center Gauge(E,n),j));
theorem :: JORDAN1A:67
1 <= m & m <= n & 1 <= j & j <= width Gauge(E,n) implies
LSeg(Gauge(E,m)*(Center Gauge(E,m),1),
Gauge(E,n)*(Center Gauge(E,n),j)) c=
LSeg(Gauge(E,m)*(Center Gauge(E,m),1),
Gauge(E,m)*(Center Gauge(E,m),len Gauge(E,m)));
theorem :: JORDAN1A:68
m <= n & 1 < i & i+1 < len Gauge(E,m) & 1 < j & j+1 < width Gauge(E,m)
implies
for i1,j1 being Nat st
2|^(n-'m)*(i-2)+2 <= i1 & i1 < 2|^(n-'m)*(i-1)+2 &
2|^(n-'m)*(j-2)+2 <= j1 & j1 < 2|^(n-'m)*(j-1)+2
holds cell(Gauge(E,n),i1,j1) c= cell(Gauge(E,m),i,j);
theorem :: JORDAN1A:69
m <= n & 3 <= i & i < len Gauge(E,m) & 1 < j & j+1 < width Gauge(E,m)
implies
for i1,j1 being Nat st
i1 = 2|^(n-'m)*(i-2)+2 & j1 = 2|^(n-'m)*(j-2)+2
holds cell(Gauge(E,n),i1-'1,j1) c= cell(Gauge(E,m),i-'1,j);
theorem :: JORDAN1A:70
for C being compact non vertical non horizontal Subset of TOP-REAL 2 holds
i <= len Gauge(C,n) implies cell(Gauge(C,n),i,0) c= UBD C;
theorem :: JORDAN1A:71
for C being compact non vertical non horizontal Subset of TOP-REAL 2 holds
i <= len Gauge(E,n) implies cell(Gauge(E,n),i,width Gauge(E,n)) c= UBD E;
begin :: Cages
theorem :: JORDAN1A:72
p in C implies north_halfline p meets L~Cage(C,n);
theorem :: JORDAN1A:73
p in C implies east_halfline p meets L~Cage(C,n);
theorem :: JORDAN1A:74
p in C implies south_halfline p meets L~Cage(C,n);
theorem :: JORDAN1A:75
p in C implies west_halfline p meets L~Cage(C,n);
theorem :: JORDAN1A:76
ex k,t st 1 <= k & k < len Cage(C,n) & 1 <= t & t <= width (Gauge(C,n)) &
Cage(C,n)/.k = Gauge(C,n)*(1,t);
theorem :: JORDAN1A:77
ex k,t st 1 <= k & k < len Cage(C,n) & 1 <= t & t <= len (Gauge(C,n)) &
Cage(C,n)/.k = Gauge(C,n)*(t,1);
theorem :: JORDAN1A:78
ex k,t st 1 <= k & k < len Cage(C,n) & 1 <= t & t <= width (Gauge(C,n)) &
Cage(C,n)/.k = Gauge(C,n)*(len(Gauge(C,n)),t);
theorem :: JORDAN1A:79
1 <= k & k <= len Cage(C,n) & 1 <= t & t <= len (Gauge(C,n)) &
Cage(C,n)/.k = Gauge(C,n)*(t,width Gauge(C,n)) implies
Cage(C,n)/.k in N-most L~Cage(C,n);
theorem :: JORDAN1A:80
1 <= k & k <= len Cage(C,n) & 1 <= t & t <= width (Gauge(C,n)) &
Cage(C,n)/.k = Gauge(C,n)*(1,t) implies Cage(C,n)/.k in W-most L~Cage(C,n);
theorem :: JORDAN1A:81
1 <= k & k <= len Cage(C,n) & 1 <= t & t <= len (Gauge(C,n)) &
Cage(C,n)/.k = Gauge(C,n)*(t,1) implies Cage(C,n)/.k in S-most L~Cage(C,n);
theorem :: JORDAN1A:82
1 <= k & k <= len Cage(C,n) & 1 <= t & t <= width (Gauge(C,n)) &
Cage(C,n)/.k = Gauge(C,n)*(len Gauge(C,n),t) implies
Cage(C,n)/.k in E-most L~Cage(C,n);
theorem :: JORDAN1A:83
W-bound L~Cage(C,n) = W-bound C - (E-bound C - W-bound C)/(2|^n);
theorem :: JORDAN1A:84
S-bound L~Cage(C,n) = S-bound C - (N-bound C - S-bound C)/(2|^n);
theorem :: JORDAN1A:85
E-bound L~Cage(C,n) = E-bound C + (E-bound C - W-bound C)/(2|^n);
theorem :: JORDAN1A:86
N-bound L~Cage(C,n) + S-bound L~Cage(C,n) =
N-bound L~Cage(C,m) + S-bound L~Cage(C,m);
theorem :: JORDAN1A:87
E-bound L~Cage(C,n) + W-bound L~Cage(C,n) =
E-bound L~Cage(C,m) + W-bound L~Cage(C,m);
theorem :: JORDAN1A:88
i < j implies E-bound L~Cage(C,j) < E-bound L~Cage(C,i);
theorem :: JORDAN1A:89
i < j implies W-bound L~Cage(C,i) < W-bound L~Cage(C,j);
theorem :: JORDAN1A:90
i < j implies S-bound L~Cage(C,i) < S-bound L~Cage(C,j);
theorem :: JORDAN1A:91
1 <= i & i <= len Gauge(C,n) implies
N-bound L~Cage(C,n) = Gauge(C,n)*(i,len Gauge(C,n))`2;
theorem :: JORDAN1A:92
1 <= i & i <= len Gauge(C,n) implies
E-bound L~Cage(C,n) = Gauge(C,n)*(len Gauge(C,n),i)`1;
theorem :: JORDAN1A:93
1 <= i & i <= len Gauge(C,n) implies
S-bound L~Cage(C,n) = Gauge(C,n)*(i,1)`2;
theorem :: JORDAN1A:94
1 <= i & i <= len Gauge(C,n) implies
W-bound L~Cage(C,n) = Gauge(C,n)*(1,i)`1;
theorem :: JORDAN1A:95
x in C & p in north_halfline x /\ L~Cage(C,n) implies p`2 > x`2;
theorem :: JORDAN1A:96
x in C & p in east_halfline x /\ L~Cage(C,n) implies p`1 > x`1;
theorem :: JORDAN1A:97
x in C & p in south_halfline x /\ L~Cage(C,n) implies p`2 < x`2;
theorem :: JORDAN1A:98
x in C & p in west_halfline x /\ L~Cage(C,n) implies p`1 < x`1;
theorem :: JORDAN1A:99
x in N-most C & p in north_halfline x &
1 <= i & i < len Cage(C,n) & p in LSeg(Cage(C,n),i) implies
LSeg(Cage(C,n),i) is horizontal;
theorem :: JORDAN1A:100
x in E-most C & p in east_halfline x &
1 <= i & i < len Cage(C,n) & p in LSeg(Cage(C,n),i) implies
LSeg(Cage(C,n),i) is vertical;
theorem :: JORDAN1A:101
x in S-most C & p in south_halfline x &
1 <= i & i < len Cage(C,n) & p in LSeg(Cage(C,n),i) implies
LSeg(Cage(C,n),i) is horizontal;
theorem :: JORDAN1A:102
x in W-most C & p in west_halfline x &
1 <= i & i < len Cage(C,n) & p in LSeg(Cage(C,n),i) implies
LSeg(Cage(C,n),i) is vertical;
theorem :: JORDAN1A:103
x in N-most C & p in north_halfline x /\ L~Cage(C,n)
implies p`2 = N-bound L~Cage(C,n);
theorem :: JORDAN1A:104
x in E-most C & p in east_halfline x /\ L~Cage(C,n)
implies p`1 = E-bound L~Cage(C,n);
theorem :: JORDAN1A:105
x in S-most C & p in south_halfline x /\ L~Cage(C,n)
implies p`2 = S-bound L~Cage(C,n);
theorem :: JORDAN1A:106
x in W-most C & p in west_halfline x /\ L~Cage(C,n)
implies p`1 = W-bound L~Cage(C,n);
theorem :: JORDAN1A:107
x in N-most C implies
ex p being Point of TOP-REAL 2 st north_halfline x /\ L~Cage(C,n) = {p};
theorem :: JORDAN1A:108
x in E-most C implies
ex p being Point of TOP-REAL 2 st east_halfline x /\ L~Cage(C,n) = {p};
theorem :: JORDAN1A:109
x in S-most C implies
ex p being Point of TOP-REAL 2 st south_halfline x /\ L~Cage(C,n) = {p};
theorem :: JORDAN1A:110
x in W-most C implies
ex p being Point of TOP-REAL 2 st west_halfline x /\ L~Cage(C,n) = {p};
Back to top