:: Properties of the External Approximation of Jordan's Curve
:: by Artur Korni{\l}owicz
::
:: Received June 24, 1999
:: Copyright (c) 1999-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, RELAT_2, RCOMP_1, SPPOL_1, SUBSET_1, EUCLID, TOPREAL1,
XXREAL_0, ARYTM_3, FINSEQ_1, JORDAN9, MATRIX_1, JORDAN8, PARTFUN1,
RELAT_1, TREES_1, GOBOARD1, GOBOARD5, ARYTM_1, CARD_1, XBOOLE_0, TARSKI,
RLTOPSP1, PSCOMP_1, NEWTON, MCART_1, PRE_TOPC, GOBOARD9, TOPS_1, REAL_1,
CONNSP_1, STRUCT_0, JORDAN2C, CONNSP_3, XXREAL_2, SETFAM_1, ZFMISC_1,
TOPREAL4, PCOMPS_1, WEIERSTR, METRIC_1, JORDAN10, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, REAL_1, NAT_1, NAT_D, PARTFUN1, FINSEQ_1, NEWTON, DOMAIN_1,
STRUCT_0, METRIC_1, TBSP_1, WEIERSTR, PRE_TOPC, TOPS_1, CONNSP_1,
CONNSP_3, COMPTS_1, PCOMPS_1, MATRIX_0, RLTOPSP1, EUCLID, TOPREAL1,
GOBOARD1, GOBOARD5, TOPREAL4, PSCOMP_1, GOBOARD9, SPPOL_1, JORDAN2C,
JORDAN8, GOBRD13, TOPREAL6, JORDAN9, XXREAL_0;
constructors REAL_1, NEWTON, TOPS_1, CONNSP_1, TBSP_1, TOPREAL4, PSCOMP_1,
WEIERSTR, GOBOARD9, CONNSP_3, JORDAN2C, TOPREAL6, JORDAN8, GOBRD13,
JORDAN9, NAT_D, FUNCSDOM;
registrations SUBSET_1, RELSET_1, FINSEQ_1, STRUCT_0, PRE_TOPC, COMPTS_1,
PCOMPS_1, EUCLID, TOPREAL1, SPPOL_2, SPRECT_1, JORDAN2C, TOPREAL6,
JORDAN8, FUNCT_1, NEWTON, ORDINAL1, XREAL_0, NAT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, SUBSET_1, PSCOMP_1, CONNSP_3;
expansions TARSKI, XBOOLE_0;
theorems CONNSP_1, CONNSP_3, EUCLID, GOBOARD6, GOBOARD7, GOBOARD9, GOBRD11,
GOBRD13, GOBRD14, JGRAPH_1, JORDAN2C, JORDAN3, JORDAN6, JORDAN8, JORDAN9,
NEWTON, NAT_1, PRE_TOPC, SETFAM_1, SPPOL_2, SPRECT_1, SPRECT_3, SPRECT_4,
SUBSET_1, TARSKI, TOPREAL1, TOPREAL3, TOPREAL4, TOPREAL6, TOPS_1,
WEIERSTR, ZFMISC_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0,
MATRIX_0, XREAL_0, COMPTS_1, RLTOPSP1, NAT_D;
schemes NAT_1;
begin :: Properties of the external approximation of Jordan's curve
registration
cluster connected compact non vertical non horizontal for
Subset of TOP-REAL 2;
existence
proof
take R^2-unit_square;
thus thesis;
end;
end;
reserve i, j, k, n for Nat,
P for Subset of TOP-REAL 2,
C for connected compact non vertical non horizontal Subset of TOP-REAL 2;
theorem Th1:
1 <= k & k+1 <= len Cage(C,n) & [i,j] in Indices Gauge(C,n) & [i,
j+1] in Indices Gauge(C,n) & Cage(C,n)/.k = Gauge(C,n)*(i,j) & Cage(C,n)/.(k+1)
= Gauge(C,n)*(i,j+1) implies i < len Gauge(C,n)
proof
set f = Cage(C,n), G = Gauge(C,n);
assume that
A1: 1 <= k & k+1 <= len Cage(C,n) and
A2: [i,j] in Indices Gauge(C,n) and
A3: [i,j+1] in Indices Gauge(C,n) & Cage(C,n)/.k = Gauge(C,n)*(i,j) &
Cage(C,n)/.(k+1) = Gauge(C,n)*(i,j+1);
assume
A4: i >= len G;
len G = width G by JORDAN8:def 1;
then
A5: j <= len G by A2,MATRIX_0:32;
i <= len G by A2,MATRIX_0:32;
then
A6: i = len G by A4,XXREAL_0:1;
f is_sequence_on G by JORDAN9:def 1;
then right_cell(f,k,G) = cell(G,i,j) by A1,A2,A3,GOBRD13:22;
hence contradiction by A1,A6,A5,JORDAN8:16,JORDAN9:31;
end;
theorem Th2:
1 <= k & k+1 <= len Cage(C,n) & [i,j] in Indices Gauge(C,n) & [i,
j+1] in Indices Gauge(C,n) & Cage(C,n)/.k = Gauge(C,n)*(i,j+1) & Cage(C,n)/.(k+
1) = Gauge(C,n)*(i,j) implies i > 1
proof
set f = Cage(C,n), G = Gauge(C,n);
assume that
A1: 1 <= k & k+1 <= len Cage(C,n) and
A2: [i,j] in Indices Gauge(C,n) and
A3: [i,j+1] in Indices Gauge(C,n) & Cage(C,n)/.k = Gauge(C,n)*(i,j+1) &
Cage (C,n)/.(k+1) = Gauge(C,n)*(i,j);
assume
A4: i <= 1;
1 <= i by A2,MATRIX_0:32;
then i = 1 by A4,XXREAL_0:1;
then
A5: i-'1 = 0 by XREAL_1:232;
len G = width G by JORDAN8:def 1;
then
A6: j <= len G by A2,MATRIX_0:32;
f is_sequence_on G by JORDAN9:def 1;
then right_cell(f,k,G) = cell(G,i-'1,j) by A1,A2,A3,GOBRD13:28;
hence contradiction by A1,A5,A6,JORDAN8:18,JORDAN9:31;
end;
theorem Th3:
1 <= k & k+1 <= len Cage(C,n) & [i,j] in Indices Gauge(C,n) & [i+
1,j] in Indices Gauge(C,n) & Cage(C,n)/.k = Gauge(C,n)*(i,j) & Cage(C,n)/.(k+1)
= Gauge(C,n)*(i+1,j) implies j > 1
proof
set f = Cage(C,n), G = Gauge(C,n);
assume that
A1: 1 <= k & k+1 <= len Cage(C,n) and
A2: [i,j] in Indices Gauge(C,n) and
A3: [i+1,j] in Indices Gauge(C,n) & Cage(C,n)/.k = Gauge(C,n)*(i,j) &
Cage(C,n)/.(k+1) = Gauge(C,n)*(i+1,j);
assume
A4: j <= 1;
1 <= j by A2,MATRIX_0:32;
then j = 1 by A4,XXREAL_0:1;
then
A5: j-'1 = 0 by XREAL_1:232;
A6: i <= len G by A2,MATRIX_0:32;
f is_sequence_on G by JORDAN9:def 1;
then right_cell(f,k,G) = cell(G,i,j-'1) by A1,A2,A3,GOBRD13:24;
hence contradiction by A1,A5,A6,JORDAN8:17,JORDAN9:31;
end;
theorem Th4:
1 <= k & k+1 <= len Cage(C,n) & [i,j] in Indices Gauge(C,n) & [i+
1,j] in Indices Gauge(C,n) & Cage(C,n)/.k = Gauge(C,n)*(i+1,j) & Cage(C,n)/.(k+
1) = Gauge(C,n)*(i,j) implies j < width Gauge(C,n)
proof
set f = Cage(C,n), G = Gauge(C,n);
assume that
A1: 1 <= k & k+1 <= len Cage(C,n) and
A2: [i,j] in Indices Gauge(C,n) and
A3: [i+1,j] in Indices Gauge(C,n) & Cage(C,n)/.k = Gauge(C,n)*(i+1,j) &
Cage (C,n)/.(k+1) = Gauge(C,n)*(i,j);
assume
A4: j >= width G;
j <= width G by A2,MATRIX_0:32;
then
A5: j = width G by A4,XXREAL_0:1;
A6: len G = width G & i <= len G by A2,JORDAN8:def 1,MATRIX_0:32;
f is_sequence_on G by JORDAN9:def 1;
then right_cell(f,k,G) = cell(G,i,j) by A1,A2,A3,GOBRD13:26;
hence contradiction by A1,A5,A6,JORDAN8:15,JORDAN9:31;
end;
theorem Th5:
C misses L~Cage(C,n)
proof
set f = Cage(C,n), G = Gauge(C,n);
assume not thesis;
then consider c being object such that
A1: c in C and
A2: c in L~f by XBOOLE_0:3;
L~f = union { LSeg(f,i) where i is Nat: 1 <= i & i+1 <= len f
} by TOPREAL1:def 4;
then consider Z being set such that
A3: c in Z and
A4: Z in { LSeg(f,i) where i is Nat: 1 <= i & i+1 <= len f }
by A2,TARSKI:def 4;
consider i being Nat such that
A5: Z = LSeg(f,i) and
A6: 1 <= i & i+1 <= len f by A4;
f is_sequence_on G by JORDAN9:def 1;
then LSeg(f,i) = left_cell(f,i,G) /\ right_cell(f,i,G) by A6,GOBRD13:29;
then
A7: c in left_cell(f,i,G) by A3,A5,XBOOLE_0:def 4;
left_cell(f,i,G) misses C by A6,JORDAN9:31;
hence contradiction by A1,A7,XBOOLE_0:3;
end;
theorem Th6:
N-bound L~Cage(C,n) = N-bound C + (N-bound C - S-bound C)/(2|^n)
proof
set a = N-bound C, s = S-bound C, w = W-bound C, f = Cage(C,n), G = Gauge(C,
n);
consider i such that
A1: 1 <= i and
A2: i+1 <= len G and
A3: f/.1 = G*(i,width G) and
f/.2 = G*(i+1,width G) and
N-min C in cell(G,i,width G-'1) and
N-min C <> G*(i,width G-'1) by JORDAN9:def 1;
A4: len G = width G by JORDAN8:def 1;
4 <= len G by JORDAN8:10;
then
A5: 1 <= len G by XXREAL_0:2;
i+0 <= i+1 by XREAL_1:6;
then i <= len G by A2,XXREAL_0:2;
then
A6: [i,len G] in Indices G by A1,A4,A5,MATRIX_0:30;
A7: 2|^n <> 0 by NEWTON:83;
thus N-bound L~f = (N-min L~f)`2 by EUCLID:52
.= (f/.1)`2 by JORDAN9:32
.= |[w+((E-bound C-w)/(2|^n))*(i-2), s+((a-s)/(2|^n))*(len G-2)]|`2 by A3
,A4,A6,JORDAN8:def 1
.= s+((a-s)/(2|^n))*(len G-2) by EUCLID:52
.= s+((a-s)/(2|^n))*(2|^n+3-2) by JORDAN8:def 1
.= s+((a-s)/(2|^n))*2|^n+(a-s)/(2|^n)
.= s+(a-s)+(a-s)/(2|^n) by A7,XCMPLX_1:87
.= a+(a-s)/(2|^n);
end;
theorem Th7:
i < j implies N-bound L~Cage(C,j) < N-bound L~Cage(C,i)
proof
assume
A1: i < j;
defpred P[Nat] means i < $1 implies N-bound L~Cage(C,$1) <
N-bound L~Cage(C,i);
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A3: P[n];
set j = n + 1, a = N-bound C, s = S-bound C;
A4: a+(a-s)/(2|^j) - (a+(a-s)/(2|^n)) = 0 + (a-s)/(2|^j) - (a-s)/(2|^n)
.= (a-s)/(2|^n*2) - (a-s)/(2|^n)/(2/2) by NEWTON:6
.= (a-s)/(2|^n*2) - (a-s)*2/(2|^n*2) by XCMPLX_1:84
.= (a-s - (2*a-2*s))/(2|^n*2) by XCMPLX_1:120
.= (s-a)/(2|^n*2);
2|^n > 0 by NEWTON:83;
then
A5: 2|^n*2 > 0 * 2 by XREAL_1:68;
A6: N-bound L~Cage(C,n) = a+(a-s)/(2|^n) & N-bound L~Cage(C,j) = a+(a-s)/(
2|^j) by Th6;
s - a < 0 by SPRECT_1:32,XREAL_1:49;
then 0 > a+(a-s)/(2|^j) - (a+(a-s)/(2|^n)) by A5,A4,XREAL_1:141;
then
A7: N-bound L~Cage(C,n+1) < N-bound L~Cage(C,n) by A6,XREAL_1:48;
assume i < n+1;
then i <= n by NAT_1:13;
hence thesis by A3,A7,XXREAL_0:1,2;
end;
A8: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A8,A2);
hence thesis by A1;
end;
registration
let C be connected compact non vertical non horizontal Subset of TOP-REAL 2,
n be Nat;
cluster Cl RightComp Cage(C,n) -> compact;
coherence by GOBRD14:32;
end;
theorem Th8:
N-min C in RightComp Cage(C,n)
proof
set f = Cage(C,n), G = Gauge(C,n);
consider k being Nat such that
A1: 1 <= k and
A2: k+1 <= len G and
A3: f/.1 = G*(k,width G) & f/.2 = G*(k+1,width G) and
A4: N-min C in cell(G,k,width G-'1) and
N-min C <> G*(k,width G-'1) by JORDAN9:def 1;
A5: len G = width G by JORDAN8:def 1;
A6: 1 <= k+1 by NAT_1:11;
then
A7: 1 <= len G by A2,XXREAL_0:2;
then
A8: [k+1,len G] in Indices G by A2,A5,A6,MATRIX_0:30;
L~f <> {};
then
A9: f is_sequence_on G & 1+1 <= len f by GOBRD14:2,JORDAN9:def 1;
then right_cell(f,1,G) is closed by GOBRD13:30;
then Fr right_cell(f,1,G) = right_cell(f,1,G) \ Int right_cell(f,1,G) by
TOPS_1:43;
then
A10: Fr right_cell(f,1,G) \/ Int right_cell(f,1,G) = right_cell(f,1,G) by
TOPS_1:16,XBOOLE_1:45;
A11: k < len G by A2,NAT_1:13;
then [k,len G] in Indices G by A1,A5,A7,MATRIX_0:30;
then
A12: cell(G,k,len G-'1) = right_cell(f,1,G) by A3,A9,A5,A8,GOBRD13:24;
A13: Int right_cell(f,1) c= RightComp f by GOBOARD9:def 2;
Int right_cell(f,1,G) c= Int right_cell(f,1) by A9,GOBRD13:33,TOPS_1:19;
then
A14: Int cell(G,k,len G-'1) c= RightComp f by A12,A13;
RightComp f misses L~f by SPRECT_3:25;
then
A15: RightComp f /\ L~f = {};
A16: Fr cell(G,k,len G-'1) c= RightComp f \/ L~f
proof
let q be object;
assume
A17: q in Fr cell(G,k,len G-'1);
then reconsider s = q as Point of TOP-REAL 2;
4 <= len G by JORDAN8:10;
then 4 - 1 <= len G - 1 by XREAL_1:13;
then 0 <= len G - 1 by XXREAL_0:2;
then
A18: len G-'1 = len G - 1 by XREAL_0:def 2;
A19: len G - 1 < len G - 0 by XREAL_1:15;
then Int cell(G,k,len G-'1) <> {} by A5,A11,A18,GOBOARD9:14;
then consider p being object such that
A20: p in Int cell(G,k,len G-'1) by XBOOLE_0:def 1;
reconsider p as Point of TOP-REAL 2 by A20;
per cases;
suppose
q in L~f;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A21: not q in L~f;
A22: LSeg(p,s) c= (L~f)`
proof
3 <= len G-'1 by GOBRD14:7;
then
A23: 1 <= len G-'1 by XXREAL_0:2;
then
A24: Int cell(G,k,len G-'1) = { |[x,y]| where x, y is Real:
G*(k,1)`1
< x & x < G*(k+1,1)`1 & G*(1,len G-'1)`2 < y & y < G*(1,len G-'1+1)`2 } by A1
,A5,A11,A18,A19,GOBOARD6:26;
A25: cell(G,k,len G-'1) = { |[m,o]| where m, o is Real:
G*(k,1)`1 <= m
& m <= G*(k+1,1)`1 & G*(1,len G-'1)`2 <= o & o <= G*(1,len G-'1+1)`2 } by A1,A5
,A11,A18,A19,A23,GOBRD11:32;
Fr cell(G,k,len G-'1) c= cell(G,k,len G-'1) by A9,A12,GOBRD13:30
,TOPS_1:35;
then q in cell(G,k,len G-'1) by A17;
then consider m, o being Real such that
A26: s = |[m,o]| and
A27: G*(k,1)`1 <= m and
A28: m <= G*(k+1,1)`1 and
A29: G*(1,len G-'1)`2 <= o and
A30: o <= G*(1,len G-'1+1)`2 by A25;
A31: s`2 = o by A26,EUCLID:52;
consider x, y being Real such that
A32: p = |[x,y]| and
A33: G*(k,1)`1 < x and
A34: x < G*(k+1,1)`1 and
A35: G*(1,len G-'1)`2 < y and
A36: y < G*(1,len G-'1+1)`2 by A20,A24;
A37: p`1 = x by A32,EUCLID:52;
let a be object;
assume
A38: a in LSeg(p,s);
then reconsider b = a as Point of TOP-REAL 2;
A39: b = |[b`1,b`2]| by EUCLID:53;
A40: p`2 = y by A32,EUCLID:52;
A41: s`1 = m by A26,EUCLID:52;
now
per cases;
case
b = s;
hence thesis by A21,SUBSET_1:29;
end;
case
A42: b <> s;
now
per cases by XXREAL_0:1;
case
A43: s`1 < p`1 & s`2 < p`2;
then s`2 < b`2 by A38,A42,TOPREAL6:30;
then
A44: G*(1,len G-'1)`2 < b`2 by A29,A31,XXREAL_0:2;
b`1 <= p`1 by A38,A43,TOPREAL6:29;
then
A45: b`1 < G*(k+1,1)`1 by A34,A37,XXREAL_0:2;
b`2 <= p`2 by A38,A43,TOPREAL6:30;
then
A46: b`2 < G*(1,len G-'1+1)`2 by A36,A40,XXREAL_0:2;
s`1 < b`1 by A38,A42,A43,TOPREAL6:29;
then G*(k,1)`1 < b`1 by A27,A41,XXREAL_0:2;
hence b in Int cell(G,k,len G-'1) by A24,A39,A45,A44,A46;
end;
case
A47: s`1 < p`1 & s`2 > p`2;
then b`2 < s`2 by A38,A42,TOPREAL6:30;
then
A48: b`2 < G*(1,len G-'1+1)`2 by A30,A31,XXREAL_0:2;
b`1 <= p`1 by A38,A47,TOPREAL6:29;
then
A49: b`1 < G*(k+1,1)`1 by A34,A37,XXREAL_0:2;
p`2 <= b`2 by A38,A47,TOPREAL6:30;
then
A50: G*(1,len G-'1)`2 < b`2 by A35,A40,XXREAL_0:2;
s`1 < b`1 by A38,A42,A47,TOPREAL6:29;
then G*(k,1)`1 < b`1 by A27,A41,XXREAL_0:2;
hence b in Int cell(G,k,len G-'1) by A24,A39,A49,A50,A48;
end;
case
A51: s`1 < p`1 & s`2 = p`2;
then b`1 <= p`1 by A38,TOPREAL6:29;
then
A52: b`1 < G*(k+1,1)`1 by A34,A37,XXREAL_0:2;
s`1 < b`1 by A38,A42,A51,TOPREAL6:29;
then
A53: G*(k,1)`1 < b`1 by A27,A41,XXREAL_0:2;
p`2 = b`2 by A38,A51,GOBOARD7:6;
hence b in Int cell(G,k,len G-'1) by A24,A39,A35,A36,A40,A53
,A52;
end;
case
A54: s`1 > p`1 & s`2 < p`2;
then s`2 < b`2 by A38,A42,TOPREAL6:30;
then
A55: G*(1,len G-'1)`2 < b`2 by A29,A31,XXREAL_0:2;
b`1 >= p`1 by A38,A54,TOPREAL6:29;
then
A56: G*(k,1)`1 < b`1 by A33,A37,XXREAL_0:2;
b`2 <= p`2 by A38,A54,TOPREAL6:30;
then
A57: b`2 < G*(1,len G-'1+1)`2 by A36,A40,XXREAL_0:2;
s`1 > b`1 by A38,A42,A54,TOPREAL6:29;
then b`1 < G*(k+1,1)`1 by A28,A41,XXREAL_0:2;
hence b in Int cell(G,k,len G-'1) by A24,A39,A56,A55,A57;
end;
case
A58: s`1 > p`1 & s`2 > p`2;
then s`2 > b`2 by A38,A42,TOPREAL6:30;
then
A59: b`2 < G*(1,len G-'1+1)`2 by A30,A31,XXREAL_0:2;
b`1 >= p`1 by A38,A58,TOPREAL6:29;
then
A60: G*(k,1)`1 < b`1 by A33,A37,XXREAL_0:2;
b`2 >= p`2 by A38,A58,TOPREAL6:30;
then
A61: G*(1,len G-'1)`2 < b`2 by A35,A40,XXREAL_0:2;
s`1 > b`1 by A38,A42,A58,TOPREAL6:29;
then b`1 < G*(k+1,1)`1 by A28,A41,XXREAL_0:2;
hence b in Int cell(G,k,len G-'1) by A24,A39,A60,A61,A59;
end;
case
A62: s`1 > p`1 & s`2 = p`2;
then b`1 >= p`1 by A38,TOPREAL6:29;
then
A63: G*(k,1)`1 < b`1 by A33,A37,XXREAL_0:2;
s`1 > b`1 by A38,A42,A62,TOPREAL6:29;
then
A64: b`1 < G*(k+1,1)`1 by A28,A41,XXREAL_0:2;
b`2 = p`2 by A38,A62,GOBOARD7:6;
hence b in Int cell(G,k,len G-'1) by A24,A39,A35,A36,A40,A63
,A64;
end;
case
A65: s`1 = p`1 & s`2 > p`2;
then b`2 >= p`2 by A38,TOPREAL6:30;
then
A66: G*(1,len G-'1)`2 < b`2 by A35,A40,XXREAL_0:2;
s`2 > b`2 by A38,A42,A65,TOPREAL6:30;
then
A67: b`2 < G*(1,len G-'1+1)`2 by A30,A31,XXREAL_0:2;
b`1 = p`1 by A38,A65,GOBOARD7:5;
hence b in Int cell(G,k,len G-'1) by A24,A39,A33,A34,A37,A66
,A67;
end;
case
A68: s`1 = p`1 & s`2 < p`2;
then b`2 <= p`2 by A38,TOPREAL6:30;
then
A69: b`2 < G*(1,len G-'1+1)`2 by A36,A40,XXREAL_0:2;
s`2 < b`2 by A38,A42,A68,TOPREAL6:30;
then
A70: G*(1,len G-'1)`2 < b`2 by A29,A31,XXREAL_0:2;
b`1 = p`1 by A38,A68,GOBOARD7:5;
hence b in Int cell(G,k,len G-'1) by A24,A39,A33,A34,A37,A70
,A69;
end;
case
s`1 = p`1 & s`2 = p`2;
then p = s by TOPREAL3:6;
then LSeg(p,s) = {p} by RLTOPSP1:70;
hence b in Int cell(G,k,len G-'1) by A20,A38,TARSKI:def 1;
end;
end;
then not b in L~f by A15,A14,XBOOLE_0:def 4;
hence thesis by SUBSET_1:29;
end;
end;
hence thesis;
end;
A71: s in LSeg(p,s) by RLTOPSP1:68;
now
take a = p;
thus a in {p} & a in LSeg(p,s) by RLTOPSP1:68,TARSKI:def 1;
end;
then
A72: {p} meets LSeg(p,s) by XBOOLE_0:3;
RightComp f is_a_component_of (L~f)` & {p} c= RightComp f by A14,A20,
GOBOARD9:def 2,ZFMISC_1:31;
then LSeg(p,s) c= RightComp f by A22,A72,GOBOARD9:4;
hence thesis by A71,XBOOLE_0:def 3;
end;
end;
C misses L~f by Th5;
then N-min C in C & C /\ L~f = {} by SPRECT_1:11;
then
A73: not N-min C in L~f by XBOOLE_0:def 4;
RightComp f c= RightComp f \/ L~f by XBOOLE_1:7;
then Int cell(G,k,len G-'1) c= RightComp f \/ L~f by A14;
then right_cell(f,1,G) c= RightComp f \/ L~f by A12,A16,A10,XBOOLE_1:8;
hence thesis by A73,A4,A5,A12,XBOOLE_0:def 3;
end;
theorem Th9:
C meets RightComp Cage (C,n)
proof
N-min C in C & N-min C in RightComp Cage(C,n) by Th8,SPRECT_1:11;
then C /\ RightComp Cage (C,n) <> {} by XBOOLE_0:def 4;
hence thesis;
end;
theorem Th10:
C misses LeftComp Cage(C,n)
proof
set f = Cage(C,n);
assume
A1: C meets LeftComp f;
RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
then
A2: ex R being Subset of (TOP-REAL 2)|(L~f)` st R = RightComp f & R
is a_component by CONNSP_1:def 6;
C misses L~f by Th5;
then
A3: C /\ L~f = {};
C c= the carrier of (TOP-REAL 2)|(L~f)`
proof
let c be object;
assume
A4: c in C;
then not c in L~f by A3,XBOOLE_0:def 4;
then c in (L~f)` by A4,SUBSET_1:29;
hence thesis by PRE_TOPC:8;
end;
then reconsider C1 = C as Subset of (TOP-REAL 2)|(L~f)`;
LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
then
A5: ex L being Subset of (TOP-REAL 2)|(L~f)` st L = LeftComp f & L
is a_component by CONNSP_1:def 6;
C meets RightComp f & C1 is connected by Th9,CONNSP_1:23;
hence contradiction by A1,A5,A2,JORDAN2C:92,SPRECT_4:6;
end;
theorem Th11:
C c= RightComp Cage(C,n)
proof
set f = Cage(C,n);
let c be object;
assume
A1: c in C;
C misses L~f by Th5;
then C /\ L~f = {};
then
A2: not c in L~f by A1,XBOOLE_0:def 4;
C misses LeftComp f by Th10;
then C /\ LeftComp f = {};
then not c in LeftComp f by A1,XBOOLE_0:def 4;
hence thesis by A1,A2,GOBRD14:18;
end;
theorem Th12:
C c= BDD L~Cage(C,n)
proof
C c= RightComp Cage(C,n) & RightComp Cage(C,n) c= BDD L~Cage(C,n) by Th11,
GOBRD14:35,JORDAN2C:22;
hence thesis;
end;
theorem Th13:
UBD L~Cage(C,n) c= UBD C
proof
set f = Cage(C,n);
A1: UBD C = union {B where B is Subset of TOP-REAL 2: B
is_outside_component_of C} by JORDAN2C:def 5;
let x be object;
A2: UBD L~f = union {B where B is Subset of TOP-REAL 2: B
is_outside_component_of L~f} by JORDAN2C:def 5;
assume x in UBD L~f;
then consider L being set such that
A3: x in L and
A4: L in {B where B is Subset of TOP-REAL 2: B is_outside_component_of
L~f} by A2,TARSKI:def 4;
consider B being Subset of TOP-REAL 2 such that
A5: L = B and
A6: B is_outside_component_of L~f by A4;
reconsider B1 = B as Subset of Euclid 2 by TOPREAL3:8;
A7: B1 misses RightComp f by A6,GOBRD14:35,JORDAN2C:118;
then
A8: B1 /\ RightComp f = {};
the carrier of (TOP-REAL 2)|C` = C` by PRE_TOPC:8;
then reconsider P1 = Component_of (Down(B,C`)) as Subset of TOP-REAL 2 by
XBOOLE_1:1;
B is_a_component_of (L~f)` by A6,JORDAN2C:def 3;
then consider B2 being Subset of (TOP-REAL 2)|(L~f)` such that
A9: B2 = B and
A10: B2 is a_component by CONNSP_1:def 6;
B2 is connected by A10,CONNSP_1:def 5;
then
A11: B is connected by A9,CONNSP_1:23;
A12: C c= RightComp f by Th11;
then not x in C by A3,A5,A8,XBOOLE_0:def 4;
then x in C` by A3,A5,XBOOLE_0:def 5;
then
A13: x in B /\ C` by A3,A5,XBOOLE_0:def 4;
not B is bounded by A6,JORDAN2C:def 3;
then
A14: not B1 is bounded by JORDAN2C:11;
B1 misses C by A7,Th11,XBOOLE_1:63;
then P1 is_outside_component_of C by A11,A14,JORDAN2C:63;
then
A15: P1 in {W where W is Subset of TOP-REAL 2: W is_outside_component_of C };
B c= C`
proof
let a be object;
assume
A16: a in B;
then not a in C by A12,A8,XBOOLE_0:def 4;
hence thesis by A16,XBOOLE_0:def 5;
end;
then Down(B,C`) = B by XBOOLE_1:28;
then Down(B,C`) c= Component_of Down(B,C`) by A11,CONNSP_1:46,CONNSP_3:1;
hence thesis by A1,A13,A15,TARSKI:def 4;
end;
definition
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
func UBD-Family C -> set equals
the set of all UBD L~Cage(C,n) where n is Nat ;
coherence;
func BDD-Family C -> set equals
the set of all Cl BDD L~Cage(C,n) where n is Nat ;
coherence;
end;
definition
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
redefine func UBD-Family C -> Subset-Family of TOP-REAL 2; :: redefines UBD-Family (JORDAN10, definition)
coherence
proof
the set of all UBD L~Cage(C,i) where i is Nat c=
bool the carrier of TOP-REAL 2
proof
let x be object;
assume x in the set of all UBD L~Cage(C,i) where i is Nat ;
then ex i being Nat st x = UBD L~Cage(C,i);
hence thesis;
end;
hence thesis;
end;
redefine func BDD-Family C -> Subset-Family of TOP-REAL 2; :: redefines BDD-Family (JORDAN10, definition)
coherence
proof
the set of all Cl BDD L~Cage(C,i) where i is Nat
c= bool the carrier of TOP-REAL 2
proof
let x be object;
assume x in the set of all Cl BDD L~Cage(C,i) where i is Nat ;
then ex i being Nat st x = Cl BDD L~Cage(C,i);
hence thesis;
end;
hence thesis;
end;
end;
registration
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
cluster UBD-Family C -> non empty;
coherence
proof
UBD L~Cage(C,0) in UBD-Family C;
hence thesis;
end;
cluster BDD-Family C -> non empty;
coherence
proof
Cl BDD L~Cage(C,0) in BDD-Family C;
hence thesis;
end;
end;
theorem Th14:
union UBD-Family C = UBD C
proof
A1: UBD L~Cage(C,0) c= UBD C & UBD L~Cage(C,0) = LeftComp Cage(C,0) by Th13,
GOBRD14:36;
for X being set st X in UBD-Family C holds X c= UBD C
proof
let X be set;
assume X in UBD-Family C;
then ex n st X = UBD L~Cage(C,n);
hence thesis by Th13;
end;
hence union UBD-Family C c= UBD C by ZFMISC_1:76;
let x be object such that
A2: x in UBD C;
UBD C = union {B where B is Subset of TOP-REAL 2: B
is_outside_component_of C} by JORDAN2C:def 5;
then consider A being set such that
A3: x in A and
A4: A in {B where B is Subset of TOP-REAL 2: B is_outside_component_of C
} by A2,TARSKI:def 4;
ex B being Subset of TOP-REAL 2 st A = B & B is_outside_component_of C by A4;
then reconsider p = x as Point of TOP-REAL 2 by A3;
consider q being Point of TOP-REAL 2 such that
A5: q`2 > N-bound L~Cage(C,0) and
A6: p <> q by TOPREAL6:33;
Cage(C,0)/.1 = N-min L~Cage(C,0) by JORDAN9:32;
then q in LeftComp Cage(C,0) by A5,JORDAN2C:113;
then consider P such that
A7: P is_S-P_arc_joining p,q and
A8: P c= UBD C by A2,A6,A1,TOPREAL4:29;
consider f being FinSequence of TOP-REAL 2 such that
A9: f is being_S-Seq and
A10: P = L~f and
A11: p = f/.1 and
q = f/.len f by A7,TOPREAL4:def 1;
reconsider f as being_S-Seq FinSequence of TOP-REAL 2 by A9;
2 <= len f by NAT_D:60;
then
A12: x in P by A10,A11,JORDAN3:1;
L~f is non empty & the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2
by EUCLID:def 8;
then reconsider
P1 = P, C1 = C as non empty compact Subset of TopSpaceMetr Euclid
2 by A10,COMPTS_1:23;
set d = min_dist_min(P1,C1);
UBD C is_outside_component_of C by JORDAN2C:68;
then UBD C is_a_component_of C` by JORDAN2C:def 3;
then C misses UBD C by JORDAN2C:117;
then P misses C by A8,XBOOLE_1:63;
then d > 0 by JGRAPH_1:38;
then d/2 > 0 by XREAL_1:139;
then consider n such that
1 < n and
A13: dist(Gauge(C,n)*(1,1),Gauge(C,n)*(1,2)) < d/2 & dist(Gauge(C,n)*(1,
1),Gauge( C,n)*(2,1)) < d/2 by GOBRD14:11;
set G = Gauge(C,n), g = Cage(C,n);
A14: UBD L~g in UBD-Family C;
A15: now
assume L~g /\ P <> {};
then consider a being object such that
A16: a in L~g /\ P by XBOOLE_0:def 1;
a in L~g by A16,XBOOLE_0:def 4;
then consider i being Nat such that
A17: 1 <= i & i+1 <= len g and
A18: a in LSeg(g,i) by SPPOL_2:13;
right_cell(g,i,G) meets C by A17,JORDAN9:31;
then consider c being object such that
A19: c in right_cell(g,i,G) /\ C by XBOOLE_0:4;
reconsider c as Point of Euclid 2 by A19,TOPREAL3:8;
reconsider a9 = a as Point of Euclid 2 by A16,TOPREAL3:8;
A20: c in C by A19,XBOOLE_0:def 4;
reconsider c9 = c as Point of TOP-REAL 2 by A19;
A21: g is_sequence_on G by JORDAN9:def 1;
then consider i1, j1, i2, j2 being Nat such that
A22: [i1,j1] in Indices G and
A23: g/.i = G*(i1,j1) and
A24: [i2,j2] in Indices G and
A25: g/.(i+1) = G*(i2,j2) and
A26: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
or i1 = i2 & j1 = j2+1 by A17,JORDAN8:3;
left_cell(g,i,G) /\ right_cell(g,i,G) = LSeg(g,i) by A17,A21,GOBRD13:29;
then
A27: a in right_cell(g,i,G) by A18,XBOOLE_0:def 4;
a in P by A16,XBOOLE_0:def 4;
then
A28: dist(a9,c) >= d by A20,WEIERSTR:34;
reconsider A = a as Point of TOP-REAL 2 by A16;
set e = E-bound C, w = W-bound C, p = N-bound C, s = S-bound C;
A29: 4 <= len G by JORDAN8:10;
then
A30: 1 <= len G by XXREAL_0:2;
A31: len G = width G by JORDAN8:def 1;
then
A32: 1 <= width G by A29,XXREAL_0:2;
A33: [1,1] in Indices G by A31,A30,MATRIX_0:30;
A34: c in right_cell(g,i,G) by A19,XBOOLE_0:def 4;
now
per cases by A26;
case
A35: i1 = i2 & j1+1 = j2;
then
A36: i1 < len G by A17,A22,A23,A24,A25,Th1;
then
A37: i1+1 <= len G by NAT_1:13;
A38: 1 <= i1 by A22,MATRIX_0:32;
then 1 <= i1+1 by NAT_1:13;
then
A39: [i1+1,1] in Indices G by A32,A37,MATRIX_0:30;
[i1,1] in Indices G by A32,A38,A36,MATRIX_0:30;
then
A40: dist(G*(i1,1),G*(i1+1,1)) = G*(i1+1,1)`1 - G*(i1,1)`1 & dist(G*(
i1,1),G*(i1+ 1,1)) = (e-w)/2|^n by A39,GOBRD14:5,10;
A41: j1+1 <= width G by A24,A35,MATRIX_0:32;
then
A42: j1 < width G by NAT_1:13;
A43: 1 <= j1 by A22,MATRIX_0:32;
then 1 <= j1+1 by NAT_1:13;
then
A44: [1,j1+1] in Indices G by A30,A41,MATRIX_0:30;
A45: right_cell(g,i,G) = cell(G,i1,j1) by A17,A21,A22,A23,A24,A25,A35,
GOBRD13:22
.= { |[r,t]| where r, t is Real:
G*(i1,1)`1 <= r & r <= G*(i1+1,1
)`1 & G*(1,j1)`2 <= t & t <= G*(1,j1+1)`2 } by A38,A36,A43,A42,GOBRD11:32;
then consider aa, ab being Real such that
A46: a = |[aa,ab]| and
A47: G*(i1,1)`1 <= aa & aa <= G*(i1+1,1)`1 & G*(1,j1)`2 <= ab & ab
<= G*(1 ,j1+1)`2 by A27;
A48: A`1 = aa & A`2 = ab by A46,EUCLID:52;
[1,j1] in Indices G by A30,A43,A42,MATRIX_0:30;
then
A49: dist(G*(1,j1),G*(1,j1+1)) = G*(1,j1+1)`2 - G*(1,j1)`2 & dist(G*(1
,j1),G*(1, j1+1)) = (p-s)/2|^n by A44,GOBRD14:6,9;
consider r, t being Real such that
A50: c = |[r,t]| and
A51: G*(i1,1)`1 <= r & r <= G*(i1+1,1)`1 & G*(1,j1)`2 <= t & t <=
G*(1,j1+ 1)`2 by A34,A45;
c9`1 = r & c9`2 = t by A50,EUCLID:52;
hence dist(A,c9) <= (p-s)/2|^n + (e-w)/2|^n by A51,A47,A48,A49,A40,
TOPREAL6:95;
end;
case
A52: i1+1 = i2 & j1 = j2;
then
A53: i1+1 <= len G by A24,MATRIX_0:32;
then
A54: i1 < len G by NAT_1:13;
A55: 1 <= i1 by A22,MATRIX_0:32;
then 1 <= i1+1 by NAT_1:13;
then
A56: [i1+1,1] in Indices G by A32,A53,MATRIX_0:30;
[i1,1] in Indices G by A32,A55,A54,MATRIX_0:30;
then
A57: dist(G*(i1,1),G*(i1+1,1)) = G*(i1+1,1)`1 - G*(i1,1)`1 & dist(G*(
i1,1),G*(i1+ 1,1)) = (e-w)/2|^n by A56,GOBRD14:5,10;
A58: j2 <= width G by A24,MATRIX_0:32;
j2 > 1 by A17,A22,A23,A24,A25,A52,Th3;
then
A59: j2-1 > 0 by XREAL_1:50;
then
A60: j2-1 = j2-'1 by XREAL_0:def 2;
then
A61: 1 <= j2-'1 by A59,NAT_1:14;
width G - 1 < width G - 0 by XREAL_1:15;
then
A62: j2-'1 < width G by A60,A58,XREAL_1:15;
then
A63: [1,j2-'1] in Indices G by A30,A61,MATRIX_0:30;
A64: right_cell(g,i,G) = cell(G,i1,j2-'1) by A17,A21,A22,A23,A24,A25,A52,
GOBRD13:24
.= { |[r,t]| where r, t is Real:
G*(i1,1)`1 <= r & r <= G*(i1+1,1
)`1 & G*(1,j2-'1)`2 <= t & t <= G*(1,j2-'1+1)`2 } by A55,A54,A61,A62,GOBRD11:32
;
then consider aa, ab being Real such that
A65: a = |[aa,ab]| and
A66: G*(i1,1)`1 <= aa & aa <= G*(i1+1,1)`1 & G*(1,j2-'1)`2 <= ab &
ab <= G *(1,j2-'1+1)`2 by A27;
A67: A`1 = aa & A`2 = ab by A65,EUCLID:52;
1 <= j2-'1+1 by A61,NAT_1:13;
then [1,j2-'1+1] in Indices G by A30,A60,A58,MATRIX_0:30;
then
A68: dist(G*(1,j2-'1),G*(1,j2-'1+1)) = G*(1,j2-'1+1)`2 - G*(1,j2-'1)
`2 & dist(G*( 1,j2-'1),G*(1,j2-'1+1)) = (p-s)/2|^n by A63,GOBRD14:6,9;
consider r, t being Real such that
A69: c = |[r,t]| and
A70: G*(i1,1)`1 <= r & r <= G*(i1+1,1)`1 & G*(1,j2-'1)`2 <= t & t
<= G*(1, j2-'1+1)`2 by A34,A64;
c9`1 = r & c9`2 = t by A69,EUCLID:52;
hence dist(A,c9) <= (p-s)/2|^n + (e-w)/2|^n by A70,A66,A67,A68,A57,
TOPREAL6:95;
end;
case
A71: i1 = i2+1 & j1 = j2;
A72: 1 <= j1+1 by NAT_1:12;
A73: j1 < width G by A17,A22,A23,A24,A25,A71,Th4;
then j1+1 <= width G by NAT_1:13;
then
A74: [1,j1+1] in Indices G by A30,A72,MATRIX_0:30;
A75: 1 <= j1 by A22,MATRIX_0:32;
then [1,j1] in Indices G by A30,A73,MATRIX_0:30;
then
A76: dist(G*(1,j1),G*(1,j1+1)) = G*(1,j1+1)`2 - G*(1,j1)`2 & dist(G*(
1,j1),G*(1, j1+1)) = (p-s)/2|^n by A74,GOBRD14:6,9;
A77: i2+1 <= len G by A22,A71,MATRIX_0:32;
then
A78: i2 < len G by NAT_1:13;
A79: 1 <= i2 by A24,MATRIX_0:32;
then 1 <= i2+1 by NAT_1:13;
then
A80: [i2+1,1] in Indices G by A32,A77,MATRIX_0:30;
A81: right_cell(g,i,G) = cell(G,i2,j1) by A17,A21,A22,A23,A24,A25,A71,
GOBRD13:26
.= { |[r,t]| where r, t is Real:
G*(i2,1)`1 <= r & r <= G*(i2+1,1
)`1 & G*(1,j1)`2 <= t & t <= G*(1,j1+1)`2 } by A79,A78,A75,A73,GOBRD11:32;
then consider aa, ab being Real such that
A82: a = |[aa,ab]| and
A83: G*(i2,1)`1 <= aa & aa <= G*(i2+1,1)`1 & G*(1,j1)`2 <= ab &
ab <= G*(1 ,j1+1)`2 by A27;
A84: A`1 = aa & A`2 = ab by A82,EUCLID:52;
[i2,1] in Indices G by A32,A79,A78,MATRIX_0:30;
then
A85: dist(G*(i2,1),G*(i2+1,1)) = G*(i2+1,1)`1 - G*(i2,1)`1 & dist(G*(
i2,1),G*(i2+ 1,1)) = (e-w)/2|^n by A80,GOBRD14:5,10;
consider r, t being Real such that
A86: c = |[r,t]| and
A87: G*(i2,1)`1 <= r & r <= G*(i2+1,1)`1 & G*(1,j1)`2 <= t & t <=
G*(1,j1+ 1)`2 by A34,A81;
c9`1 = r & c9`2 = t by A86,EUCLID:52;
hence dist(A,c9) <= (p-s)/2|^n + (e-w)/2|^n by A87,A83,A84,A76,A85,
TOPREAL6:95;
end;
case
A88: i1 = i2 & j1 = j2+1;
then
A89: j2+1 <= width G by A22,MATRIX_0:32;
then
A90: j2 < width G by NAT_1:13;
A91: 1 <= j2 by A24,MATRIX_0:32;
then 1 <= j2+1 by NAT_1:13;
then
A92: [1,j2+1] in Indices G by A30,A89,MATRIX_0:30;
[1,j2] in Indices G by A30,A91,A90,MATRIX_0:30;
then
A93: dist(G*(1,j2),G*(1,j2+1)) = G*(1,j2+1)`2 - G*(1,j2)`2 & dist(G*(
1,j2),G*(1, j2+1)) = (p-s)/2|^n by A92,GOBRD14:6,9;
A94: i1 <= len G by A22,MATRIX_0:32;
i1 > 1 by A17,A22,A23,A24,A25,A88,Th2;
then
A95: i1-1 > 0 by XREAL_1:50;
then
A96: i1-1 = i1-'1 by XREAL_0:def 2;
then
A97: 1 <= i1-'1 by A95,NAT_1:14;
len G - 1 < len G - 0 by XREAL_1:15;
then
A98: i1-'1 < len G by A96,A94,XREAL_1:15;
then
A99: [i1-'1,1] in Indices G by A32,A97,MATRIX_0:30;
A100: right_cell(g,i,G) = cell(G,i1-'1,j2) by A17,A21,A22,A23,A24,A25,A88,
GOBRD13:28
.= { |[r,t]| where r, t is Real:
G*(i1-'1,1)`1 <= r & r <= G*(i1
-'1+1,1)`1 & G*(1,j2)`2 <= t & t <= G*(1,j2+1)`2 } by A97,A98,A91,A90,
GOBRD11:32;
then consider aa, ab being Real such that
A101: a = |[aa,ab]| and
A102: G*(i1-'1,1)`1 <= aa & aa <= G*(i1-'1+1,1)`1 & G*(1,j2)`2 <=
ab & ab <= G*(1,j2+1)`2 by A27;
A103: A`1 = aa & A`2 = ab by A101,EUCLID:52;
1 <= i1-'1+1 by A97,NAT_1:13;
then [i1-'1+1,1] in Indices G by A32,A96,A94,MATRIX_0:30;
then
A104: dist(G*(i1-'1,1),G*(i1-'1+1,1)) = G*(i1-'1+1,1)`1 - G*(i1 -'1,1)
`1 & dist(G* (i1-'1,1),G* (i1-'1+1,1)) = (e-w)/2|^n by A99,GOBRD14:5,10;
consider r, t being Real such that
A105: c = |[r,t]| and
A106: G*(i1-'1,1)`1 <= r & r <= G*(i1-'1+1,1)`1 & G*(1,j2)`2 <= t
& t <= G* (1,j2+1)`2 by A34,A100;
c9`1 = r & c9`2 = t by A105,EUCLID:52;
hence dist(A,c9) <= (p-s)/2|^n + (e-w)/2|^n by A106,A102,A103,A93,A104,
TOPREAL6:95;
end;
end;
then
A107: dist(a9,c) <= (p-s)/2|^n + (e-w)/2|^n by TOPREAL6:def 1;
1+1 <= len G by A29,XXREAL_0:2;
then [1+1,1] in Indices G by A32,MATRIX_0:30;
then
A108: dist(G*(1,1),G*(1+1,1)) = (e-w)/2|^n by A33,GOBRD14:10;
1+1 <= width G by A31,A29,XXREAL_0:2;
then [1,1+1] in Indices G by A30,MATRIX_0:30;
then dist(G*(1,1),G*(1,1+1)) = (p-s)/2|^n by A33,GOBRD14:9;
then (p-s)/2|^n + (e-w)/2|^n < d/2 + d/2 by A13,A108,XREAL_1:8;
hence contradiction by A28,A107,XXREAL_0:2;
end;
A109: P c= (L~g)`
proof
let a be object;
assume
A110: a in P;
then not a in L~g by A15,XBOOLE_0:def 4;
hence thesis by A110,SUBSET_1:29;
end;
0 < n or 0 = n;
then N-bound L~(Cage(C,0)) >= N-bound L~g by Th7;
then g/.1 = N-min L~g & q`2 > N-bound L~g by A5,JORDAN9:32,XXREAL_0:2;
then q in LeftComp g by JORDAN2C:113;
then q in UBD L~g by GOBRD14:36;
then
A111: {q} c= UBD L~g by ZFMISC_1:31;
A112: P is_an_arc_of p,q by A7,TOPREAL4:2;
now
take a = q;
thus a in {q} & a in P by A112,TARSKI:def 1,TOPREAL1:1;
end;
then
A113: {q} meets P by XBOOLE_0:3;
UBD L~g is_outside_component_of L~g by JORDAN2C:68;
then ex E being Subset of (TOP-REAL 2)|(L~g)` st E = UBD L~g & E
is a_component & not E is bounded Subset of Euclid 2 by JORDAN2C:14;
then UBD L~g is_a_component_of (L~g)` by CONNSP_1:def 6;
then P c= UBD L~g by A109,A112,A111,A113,GOBOARD9:4,JORDAN6:10;
hence thesis by A12,A14,TARSKI:def 4;
end;
theorem Th15:
C c= meet BDD-Family C
proof
for Z being set st Z in BDD-Family C holds C c= Z
proof
let Z be set;
assume Z in BDD-Family C;
then consider k being Nat such that
A1: Z = Cl BDD L~Cage(C,k);
C c= BDD L~Cage(C,k) & BDD L~Cage(C,k) c= Cl BDD L~Cage(C,k) by Th12,
PRE_TOPC:18;
hence thesis by A1;
end;
hence thesis by SETFAM_1:5;
end;
theorem Th16:
BDD C misses LeftComp Cage(C,n)
proof
set f = Cage(C,n);
assume BDD C /\ LeftComp f <> {};
then consider x being Point of TOP-REAL 2 such that
A1: x in BDD C /\ LeftComp f by SUBSET_1:4;
BDD C misses UBD C by JORDAN2C:24;
then
A2: BDD C /\ UBD C = {};
x in BDD C by A1,XBOOLE_0:def 4;
then not x in UBD C by A2,XBOOLE_0:def 4;
then
A3: not x in union UBD-Family C by Th14;
A4: x in LeftComp f by A1,XBOOLE_0:def 4;
UBD L~f in the set of all UBD L~Cage(C,k) where k is Nat ;
then not x in UBD L~f by A3,TARSKI:def 4;
hence contradiction by A4,GOBRD14:36;
end;
theorem Th17:
BDD C c= RightComp Cage(C,n)
proof
set f = Cage(C,n);
let x be object;
LeftComp f is_outside_component_of L~f by GOBRD14:34;
then
A1: UBD L~f = union {E where E is Subset of TOP-REAL 2: E
is_outside_component_of L~f} & LeftComp f in {E where E is Subset of TOP-REAL 2
: E is_outside_component_of L~f} by JORDAN2C:def 5;
assume
A2: x in BDD C;
A3: now
assume x in Cl LeftComp f;
then BDD C meets LeftComp f by A2,PRE_TOPC:def 7;
hence contradiction by Th16;
end;
BDD C misses UBD C by JORDAN2C:24;
then BDD C /\ UBD C = {};
then not x in UBD C by A2,XBOOLE_0:def 4;
then
A4: not x in union UBD-Family C by Th14;
UBD L~f in the set of all UBD L~Cage(C,k) where k is Nat ;
then not x in UBD L~Cage(C,n) by A4,TARSKI:def 4;
then
A5: not x in LeftComp f by A1,TARSKI:def 4;
L~f = (Cl LeftComp f) \ LeftComp f by GOBRD14:20;
then not x in L~f by A3,XBOOLE_0:def 5;
hence thesis by A2,A5,GOBRD14:18;
end;
theorem Th18:
P is_inside_component_of C implies P misses L~Cage(C,n)
proof
set f = Cage(C,n);
assume P is_inside_component_of C;
then
A1: P c= BDD C by JORDAN2C:22;
assume P /\ L~f <> {};
then consider x being Point of TOP-REAL 2 such that
A2: x in P /\ L~f by SUBSET_1:4;
x in P by A2,XBOOLE_0:def 4;
then
A3: x in BDD C by A1;
A4: BDD C c= RightComp f by Th17;
x in L~f by A2,XBOOLE_0:def 4;
hence contradiction by A3,A4,GOBRD14:18;
end;
theorem Th19:
BDD C misses L~Cage(C,n)
proof
assume not thesis;
then consider x being object such that
A1: x in BDD C /\ L~Cage(C,n) by XBOOLE_0:4;
A2: x in L~Cage(C,n) by A1,XBOOLE_0:def 4;
BDD C = union {B where B is Subset of TOP-REAL 2: B
is_inside_component_of C} & x in BDD C by A1,JORDAN2C:def 4,XBOOLE_0:def 4;
then consider Z being set such that
A3: x in Z and
A4: Z in {B where B is Subset of TOP-REAL 2: B is_inside_component_of C}
by TARSKI:def 4;
consider B being Subset of TOP-REAL 2 such that
A5: Z = B and
A6: B is_inside_component_of C by A4;
B misses L~Cage(C,n) by A6,Th18;
then B /\ L~Cage(C,n) = {};
hence thesis by A3,A5,A2,XBOOLE_0:def 4;
end;
theorem Th20:
COMPLEMENT UBD-Family C = BDD-Family C
proof
for P being Subset of TOP-REAL 2 holds P in BDD-Family C iff P` in
UBD-Family C
proof
let P being Subset of TOP-REAL 2;
thus P in BDD-Family C implies P` in UBD-Family C
proof
assume P in BDD-Family C;
then consider k such that
A1: P = Cl BDD L~Cage(C,k);
P = Cl RightComp Cage(C,k) by A1,GOBRD14:37;
then
A2: P = (RightComp Cage(C,k)) \/ L~Cage(C,k) by GOBRD14:21;
P` /\ (LeftComp Cage(C,k))` = (P \/ LeftComp Cage(C,k))` by XBOOLE_1:53
.= ([#]the carrier of TOP-REAL 2)` by A2,GOBRD14:15
.= {}the carrier of TOP-REAL 2 by XBOOLE_1:37;
then
A3: P` misses (LeftComp Cage(C,k))`;
L~Cage(C,k) misses LeftComp Cage(C,k) & RightComp Cage(C,k) misses
LeftComp Cage(C,k) by GOBRD14:14,SPRECT_3:26;
then P misses LeftComp Cage(C,k) by A2,XBOOLE_1:70;
then P` = LeftComp Cage(C,k) by A3,SUBSET_1:25;
then P` = UBD L~Cage(C,k) by GOBRD14:36;
hence thesis;
end;
assume P` in UBD-Family C;
then consider k such that
A4: P` = UBD L~Cage(C,k);
A5: P` = LeftComp Cage(C,k) by A4,GOBRD14:36;
then P` misses RightComp Cage(C,k) & P` misses L~Cage(C,k) by GOBRD14:14
,SPRECT_3:26;
then P` misses (RightComp Cage(C,k)) \/ L~Cage(C,k) by XBOOLE_1:70;
then
A6: P` misses Cl RightComp Cage(C,k) by GOBRD14:21;
P`` /\ (Cl RightComp Cage(C,k))` = (P` \/ (Cl RightComp Cage(C,k)))`
by XBOOLE_1:53
.= (P` \/ ((RightComp Cage(C,k)) \/ L~Cage(C,k)))` by GOBRD14:21
.= ([#]the carrier of TOP-REAL 2)` by A5,GOBRD14:15
.= {}the carrier of TOP-REAL 2 by XBOOLE_1:37;
then P`` misses (Cl RightComp Cage(C,k))`;
then P`` = Cl RightComp Cage(C,k) by A6,SUBSET_1:25;
then P = Cl BDD L~Cage(C,k) by GOBRD14:37;
hence thesis;
end;
hence thesis by SETFAM_1:def 7;
end;
theorem
meet BDD-Family C = C \/ BDD C
proof
thus meet BDD-Family C c= C \/ BDD C
proof
let x be object;
assume
A1: x in meet BDD-Family C;
COMPLEMENT UBD-Family C = BDD-Family C by Th20;
then
([#] the carrier of TOP-REAL 2) \ union UBD-Family C = meet BDD-Family
C by SETFAM_1:33;
then not x in union UBD-Family C by A1,XBOOLE_0:def 5;
then
A2: not x in UBD C by Th14;
per cases;
suppose
A3: not x in C;
A4: BDD C \/ UBD C = C` by JORDAN2C:27;
x in C` by A1,A3,SUBSET_1:29;
then x in BDD C by A2,A4,XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x in C;
hence thesis by XBOOLE_0:def 3;
end;
end;
(BDD C) misses (UBD C) by JORDAN2C:24;
then
A5: (BDD C) /\ (UBD C) = {};
A6: BDD C c= meet BDD-Family C
proof
let x be object;
assume
A7: x in BDD C;
then not x in UBD C by A5,XBOOLE_0:def 4;
then
A8: not x in union UBD-Family C by Th14;
for Y being set st Y in BDD-Family C holds x in Y
proof
let Y be set;
assume Y in BDD-Family C;
then consider n such that
A9: Y = Cl BDD L~Cage(C,n) and
not contradiction;
LeftComp Cage(C,n) is_outside_component_of L~Cage(C,n) by GOBRD14:34;
then
A10: LeftComp Cage(C,n) in {B where B is Subset of TOP-REAL 2: B
is_outside_component_of L~Cage(C,n)};
BDD C misses L~Cage(C,n) by Th19;
then BDD C /\ L~Cage(C,n) = {};
then
A11: not x in L~Cage(C,n) by A7,XBOOLE_0:def 4;
RightComp Cage(C,n) is_inside_component_of L~Cage(C,n) by GOBRD14:35;
then
A12: RightComp Cage(C,n) in {B where B is Subset of TOP-REAL 2: B
is_inside_component_of L~Cage(C,n)};
UBD L~Cage(C,n) in UBD-Family C;
then UBD L~Cage(C,n) = union{B where B is Subset of TOP-REAL 2: B
is_outside_component_of L~Cage(C,n)} & not x in UBD L~Cage(C,n) by A8,
JORDAN2C:def 5,TARSKI:def 4;
then not x in LeftComp Cage(C,n) by A10,TARSKI:def 4;
then BDD L~Cage(C,n) = union{B where B is Subset of TOP-REAL 2: B
is_inside_component_of L~Cage(C,n)} & x in RightComp Cage(C,n) by A7,A11,
GOBRD14:18,JORDAN2C:def 4;
then
A13: x in BDD L~Cage(C,n) by A12,TARSKI:def 4;
BDD L~Cage(C,n) c= Cl BDD L~Cage(C,n) by PRE_TOPC:18;
hence thesis by A9,A13;
end;
hence thesis by SETFAM_1:def 1;
end;
C c= meet BDD-Family C by Th15;
hence thesis by A6,XBOOLE_1:8;
end;