Copyright (c) 1999 Association of Mizar Users
environ
vocabulary RELAT_2, COMPTS_1, SPPOL_1, EUCLID, TOPREAL1, FINSEQ_1, JORDAN9,
MATRIX_1, JORDAN8, GOBOARD1, GOBOARD5, TREES_1, BOOLE, ARYTM_1, TARSKI,
PSCOMP_1, ARYTM_3, GROUP_1, MCART_1, PRE_TOPC, GOBOARD9, TOPS_1,
SUBSET_1, CONNSP_1, RELAT_1, JORDAN2C, LATTICES, CONNSP_3, SETFAM_1,
TOPREAL4, PCOMPS_1, WEIERSTR, METRIC_1, JORDAN10, FINSEQ_4;
notation TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, XREAL_0, REAL_1, NAT_1,
BINARITH, STRUCT_0, METRIC_1, TBSP_1, FINSEQ_1, NEWTON, FINSEQ_4,
WEIERSTR, PRE_TOPC, TOPS_1, CONNSP_1, CONNSP_3, COMPTS_1, PCOMPS_1,
MATRIX_1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD5, TOPREAL4, PSCOMP_1,
GOBOARD9, SPPOL_1, JORDAN2C, JORDAN8, GOBRD13, GOBRD14, JORDAN9;
constructors BINARITH, CARD_4, CONNSP_1, CONNSP_3, FINSEQ_4, GOBOARD9,
GOBRD13, GOBRD14, JORDAN2C, JORDAN8, JORDAN9, PSCOMP_1, REAL_1, REALSET1,
TBSP_1, TOPREAL4, TOPS_1, WEIERSTR, JORDAN1;
clusters XREAL_0, BORSUK_2, EUCLID, GOBRD14, JORDAN8, PCOMPS_1, PRE_TOPC,
PSCOMP_1, RELSET_1, SPPOL_2, SPRECT_1, STRUCT_0, TOPREAL6, SUBSET_1,
FINSEQ_1, ARYTM_3, SPRECT_4, JORDAN2C, MEMBERED;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0;
theorems AXIOMS, BINARITH, CONNSP_1, CONNSP_3, EUCLID, GOBOARD5, GOBOARD6,
GOBOARD7, GOBOARD9, GOBRD11, GOBRD13, GOBRD14, HEINE, JGRAPH_1, JORDAN1,
JORDAN2C, JORDAN3, JORDAN6, JORDAN8, JORDAN9, NEWTON, NAT_1, PRE_TOPC,
PSCOMP_1, REAL_1, REAL_2, RLVECT_1, SETFAM_1, SPPOL_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, SQUARE_1,
XCMPLX_0, XCMPLX_1;
schemes NAT_1;
begin :: Properties of the external approximation of Jordan's curve
definition
cluster connected compact non vertical non horizontal 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);
A4: i <= len G by A2,GOBOARD5:1;
assume i >= len G;
then A5: i = len G by A4,REAL_1:def 5;
f is_sequence_on G by JORDAN9:def 1;
then A6: right_cell(f,k,G) = cell(G,i,j) by A1,A2,A3,GOBRD13:23;
len G = width G by JORDAN8:def 1;
then j <= len G by A2,GOBOARD5:1;
then cell(G,len G,j) misses C by JORDAN8:19;
hence contradiction by A1,A5,A6,JORDAN9:33;
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);
A4: 1 <= i by A2,GOBOARD5:1;
assume i <= 1;
then i = 1 by A4,REAL_1:def 5;
then A5: i-'1 = 0 by GOBOARD9:1;
f is_sequence_on G by JORDAN9:def 1;
then A6: right_cell(f,k,G) = cell(G,i-'1,j) by A1,A2,A3,GOBRD13:29;
len G = width G by JORDAN8:def 1;
then j <= len G by A2,GOBOARD5:1;
then cell(G,0,j) misses C by JORDAN8:21;
hence contradiction by A1,A5,A6,JORDAN9:33;
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);
A4: 1 <= j by A2,GOBOARD5:1;
assume j <= 1;
then j = 1 by A4,REAL_1:def 5;
then A5: j-'1 = 0 by GOBOARD9:1;
f is_sequence_on G by JORDAN9:def 1;
then A6: right_cell(f,k,G) = cell(G,i,j-'1) by A1,A2,A3,GOBRD13:25;
i <= len G by A2,GOBOARD5:1;
then cell(G,i,0) misses C by JORDAN8:20;
hence contradiction by A1,A5,A6,JORDAN9:33;
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);
A4: j <= width G by A2,GOBOARD5:1;
assume j >= width G;
then A5: j = width G by A4,REAL_1:def 5;
f is_sequence_on G by JORDAN9:def 1;
then A6: right_cell(f,k,G) = cell(G,i,j) by A1,A2,A3,GOBRD13:27;
A7: len G = width G by JORDAN8:def 1;
i <= len G by A2,GOBOARD5:1;
then cell(G,i,len G) misses C by JORDAN8:18;
hence contradiction by A1,A5,A6,A7,JORDAN9:33;
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 set such that
A1: c in C & 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 6;
then consider Z being set such that
A2: c in Z and
A3: Z in { LSeg(f,i) where i is Nat: 1 <= i & i+1 <= len f }
by A1,TARSKI:def 4;
consider i being Nat such that
A4: Z = LSeg(f,i) and
A5: 1 <= i & i+1 <= len f by A3;
f is_sequence_on G by JORDAN9:def 1;
then LSeg(f,i) = left_cell(f,i,G) /\ right_cell(f,i,G) by A5,GOBRD13:30;
then A6: c in left_cell(f,i,G) by A2,A4,XBOOLE_0:def 3;
left_cell(f,i,G) misses C by A5,JORDAN9:33;
hence contradiction by A1,A6,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 & i+1 <= len G and
A2: f/.1 = G*(i,width G) and
f/.2 = G*(i+1,width G) &
N-min C in cell(G,i,width G-'1) &
N-min C <> G*(i,width G-'1) by JORDAN9:def 1;
A3: len G = width G by JORDAN8:def 1;
i+0 <= i+1 by AXIOMS:24;
then A4: i <= len G by A1,AXIOMS:22;
4 <= len G by JORDAN8:13;
then 1 <= len G by AXIOMS:22;
then A5: [i,len G] in Indices G by A1,A3,A4,GOBOARD7:10;
A6: 2|^n <> 0 by HEINE:5;
thus N-bound L~f = (N-min L~f)`2 by PSCOMP_1:94
.= (f/.1)`2 by JORDAN9:34
.= |[w+((E-bound C-w)/(2|^n))*(i-2), s+((a-s)/(2|^n))*(len G-2)]|`2
by A2,A3,A5,JORDAN8:def 1
.= s+((a-s)/(2|^n))*(len G-2) by EUCLID:56
.= s+((a-s)/(2|^n))*(2|^n+3-2) by JORDAN8:def 1
.= s+((a-s)/(2|^n))*(2|^n+(3-2)) by XCMPLX_1:29
.= s+(((a-s)/(2|^n))*2|^n+((a-s)/(2|^n))*1) by XCMPLX_1:8
.= s+((a-s)/(2|^n))*2|^n+(a-s)/(2|^n) by XCMPLX_1:1
.= s+(a-s)+(a-s)/(2|^n) by A6,XCMPLX_1:88
.= a+(a-s)/(2|^n) by XCMPLX_1:27;
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: P[0] by NAT_1:18;
A3: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A4: P[n];
assume i < n+1;
then A5: i <= n by NAT_1:38;
set j = n + 1,
a = N-bound C, s = S-bound C;
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;
2|^n > 0 by HEINE:5;
then A7: 2|^n*2 > 0 * 2 by REAL_1:70;
s < a by SPRECT_1:34;
then A8: s - a < 0 by REAL_2:105;
a+(a-s)/(2|^j) - (a+(a-s)/(2|^n))
= a + (a-s)/(2|^j) - a - (a-s)/(2|^n) by XCMPLX_1:36
.= a + (a-s)/(2|^j) +- a - (a-s)/(2|^n) by XCMPLX_0:def 8
.= a +-a + (a-s)/(2|^j) - (a-s)/(2|^n) by XCMPLX_1:1
.= 0 + (a-s)/(2|^j) - (a-s)/(2|^n) by XCMPLX_0:def 6
.= (a-s)/(2|^n*2) - (a-s)/(2|^n)/(2/2) by NEWTON:11
.= (a-s)/(2|^n*2) - (a-s)*2/(2|^n*2) by XCMPLX_1:85
.= (a-s - (a-s)*2)/(2|^n*2) by XCMPLX_1:121
.= (a-s - (2*a-2*s))/(2|^n*2) by XCMPLX_1:40
.= (a-s-2*a+2*s)/(2|^n*2) by XCMPLX_1:37
.= (a-2*a-s+2*s)/(2|^n*2) by XCMPLX_1:21
.= (-a-s+2*s)/(2|^n*2) by XCMPLX_1:187
.= (-a+-s+2*s)/(2|^n*2) by XCMPLX_0:def 8
.= (-a+(-s+2*s))/(2|^n*2) by XCMPLX_1:1
.= (-a+s)/(2|^n*2) by XCMPLX_1:184
.= (s-a)/(2|^n*2) by XCMPLX_0:def 8;
then 0 > a+(a-s)/(2|^j) - (a+(a-s)/(2|^n)) by A7,A8,REAL_2:128;
then N-bound L~Cage(C,n+1) < N-bound L~Cage(C,n) by A6,SQUARE_1:12;
hence thesis by A4,A5,AXIOMS:22,REAL_1:def 5;
end;
for n being Nat holds P[n] from Ind(A2,A3);
hence thesis by A1;
end;
definition
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:42;
end;
theorem Th8:
N-min C in RightComp Cage(C,n)
proof
set f = Cage(C,n),
G = Gauge(C,n);
A1: N-min C in C by SPRECT_1:13;
C misses L~f by Th5;
then C /\ L~f = {} by XBOOLE_0:def 7;
then A2: not N-min C in L~f by A1,XBOOLE_0:def 3;
RightComp f misses L~f by SPRECT_3:42;
then A3: RightComp f /\ L~f = {} by XBOOLE_0:def 7;
consider k being Nat such that
A4: 1 <= k & k+1 <= len G and
A5: f/.1 = G*(k,width G) and
A6: f/.2 = G*(k+1,width G) and
A7: N-min C in cell(G,k,width G-'1) and
N-min C <> G*(k,width G-'1) by JORDAN9:def 1;
A8: f is_sequence_on G by JORDAN9:def 1;
L~f <> {};
then A9: 1+1 <= len f by GOBRD14:8;
A10: len G = width G by JORDAN8:def 1;
A11: 1 <= k+1 by NAT_1:29;
then A12: 1 <= len G by A4,AXIOMS:22;
A13: k < len G by A4,NAT_1:38;
then [k,len G] in Indices G & [k+1,len G] in Indices G
by A4,A10,A11,A12,GOBOARD7:10;
then A14: cell(G,k,len G-'1) = right_cell(f,1,G) by A5,A6,A8,A9,A10,GOBRD13:25;
right_cell(f,1,G) c= right_cell(f,1) by A8,A9,GOBRD13:34;
then A15: Int right_cell(f,1,G) c= Int right_cell(f,1) by TOPS_1:48;
Int right_cell(f,1) c= RightComp f by GOBOARD9:def 2;
then A16: Int cell(G,k,len G-'1) c= RightComp f by A14,A15,XBOOLE_1:1;
RightComp f c= RightComp f \/ L~f by XBOOLE_1:7;
then A17: Int cell(G,k,len G-'1) c= RightComp f \/ L~f by A16,XBOOLE_1:1;
A18: right_cell(f,1,G) is closed by A8,A9,GOBRD13:31;
A19: Fr cell(G,k,len G-'1) c= RightComp f \/ L~f
proof
let q be set; assume
A20: q in Fr cell(G,k,len G-'1);
then reconsider s = q as Point of TOP-REAL 2;
4 <= len G by JORDAN8:13;
then 4 - 1 <= len G - 1 by REAL_1:92;
then 0 <= len G - 1 by AXIOMS:22;
then A21: len G-'1 = len G - 1 by BINARITH:def 3;
A22: len G - 1 < len G - 0 by REAL_1:92;
then Int cell(G,k,len G-'1) <> {} by A10,A13,A21,GOBOARD9:17;
then consider p being set such that
A23: p in Int cell(G,k,len G-'1) by XBOOLE_0:def 1;
reconsider p as Point of TOP-REAL 2 by A23;
per cases;
suppose q in L~f;
hence thesis by XBOOLE_0:def 2;
suppose
A24: not q in L~f;
A25: LSeg(p,s) c= (L~f)`
proof
let a be set; assume
A26: a in LSeg(p,s);
then reconsider b = a as Point of TOP-REAL 2;
3 <= len G-'1 by GOBRD14:17;
then A27: 1 <= len G-'1 by AXIOMS:22;
then A28: 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 A4,A10,A13,A21,A22,GOBOARD6:29;
A29: b = |[b`1,b`2]| by EUCLID:57;
consider x, y being Real such that
A30: p = |[x,y]| and
A31: 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 A23,A28;
Fr cell(G,k,len G-'1) c= cell(G,k,len G-'1) by A14,A18,TOPS_1:69;
then A32: q in cell(G,k,len G-'1) by A20;
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 A4,A10,A13,A21,A22,A27,GOBRD11:32;
then consider m, o being Real such that
A33: s = |[m,o]| and
A34: 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 A32;
A35: s`1 = m & s`2 = o & p`1 = x & p`2 = y by A30,A33,EUCLID:56;
now per cases;
case b = s;
hence a in (L~f)` by A24,SUBSET_1:50;
case
A36: b <> s;
now per cases by REAL_1:def 5;
case s`1 < p`1 & s`2 < p`2;
then s`1 < b`1 & b`1 <= p`1 & s`2 < b`2 & b`2 <= p`2
by A26,A36,TOPREAL6:37,38;
then G*(k,1)`1 < b`1 & b`1 < G*(k+1,1)`1 &
G*(1,len G-'1)`2 < b`2 & b`2 < G*(1,len G-'1+1)`2
by A31,A34,A35,AXIOMS:22;
hence b in Int cell(G,k,len G-'1) by A28,A29;
case s`1 < p`1 & s`2 > p`2;
then s`1 < b`1 & b`1 <= p`1 & p`2 <= b`2 & b`2 < s`2
by A26,A36,TOPREAL6:37,38;
then G*(k,1)`1 < b`1 & b`1 < G*(k+1,1)`1 &
G*(1,len G-'1)`2 < b`2 & b`2 < G*(1,len G-'1+1)`2
by A31,A34,A35,AXIOMS:22;
hence b in Int cell(G,k,len G-'1) by A28,A29;
case s`1 < p`1 & s`2 = p`2;
then s`1 < b`1 & b`1 <= p`1 & p`2 = b`2 & b`2 = s`2
by A26,A36,GOBOARD7:6,TOPREAL6:37;
then G*(k,1)`1 < b`1 & b`1 < G*(k+1,1)`1 &
G*(1,len G-'1)`2 < b`2 & b`2 < G*(1,len G-'1+1)`2
by A31,A34,A35,AXIOMS:22;
hence b in Int cell(G,k,len G-'1) by A28,A29;
case s`1 > p`1 & s`2 < p`2;
then s`1 > b`1 & b`1 >= p`1 & s`2 < b`2 & b`2 <= p`2
by A26,A36,TOPREAL6:37,38;
then G*(k,1)`1 < b`1 & b`1 < G*(k+1,1)`1 &
G*(1,len G-'1)`2 < b`2 & b`2 < G*(1,len G-'1+1)`2
by A31,A34,A35,AXIOMS:22;
hence b in Int cell(G,k,len G-'1) by A28,A29;
case s`1 > p`1 & s`2 > p`2;
then s`1 > b`1 & b`1 >= p`1 & s`2 > b`2 & b`2 >= p`2
by A26,A36,TOPREAL6:37,38;
then G*(k,1)`1 < b`1 & b`1 < G*(k+1,1)`1 &
G*(1,len G-'1)`2 < b`2 & b`2 < G*(1,len G-'1+1)`2
by A31,A34,A35,AXIOMS:22;
hence b in Int cell(G,k,len G-'1) by A28,A29;
case s`1 > p`1 & s`2 = p`2;
then s`1 > b`1 & b`1 >= p`1 & s`2 = b`2 & b`2 = p`2
by A26,A36,GOBOARD7:6,TOPREAL6:37;
then G*(k,1)`1 < b`1 & b`1 < G*(k+1,1)`1 &
G*(1,len G-'1)`2 < b`2 & b`2 < G*(1,len G-'1+1)`2
by A31,A34,A35,AXIOMS:22;
hence b in Int cell(G,k,len G-'1) by A28,A29;
case s`1 = p`1 & s`2 > p`2;
then s`1 = b`1 & b`1 = p`1 & s`2 > b`2 & b`2 >= p`2
by A26,A36,GOBOARD7:5,TOPREAL6:38;
then G*(k,1)`1 < b`1 & b`1 < G*(k+1,1)`1 &
G*(1,len G-'1)`2 < b`2 & b`2 < G*(1,len G-'1+1)`2
by A31,A34,A35,AXIOMS:22;
hence b in Int cell(G,k,len G-'1) by A28,A29;
case s`1 = p`1 & s`2 < p`2;
then s`1 = b`1 & b`1 = p`1 & s`2 < b`2 & b`2 <= p`2
by A26,A36,GOBOARD7:5,TOPREAL6:38;
then G*(k,1)`1 < b`1 & b`1 < G*(k+1,1)`1 &
G*(1,len G-'1)`2 < b`2 & b`2 < G*(1,len G-'1+1)`2
by A31,A34,A35,AXIOMS:22;
hence b in Int cell(G,k,len G-'1) by A28,A29;
case s`1 = p`1 & s`2 = p`2;
then p = s by TOPREAL3:11;
then LSeg(p,s) = {p} by TOPREAL1:7;
hence b in Int cell(G,k,len G-'1) by A23,A26,TARSKI:def 1;
end;
then not b in L~f by A3,A16,XBOOLE_0:def 3;
hence a in (L~f)` by SUBSET_1:50;
end;
hence a in (L~f)`;
end;
A37: RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
A38: {p} c= RightComp f by A16,A23,ZFMISC_1:37;
{p} meets LSeg(p,s)
proof
now take a = p;
thus a in {p} & a in LSeg(p,s) by TARSKI:def 1,TOPREAL1:6;
end; hence thesis by XBOOLE_0:3;
end;
then A39: LSeg(p,s) c= RightComp f by A25,A37,A38,GOBOARD9:6;
s in LSeg(p,s) by TOPREAL1:6;
hence thesis by A39,XBOOLE_0:def 2;
end;
A40: Int right_cell(f,1,G) c= right_cell(f,1,G) by TOPS_1:44;
Fr right_cell(f,1,G) = right_cell(f,1,G) \ Int right_cell(f,1,G)
by A18,TOPS_1:77;
then Fr right_cell(f,1,G) \/ Int right_cell(f,1,G) = right_cell(f,1,G)
by A40,XBOOLE_1:45;
then right_cell(f,1,G) c= RightComp f \/ L~f by A14,A17,A19,XBOOLE_1:8;
hence thesis by A2,A7,A10,A14,XBOOLE_0:def 2;
end;
theorem Th9:
C meets RightComp Cage (C,n)
proof
A1: N-min C in C by SPRECT_1:13;
N-min C in RightComp Cage(C,n) by Th8;
then C /\ RightComp Cage (C,n) <> {} by A1,XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 7;
end;
theorem Th10:
C misses LeftComp Cage(C,n)
proof
set f = Cage(C,n);
C misses L~f by Th5;
then A1: C /\ L~f = {} by XBOOLE_0:def 7;
A2: C meets RightComp f by Th9;
assume A3: C meets LeftComp f;
LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
then consider L being Subset of (TOP-REAL 2)|(L~f)` such that
A4: L = LeftComp f and
A5: L is_a_component_of (TOP-REAL 2)|(L~f)` by CONNSP_1:def 6;
RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
then consider R being Subset of (TOP-REAL 2)|(L~f)` such that
A6: R = RightComp f and
A7: R is_a_component_of (TOP-REAL 2)|(L~f)` by CONNSP_1:def 6;
C c= the carrier of (TOP-REAL 2)|(L~f)`
proof
let c be set;
assume c in C;
then c in the carrier of TOP-REAL 2 & not c in L~f by A1,XBOOLE_0:def 3;
then c in (L~f)` by SUBSET_1:50;
hence thesis by JORDAN1:1;
end;
then reconsider C1 = C as Subset of (TOP-REAL 2)|(L~f)`;
C1 is connected by CONNSP_1:24;
then L = R by A2,A3,A4,A5,A6,A7,JORDAN2C:100;
hence contradiction by A4,A6,SPRECT_4:7;
end;
theorem Th11:
C c= RightComp Cage(C,n)
proof
set f = Cage(C,n);
let c be set;
assume
A1: c in C;
C misses L~f by Th5;
then A2: C /\ L~f = {} by XBOOLE_0:def 7;
C misses LeftComp f by Th10;
then C /\ LeftComp f = {} by XBOOLE_0:def 7;
then not c in LeftComp f & not c in L~f by A1,A2,XBOOLE_0:def 3;
hence c in RightComp f by A1,GOBRD14:28;
end;
theorem Th12:
C c= BDD L~Cage(C,n)
proof
A1: C c= RightComp Cage(C,n) by Th11;
RightComp Cage(C,n) is_inside_component_of L~Cage(C,n) by GOBRD14:45;
then RightComp Cage(C,n) c= BDD L~Cage(C,n) by JORDAN2C:26;
hence thesis by A1,XBOOLE_1:1;
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 6;
let x be set; assume
A2: x in UBD L~f;
UBD L~f = union {B where B is Subset of TOP-REAL 2:
B is_outside_component_of L~f} by JORDAN2C:def 6;
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;
the carrier of TOP-REAL 2 = the carrier of Euclid 2 by TOPREAL3:13;
then reconsider B1 = B as Subset of Euclid 2;
B is_a_component_of (L~f)` by A6,JORDAN2C:def 4;
then consider B2 being Subset of (TOP-REAL 2)|(L~f)` such that
A7: B2 = B and
A8: B2 is_a_component_of (TOP-REAL 2)|(L~f)`
by CONNSP_1:def 6;
B2 is connected by A8,CONNSP_1:def 5;
then A9: B is connected by A7,CONNSP_3:34;
not B is Bounded by A6,JORDAN2C:def 4;
then A10: not B1 is bounded by JORDAN2C:def 2;
the carrier of (TOP-REAL 2)|C` = C` by JORDAN1:1;
then skl (Down(B,C`)) c= the carrier of TOP-REAL 2 by XBOOLE_1:1;
then reconsider P1 = skl (Down(B,C`)) as Subset of TOP-REAL 2;
RightComp f is_inside_component_of L~f by GOBRD14:45;
then A11: C c= RightComp f & B1 misses RightComp f by A6,Th11,GOBRD14:5;
then B1 misses C by XBOOLE_1:63;
then A12: P1 is_outside_component_of C by A9,A10,JORDAN2C:71;
A13: B1 /\ RightComp f = {} by A11,XBOOLE_0:def 7;
A14: Down(B,C`) = B /\ C` by CONNSP_3:def 5;
B c= C`
proof
let a be set; assume
A15: a in B;
then not a in C by A11,A13,XBOOLE_0:def 3;
then a in (the carrier of TOP-REAL 2) \ C by A15,XBOOLE_0:def 4;
hence a in C` by SUBSET_1:def 5;
end;
then Down(B,C`) = B by CONNSP_3:28;
then Down(B,C`) is connected by A9,JORDAN2C:15;
then A16: Down(B,C`) c= skl Down(B,C`) by CONNSP_3:1;
not x in C by A3,A5,A11,A13,XBOOLE_0:def 3;
then x in (the carrier of TOP-REAL 2) \ C by A3,A5,XBOOLE_0:def 4;
then x in C` by SUBSET_1:def 5;
then A17: x in B /\ C` by A3,A5,XBOOLE_0:def 3;
P1 in {W where W is Subset of TOP-REAL 2: W is_outside_component_of C}
by A12;
hence x in UBD C by A1,A14,A16,A17,TARSKI:def 4;
end;
definition
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
func UBD-Family C equals :Def1:
{ UBD L~Cage(C,n) where n is Nat : not contradiction };
coherence;
func BDD-Family C equals :Def2:
{ Cl BDD L~Cage(C,n) where n is Nat : not contradiction };
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;
coherence
proof
{ UBD L~Cage(C,i) where i is Nat : not contradiction } c=
bool the carrier of TOP-REAL 2
proof
let x be set; assume
x in { UBD L~Cage(C,i) where i is Nat : not contradiction };
then ex i being Nat st x = UBD L~Cage(C,i) & not contradiction;
hence x in bool the carrier of TOP-REAL 2;
end;
then UBD-Family C c= bool the carrier of TOP-REAL 2 by Def1;
then UBD-Family C is Subset-Family of TOP-REAL 2
by SETFAM_1:def 7;
hence thesis;
end;
redefine func BDD-Family C -> Subset-Family of TOP-REAL 2;
coherence
proof
{ Cl BDD L~Cage(C,i) where i is Nat : not contradiction } c=
bool the carrier of TOP-REAL 2
proof
let x be set; assume
x in { Cl BDD L~Cage(C,i) where i is Nat : not contradiction };
then ex i being Nat st x = Cl BDD L~Cage(C,i) & not contradiction;
hence x in bool the carrier of TOP-REAL 2;
end;
then BDD-Family C c= bool the carrier of TOP-REAL 2 by Def2;
then BDD-Family C is Subset-Family of TOP-REAL 2
by SETFAM_1:def 7;
hence thesis;
end;
end;
definition
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
cluster UBD-Family C -> non empty;
coherence
proof
consider m being Nat;
{ UBD L~Cage(C,i) where i is Nat : not contradiction } = UBD-Family C
by Def1;
then UBD L~Cage(C,m) in UBD-Family C;
hence thesis;
end;
cluster BDD-Family C -> non empty;
coherence
proof
consider m being Nat;
{ Cl BDD L~Cage(C,i) where i is Nat : not contradiction } = BDD-Family C
by Def2;
then Cl BDD L~Cage(C,m) in BDD-Family C;
hence thesis;
end;
end;
theorem Th14:
union UBD-Family C = UBD C
proof
A1: UBD-Family C = { UBD L~Cage(C,n): not contradiction } by Def1;
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) & not contradiction by A1;
hence X c= UBD C by Th13;
end;
hence union UBD-Family C c= UBD C by ZFMISC_1:94;
let x be set 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 6;
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;
consider B being Subset of TOP-REAL 2 such that
A5: A = B and B is_outside_component_of C by A4;
reconsider p = x as Point of TOP-REAL 2 by A3,A5;
consider q being Point of TOP-REAL 2 such that
A6: q`2 > N-bound L~Cage(C,0) and
A7: p <> q by TOPREAL6:41;
A8: UBD L~Cage(C,0) c= UBD C by Th13;
A9: Cage(C,0)/.1 = N-min L~Cage(C,0) by JORDAN9:34;
A10: UBD L~Cage(C,0) = LeftComp Cage(C,0) by GOBRD14:46;
q in LeftComp Cage(C,0) by A6,A9,JORDAN2C:121;
then consider P such that
A11: P is_S-P_arc_joining p,q and
A12: P c= UBD C by A2,A7,A8,A10,TOPREAL4:30;
consider f being FinSequence of TOP-REAL 2 such that
A13: f is_S-Seq and
A14: P = L~f and
A15: p = f/.1 and q = f/.len f by A11,TOPREAL4:def 1;
reconsider f as being_S-Seq FinSequence of TOP-REAL 2 by A13;
A16: L~f is non empty;
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 A14,A16;
set d = min_dist_min(P1,C1);
C is Bounded by JORDAN2C:73;
then consider B being Subset of TOP-REAL 2 such that
A17: B is_outside_component_of C & B = UBD C by JORDAN2C:76;
UBD C is_a_component_of C` by A17,JORDAN2C:def 4;
then C misses UBD C by GOBRD14:4;
then P misses C by A12,XBOOLE_1:63;
then d > 0 by JGRAPH_1:55;
then d/2 > 0 by REAL_2:127;
then consider n such that
1 < n and
A18: dist(Gauge(C,n)*(1,1),Gauge(C,n)*(1,2)) < d/2 and
A19: dist(Gauge(C,n)*(1,1),Gauge(C,n)*(2,1)) < d/2 by GOBRD14:21;
set G = Gauge(C,n),
g = Cage(C,n);
2 <= len f by SPPOL_1:2;
then A20: x in P by A14,A15,JORDAN3:34;
A21: now
assume L~g /\ P <> {};
then consider a being set such that
A22: a in L~g /\ P by XBOOLE_0:def 1;
reconsider a' = a as Point of Euclid 2 by A22,TOPREAL3:13;
reconsider A = a as Point of TOP-REAL 2 by A22;
A23: a in L~g & a in P by A22,XBOOLE_0:def 3;
then consider i such that
A24: 1 <= i & i+1 <= len g and
A25: a in LSeg(g,i) by SPPOL_2:13;
A26: g is_sequence_on G by JORDAN9:def 1;
then consider i1, j1, i2, j2 being Nat such that
A27: [i1,j1] in Indices G and
A28: g/.i = G*(i1,j1) and
A29: [i2,j2] in Indices G and
A30: g/.(i+1) = G*(i2,j2) and
A31: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A24,JORDAN8:6;
right_cell(g,i,G) meets C by A24,JORDAN9:33;
then consider c being set such that
A32: c in right_cell(g,i,G) /\ C by XBOOLE_0:4;
reconsider c as Point of Euclid 2 by A32,TOPREAL3:13;
reconsider c' = c as Point of TOP-REAL 2 by A32;
c in C by A32,XBOOLE_0:def 3;
then A33: dist(a',c) >= d by A23,WEIERSTR:40;
set e = E-bound C, w = W-bound C, p = N-bound C, s = S-bound C;
A34: len G = width G by JORDAN8:def 1;
4 <= len G by JORDAN8:13;
then A35: 1 <= len G & 1 <= width G & 1+1 <= len G & 1+1 <= width G
by A34,AXIOMS:22;
then [1,1] in Indices G & [1,1+1] in Indices G &
[1+1,1] in Indices G by GOBOARD7:10;
then A36: dist(G*(1,1),G*(1,1+1)) = (p-s)/2|^n &
dist(G*(1,1),G*(1+1,1)) = (e-w)/2|^n by GOBRD14:19,20;
A37: c in right_cell(g,i,G) by A32,XBOOLE_0:def 3;
left_cell(g,i,G) /\ right_cell(g,i,G) = LSeg(g,i) by A24,A26,GOBRD13:30
;
then A38: a in right_cell(g,i,G) by A25,XBOOLE_0:def 3;
now per cases by A31;
case
A39: i1 = i2 & j1+1 = j2;
then A40: j1+1 <= width G by A29,GOBOARD5:1;
then A41: 1 <= i1 & i1 < len G & 1 <= j1 & j1 < width G
by A24,A27,A28,A29,A30,A39,Th1,GOBOARD5:1,NAT_1:38;
A42: right_cell(g,i,G) = cell(G,i1,j1)
by A24,A26,A27,A28,A29,A30,A39,GOBRD13:23
.= { |[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 A41,GOBRD11:32;
then consider r, t being Real such that
A43: c = |[r,t]| and
A44: G*(i1,1)`1 <= r & r <= G*(i1+1,1)`1 &
G*(1,j1)`2 <= t & t <= G*(1,j1+1)`2 by A37;
consider aa, ab being Real such that
A45: a = |[aa,ab]| and
A46: G*(i1,1)`1 <= aa & aa <= G*(i1+1,1)`1 &
G*(1,j1)`2 <= ab & ab <= G*(1,j1+1)`2 by A38,A42;
A47: c'`1 = r & c'`2 = t & A`1 = aa & A`2 = ab by A43,A45,EUCLID:56;
1 <= i1+1 & i1+1 <= len G & 1 <= j1+1 by A41,NAT_1:38;
then A48: [i1,1] in Indices G & [i1+1,1] in Indices G &
[1,j1] in Indices G & [1,j1+1] in Indices G
by A35,A40,A41,GOBOARD7:10;
then A49: dist(G*(i1,1),G*(i1+1,1)) = G*(i1+1,1)`1 - G*(i1,1)`1 &
dist(G*(1,j1),G*(1,j1+1)) = G*(1,j1+1)`2 - G*(1,j1)`2
by GOBRD14:15,16;
dist(G*(1,j1),G*(1,j1+1)) = (p-s)/2|^n &
dist(G*(i1,1),G*(i1+1,1)) = (e-w)/2|^n by A48,GOBRD14:19,20;
hence dist(A,c') <= (p-s)/2|^n + (e-w)/2|^n by A44,A46,A47,A49,GOBRD14:
12;
case
A50: i1+1 = i2 & j1 = j2;
then A51: i1+1 <= len G by A29,GOBOARD5:1;
j2 > 1 by A24,A27,A28,A29,A30,A50,Th3;
then A52: j2-1 > 0 by SQUARE_1:11;
then A53: j2-1 = j2-'1 by BINARITH:def 3;
A54: j2 <= width G by A29,GOBOARD5:1;
width G - 1 < width G - 0 by REAL_1:92;
then A55: 1 <= i1 & i1 < len G & 1 <= j2-'1 & j2-'1 < width G
by A27,A51,A52,A53,A54,GOBOARD5:1,NAT_1:38,REAL_1:92,RLVECT_1:99;
A56: right_cell(g,i,G) = cell(G,i1,j2-'1)
by A24,A26,A27,A28,A29,A30,A50,GOBRD13:25
.= { |[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,GOBRD11:32;
then consider r, t being Real such that
A57: c = |[r,t]| and
A58: 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 A37;
consider aa, ab being Real such that
A59: a = |[aa,ab]| and
A60: 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 A38,A56;
A61: c'`1 = r & c'`2 = t & A`1 = aa & A`2 = ab by A57,A59,EUCLID:56;
A62: 1 <= i1+1 & i1+1 <= len G & j2-'1+1 <= width G by A55,NAT_1:38;
1 <= j2-'1+1 by A55,NAT_1:38;
then A63: [i1,1] in Indices G & [i1+1,1] in Indices G &
[1,j2-'1] in Indices G & [1,j2-'1+1] in Indices G
by A35,A55,A62,GOBOARD7:10;
then A64: dist(G*(i1,1),G*(i1+1,1)) = G*(i1+1,1)`1 - G*(i1,1)`1 &
dist(G*(1,j2-'1),G*(1,j2-'1+1)) = G*(1,j2-'1+1)`2 - G*(1,j2-'1)`2
by GOBRD14:15,16;
dist(G*(1,j2-'1),G*(1,j2-'1+1)) = (p-s)/2|^n &
dist(G*(i1,1),G*(i1+1,1)) = (e-w)/2|^n by A63,GOBRD14:19,20;
hence dist(A,c') <= (p-s)/2|^n + (e-w)/2|^n by A58,A60,A61,A64,GOBRD14:
12;
case
A65: i1 = i2+1 & j1 = j2;
then i2+1 <= len G by A27,GOBOARD5:1;
then A66: 1 <= i2 & i2 < len G & 1 <= j1 & j1 < width G
by A24,A27,A28,A29,A30,A65,Th4,GOBOARD5:1,NAT_1:38;
A67: right_cell(g,i,G) = cell(G,i2,j1)
by A24,A26,A27,A28,A29,A30,A65,GOBRD13:27
.= { |[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 A66,GOBRD11:32;
then consider r, t being Real such that
A68: c = |[r,t]| and
A69: G*(i2,1)`1 <= r & r <= G*(i2+1,1)`1 &
G*(1,j1)`2 <= t & t <= G*(1,j1+1)`2 by A37;
consider aa, ab being Real such that
A70: a = |[aa,ab]| and
A71: G*(i2,1)`1 <= aa & aa <= G*(i2+1,1)`1 &
G*(1,j1)`2 <= ab & ab <= G*(1,j1+1)`2 by A38,A67;
A72: c'`1 = r & c'`2 = t & A`1 = aa & A`2 = ab by A68,A70,EUCLID:56;
A73: 1 <= i2+1 & i2+1 <= len G & j1+1 <= width G by A66,NAT_1:38;
1 <= j1+1 by NAT_1:37;
then A74: [i2,1] in Indices G & [i2+1,1] in Indices G &
[1,j1] in Indices G & [1,j1+1] in Indices G
by A35,A66,A73,GOBOARD7:10;
then A75: dist(G*(i2,1),G*(i2+1,1)) = G*(i2+1,1)`1 - G*(i2,1)`1 &
dist(G*(1,j1),G*(1,j1+1)) = G*(1,j1+1)`2 - G*(1,j1)`2
by GOBRD14:15,16;
dist(G*(1,j1),G*(1,j1+1)) = (p-s)/2|^n &
dist(G*(i2,1),G*(i2+1,1)) = (e-w)/2|^n by A74,GOBRD14:19,20;
hence dist(A,c') <= (p-s)/2|^n + (e-w)/2|^n by A69,A71,A72,A75,GOBRD14:
12;
case
A76: i1 = i2 & j1 = j2+1;
then A77: j2+1 <= width G by A27,GOBOARD5:1;
i1 > 1 by A24,A27,A28,A29,A30,A76,Th2;
then A78: i1-1 > 0 by SQUARE_1:11;
then A79: i1-1 = i1-'1 by BINARITH:def 3;
A80: i1 <= len G by A27,GOBOARD5:1;
len G - 1 < len G - 0 by REAL_1:92;
then A81: 1 <= i1-'1 & i1-'1 < len G & 1 <= j2 & j2 < width G
by A29,A77,A78,A79,A80,GOBOARD5:1,NAT_1:38,REAL_1:92,RLVECT_1:99;
A82: right_cell(g,i,G) = cell(G,i1-'1,j2)
by A24,A26,A27,A28,A29,A30,A76,GOBRD13:29
.= { |[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 A81,GOBRD11:32;
then consider r, t being Real such that
A83: c = |[r,t]| and
A84: 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 A37;
consider aa, ab being Real such that
A85: a = |[aa,ab]| and
A86: 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 A38,A82;
A87: c'`1 = r & c'`2 = t & A`1 = aa & A`2 = ab by A83,A85,EUCLID:56;
1 <= i1-'1+1 & i1-'1+1 <= len G & 1 <= j2+1 by A81,NAT_1:38;
then A88: [i1-'1,1] in Indices G & [i1-'1+1,1] in Indices G &
[1,j2] in Indices G & [1,j2+1] in Indices G
by A35,A77,A81,GOBOARD7:10;
then A89: dist(G*(i1-'1,1),G*(i1-'1+1,1)) = G*(i1-'1+1,1)`1 - G*(i1-'1,1)`1
&
dist(G*(1,j2),G*(1,j2+1)) = G*(1,j2+1)`2 - G*(1,j2)`2
by GOBRD14:15,16;
dist(G*(1,j2),G*(1,j2+1)) = (p-s)/2|^n &
dist(G*(i1-'1,1),G*
(i1-'1+1,1)) = (e-w)/2|^n by A88,GOBRD14:19,20;
hence dist(A,c') <= (p-s)/2|^n + (e-w)/2|^n by A84,A86,A87,A89,GOBRD14:
12;
end;
then A90: dist(a',c) <= (p-s)/2|^n + (e-w)/2|^n by GOBRD14:def 1;
(p-s)/2|^n + (e-w)/2|^n < d/2 + d/2 by A18,A19,A36,REAL_1:67;
then (p-s)/2|^n + (e-w)/2|^n < d by XCMPLX_1:66;
hence contradiction by A33,A90,AXIOMS:22;
end;
L~g is Bounded by JORDAN2C:73;
then consider B being Subset of TOP-REAL 2 such that
A91: B is_outside_component_of L~g and
A92: B = UBD L~g by JORDAN2C:76;
consider E being Subset of (TOP-REAL 2)|(L~g)` such that
A93: E = B & E is_a_component_of (TOP-REAL 2)|(L~g)` and
not E is bounded Subset of Euclid 2 by A91,JORDAN2C:18;
A94: P c= (L~g)`
proof
let a be set;
assume
A95: a in P;
then not a in L~g by A21,XBOOLE_0:def 3;
hence thesis by A95,SUBSET_1:50;
end;
A96: P is_an_arc_of p,q by A11,A14,A16,TOPREAL4:3;
then A97: P is connected by JORDAN6:11;
A98: UBD L~g is_a_component_of (L~g)` by A92,A93,CONNSP_1:def 6;
A99: g/.1 = N-min L~g by JORDAN9:34;
0 < n or 0 = n by NAT_1:18;
then N-bound L~(Cage(C,0)) >= N-bound L~g by Th7;
then q`2 > N-bound L~g by A6,AXIOMS:22;
then q in LeftComp g by A99,JORDAN2C:121;
then q in UBD L~g by GOBRD14:46;
then A100: {q} c= UBD L~g by ZFMISC_1:37;
{q} meets P
proof
now take a = q;
thus a in {q} & a in P by A96,TARSKI:def 1,TOPREAL1:4;
end; hence thesis by XBOOLE_0:3;
end;
then A101: P c= UBD L~g by A94,A97,A98,A100,GOBOARD9:6;
UBD L~g in UBD-Family C by A1;
hence x in union UBD-Family C by A20,A101,TARSKI:def 4;
end;
theorem Th15:
C c= meet BDD-Family C
proof
A1: BDD-Family C = { Cl BDD L~Cage(C,k) where k is Nat : not contradiction }
by Def2;
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
A2: Z = Cl BDD L~Cage(C,k) by A1;
A3: C c= BDD L~Cage(C,k) by Th12;
BDD L~Cage(C,k) c= Cl BDD L~Cage(C,k) by PRE_TOPC:48;
hence thesis by A2,A3,XBOOLE_1:1;
end;
hence thesis by SETFAM_1:6;
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:10;
A2: x in BDD C & x in LeftComp f by A1,XBOOLE_0:def 3;
A3: UBD-Family C = { UBD L~Cage(C,k) where k is Nat : not contradiction }
by Def1;
BDD C misses UBD C by JORDAN2C:28;
then BDD C /\ UBD C = {} by XBOOLE_0:def 7;
then not x in UBD C by A2,XBOOLE_0:def 3;
then A4: not x in union UBD-Family C by Th14;
UBD L~f in { UBD L~Cage(C,k) where k is Nat : not contradiction };
then not x in UBD L~f by A3,A4,TARSKI:def 4;
hence contradiction by A2,GOBRD14:46;
end;
theorem Th17:
BDD C c= RightComp Cage(C,n)
proof
set f = Cage(C,n);
let x be set;
assume
A1: x in BDD C;
A2: UBD-Family C = { UBD L~Cage(C,k) where k is Nat : not contradiction }
by Def1;
BDD C misses UBD C by JORDAN2C:28;
then BDD C /\ UBD C = {} by XBOOLE_0:def 7;
then not x in UBD C by A1,XBOOLE_0:def 3;
then A3: not x in union UBD-Family C by Th14;
UBD L~f in { UBD L~Cage(C,k) where k is Nat : not contradiction };
then A4: not x in UBD L~Cage(C,n) by A2,A3,TARSKI:def 4;
A5: UBD L~f = union {E where E is Subset of TOP-REAL 2:
E is_outside_component_of L~f} by JORDAN2C:def 6;
LeftComp f is_outside_component_of L~f by GOBRD14:44;
then LeftComp f in {E where E is Subset of TOP-REAL 2:
E is_outside_component_of L~f};
then A6: not x in LeftComp f by A4,A5,TARSKI:def 4;
A7: L~f = (Cl LeftComp f) \ LeftComp f by GOBRD14:30;
now
assume x in Cl LeftComp f;
then BDD C meets LeftComp f by A1,PRE_TOPC:def 13;
hence contradiction by Th16;
end;
then not x in L~f by A7,XBOOLE_0:def 4;
hence x in RightComp f by A1,A6,GOBRD14:28;
end;
theorem Th18:
P is_inside_component_of C implies P misses L~Cage(C,n)
proof
set f = Cage(C,n);
assume
A1: P is_inside_component_of C;
assume P /\ L~f <> {};
then consider x being Point of TOP-REAL 2 such that
A2: x in P /\ L~f by SUBSET_1:10;
A3: x in P & x in L~f by A2,XBOOLE_0:def 3;
P c= BDD C by A1,JORDAN2C:26;
then A4: x in BDD C by A3;
BDD C c= RightComp f by Th17;
hence contradiction by A3,A4,GOBRD14:28;
end;
theorem Th19:
BDD C misses L~Cage(C,n)
proof
A1: BDD C = union {B where B is Subset of TOP-REAL 2:
B is_inside_component_of C} by JORDAN2C:def 5;
assume not thesis;
then consider x being set such that
A2: x in BDD C /\ L~Cage(C,n) by XBOOLE_0:4;
x in BDD C by A2,XBOOLE_0:def 3;
then consider Z being set such that
A3: x in Z & Z in {B where B is Subset of TOP-REAL 2:
B is_inside_component_of C} by A1,TARSKI:def 4;
consider B being Subset of TOP-REAL 2 such that
A4: Z = B & B is_inside_component_of C by A3;
B misses L~Cage(C,n) by A4,Th18;
then A5: B /\ L~Cage(C,n) = {} by XBOOLE_0:def 7;
x in L~Cage(C,n) by A2,XBOOLE_0:def 3;
hence thesis by A3,A4,A5,XBOOLE_0:def 3;
end;
theorem Th20:
COMPLEMENT UBD-Family C = BDD-Family C
proof
A1: BDD-Family C = { Cl BDD L~Cage(C,k) where k is Nat : not contradiction }
by Def2;
A2: UBD-Family C = { UBD L~Cage(C,n): not contradiction } by Def1;
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
A3: P = Cl BDD L~Cage(C,k) by A1;
P = Cl RightComp Cage(C,k) by A3,GOBRD14:47;
then A4: P = (RightComp Cage(C,k)) \/ L~Cage(C,k) by GOBRD14:31;
A5: L~Cage(C,k) misses LeftComp Cage(C,k) by SPRECT_3:43;
RightComp Cage(C,k) misses LeftComp Cage(C,k) by GOBRD14:24;
then A6: P misses LeftComp Cage(C,k) by A4,A5,XBOOLE_1:70;
A7: P \/ LeftComp Cage(C,k) = the carrier of TOP-REAL 2 by A4,GOBRD14:25;
P` /\ (LeftComp Cage(C,k))` = (P \/ LeftComp Cage(C,k))` by SUBSET_1:
29
.= ([#]the carrier of TOP-REAL 2)` by A7,SUBSET_1:def 4
.= {}the carrier of TOP-REAL 2 by SUBSET_1:21;
then P` misses (LeftComp Cage(C,k))` by XBOOLE_0:def 7;
then P` = LeftComp Cage(C,k) by A6,SUBSET_1:46;
then P` = UBD L~Cage(C,k) by GOBRD14:46;
hence P` in UBD-Family C by A2;
end;
assume P` in UBD-Family C;
then consider k such that
A8: P` = UBD L~Cage(C,k) by A2;
A9: P` = LeftComp Cage(C,k) by A8,GOBRD14:46;
then A10: P` misses RightComp Cage(C,k) by GOBRD14:24;
P` misses L~Cage(C,k) by A9,SPRECT_3:43;
then P` misses (RightComp Cage(C,k)) \/ L~Cage(C,k) by A10,XBOOLE_1:70;
then A11: P` misses Cl RightComp Cage(C,k) by GOBRD14:31;
A12: P` \/ ((RightComp Cage(C,k)) \/ L~Cage(C,k))
= the carrier of TOP-REAL 2 by A9,GOBRD14:25;
P`` /\ (Cl RightComp Cage(C,k))`
= (P` \/ (Cl RightComp Cage(C,k)))` by SUBSET_1:29
.= (P` \/ ((RightComp Cage(C,k)) \/ L~Cage(C,k)))` by GOBRD14:31
.= ([#]the carrier of TOP-REAL 2)` by A12,SUBSET_1:def 4
.= {}the carrier of TOP-REAL 2 by SUBSET_1:21;
then P`` misses (Cl RightComp Cage(C,k))` by XBOOLE_0:def 7;
then P`` = Cl RightComp Cage(C,k) by A11,SUBSET_1:46;
then P = Cl BDD L~Cage(C,k) by GOBRD14:47;
hence P in BDD-Family C by A1;
end;
hence thesis by SETFAM_1:def 8;
end;
theorem
meet BDD-Family C = C \/ BDD C
proof
(BDD C) misses (UBD C) by JORDAN2C:28;
then A1: (BDD C) /\ (UBD C) = {} by XBOOLE_0:def 7;
A2: UBD-Family C = { UBD L~Cage(C,n) where n is Nat : not contradiction }
by Def1;
A3: BDD-Family C = { Cl BDD L~Cage(C,n) where n is Nat : not contradiction }
by Def2;
thus meet BDD-Family C c= C \/ BDD C
proof
let x be set;
assume
A4: 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:47;
then not x in union UBD-Family C by A4,XBOOLE_0:def 4;
then A5: not x in UBD C by Th14;
per cases;
suppose not x in C;
then A6: x in C` by A4,SUBSET_1:50;
BDD C \/ UBD C = C` by JORDAN2C:31;
then x in BDD C by A5,A6,XBOOLE_0:def 2;
hence x in C \/ BDD C by XBOOLE_0:def 2;
suppose x in C;
hence x in C \/ BDD C by XBOOLE_0:def 2;
end;
A7: BDD C c= meet BDD-Family C
proof
let x be set;
assume
A8: x in BDD C;
then not x in UBD C by A1,XBOOLE_0:def 3;
then A9: 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
A10: Y = Cl BDD L~Cage(C,n) and not contradiction by A3;
A11: UBD L~Cage(C,n) = union{B where B is Subset of TOP-REAL 2:
B is_outside_component_of L~Cage(C,n)} by JORDAN2C:def 6;
A12: BDD L~Cage(C,n) = union{B where B is Subset of TOP-REAL 2:
B is_inside_component_of L~Cage(C,n)} by JORDAN2C:def 5;
UBD L~Cage(C,n) in UBD-Family C by A2;
then A13: not x in UBD L~Cage(C,n) by A9,TARSKI:def 4;
LeftComp Cage(C,n) is_outside_component_of L~Cage(C,n) by GOBRD14:44;
then LeftComp Cage(C,n) in {B where B is Subset of TOP-REAL 2:
B is_outside_component_of L~Cage(C,n)};
then A14: not x in LeftComp Cage(C,n) by A11,A13,TARSKI:def 4;
BDD C misses L~Cage(C,n) by Th19;
then BDD C /\ L~Cage(C,n) = {} by XBOOLE_0:def 7;
then not x in L~Cage(C,n) by A8,XBOOLE_0:def 3;
then A15: x in RightComp Cage(C,n) by A8,A14,GOBRD14:28;
RightComp Cage(C,n) is_inside_component_of L~Cage(C,n)
by GOBRD14:45;
then RightComp Cage(C,n) in {B where B is Subset of TOP-REAL 2:
B is_inside_component_of L~Cage(C,n)};
then A16: x in BDD L~Cage(C,n) by A12,A15,TARSKI:def 4;
BDD L~Cage(C,n) c= Cl BDD L~Cage(C,n) by PRE_TOPC:48;
hence x in Y by A10,A16;
end;
hence x in meet BDD-Family C by SETFAM_1:def 1;
end;
C c= meet BDD-Family C by Th15;
hence thesis by A7,XBOOLE_1:8;
end;