:: JORDAN10 semantic presentation
begin
registration
clusterV21() connected compact non horizontal non vertical for Element of K6( the carrier of (TOP-REAL 2));
existence
ex b1 being Subset of (TOP-REAL 2) st
( b1 is connected & b1 is compact & not b1 is vertical & not b1 is horizontal )
proof
take R^2-unit_square ; ::_thesis: ( R^2-unit_square is connected & R^2-unit_square is compact & not R^2-unit_square is vertical & not R^2-unit_square is horizontal )
thus ( R^2-unit_square is connected & R^2-unit_square is compact & not R^2-unit_square is vertical & not R^2-unit_square is horizontal ) ; ::_thesis: verum
end;
end;
theorem Th1: :: JORDAN10:1
for k, n, i, j being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 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)) holds
i < len (Gauge (C,n))
proof
let k, n, i, j be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 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)) holds
i < len (Gauge (C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( 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)) )
set f = Cage (C,n);
set 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)) ) ; ::_thesis: i < len (Gauge (C,n))
assume A4: i >= len (Gauge (C,n)) ; ::_thesis: contradiction
len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
then A5: j <= len (Gauge (C,n)) by A2, MATRIX_1:38;
i <= len (Gauge (C,n)) by A2, MATRIX_1:38;
then A6: i = len (Gauge (C,n)) by A4, XXREAL_0:1;
Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then right_cell ((Cage (C,n)),k,(Gauge (C,n))) = cell ((Gauge (C,n)),i,j) by A1, A2, A3, GOBRD13:22;
hence contradiction by A1, A6, A5, JORDAN8:16, JORDAN9:31; ::_thesis: verum
end;
theorem Th2: :: JORDAN10:2
for k, n, i, j being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 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) holds
i > 1
proof
let k, n, i, j be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 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) holds
i > 1
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( 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 )
set f = Cage (C,n);
set 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) ) ; ::_thesis: i > 1
assume A4: i <= 1 ; ::_thesis: contradiction
1 <= i by A2, MATRIX_1:38;
then i = 1 by A4, XXREAL_0:1;
then A5: i -' 1 = 0 by XREAL_1:232;
len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
then A6: j <= len (Gauge (C,n)) by A2, MATRIX_1:38;
Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then right_cell ((Cage (C,n)),k,(Gauge (C,n))) = cell ((Gauge (C,n)),(i -' 1),j) by A1, A2, A3, GOBRD13:28;
hence contradiction by A1, A5, A6, JORDAN8:18, JORDAN9:31; ::_thesis: verum
end;
theorem Th3: :: JORDAN10:3
for k, n, i, j being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 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) holds
j > 1
proof
let k, n, i, j be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 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) holds
j > 1
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( 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 )
set f = Cage (C,n);
set 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) ) ; ::_thesis: j > 1
assume A4: j <= 1 ; ::_thesis: contradiction
1 <= j by A2, MATRIX_1:38;
then j = 1 by A4, XXREAL_0:1;
then A5: j -' 1 = 0 by XREAL_1:232;
A6: i <= len (Gauge (C,n)) by A2, MATRIX_1:38;
Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then right_cell ((Cage (C,n)),k,(Gauge (C,n))) = cell ((Gauge (C,n)),i,(j -' 1)) by A1, A2, A3, GOBRD13:24;
hence contradiction by A1, A5, A6, JORDAN8:17, JORDAN9:31; ::_thesis: verum
end;
theorem Th4: :: JORDAN10:4
for k, n, i, j being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 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) holds
j < width (Gauge (C,n))
proof
let k, n, i, j be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 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) holds
j < width (Gauge (C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( 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)) )
set f = Cage (C,n);
set 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) ) ; ::_thesis: j < width (Gauge (C,n))
assume A4: j >= width (Gauge (C,n)) ; ::_thesis: contradiction
j <= width (Gauge (C,n)) by A2, MATRIX_1:38;
then A5: j = width (Gauge (C,n)) by A4, XXREAL_0:1;
A6: ( len (Gauge (C,n)) = width (Gauge (C,n)) & i <= len (Gauge (C,n)) ) by A2, JORDAN8:def_1, MATRIX_1:38;
Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then right_cell ((Cage (C,n)),k,(Gauge (C,n))) = cell ((Gauge (C,n)),i,j) by A1, A2, A3, GOBRD13:26;
hence contradiction by A1, A5, A6, JORDAN8:15, JORDAN9:31; ::_thesis: verum
end;
theorem Th5: :: JORDAN10:5
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C misses L~ (Cage (C,n))
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C misses L~ (Cage (C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: C misses L~ (Cage (C,n))
set f = Cage (C,n);
set G = Gauge (C,n);
assume not C misses L~ (Cage (C,n)) ; ::_thesis: contradiction
then consider c being set such that
A1: c in C and
A2: c in L~ (Cage (C,n)) by XBOOLE_0:3;
L~ (Cage (C,n)) = union { (LSeg ((Cage (C,n)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (Cage (C,n)) ) } by TOPREAL1:def_4;
then consider Z being set such that
A3: c in Z and
A4: Z in { (LSeg ((Cage (C,n)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (Cage (C,n)) ) } by A2, TARSKI:def_4;
consider i being Element of NAT such that
A5: Z = LSeg ((Cage (C,n)),i) and
A6: ( 1 <= i & i + 1 <= len (Cage (C,n)) ) by A4;
Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then LSeg ((Cage (C,n)),i) = (left_cell ((Cage (C,n)),i,(Gauge (C,n)))) /\ (right_cell ((Cage (C,n)),i,(Gauge (C,n)))) by A6, GOBRD13:29;
then A7: c in left_cell ((Cage (C,n)),i,(Gauge (C,n))) by A3, A5, XBOOLE_0:def_4;
left_cell ((Cage (C,n)),i,(Gauge (C,n))) misses C by A6, JORDAN9:31;
hence contradiction by A1, A7, XBOOLE_0:3; ::_thesis: verum
end;
theorem Th6: :: JORDAN10:6
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-bound (L~ (Cage (C,n))) = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n))
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-bound (L~ (Cage (C,n))) = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: N-bound (L~ (Cage (C,n))) = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n))
set a = N-bound C;
set s = S-bound C;
set w = W-bound C;
set f = Cage (C,n);
set G = Gauge (C,n);
consider i being Element of NAT such that
A1: 1 <= i and
A2: i + 1 <= len (Gauge (C,n)) and
A3: (Cage (C,n)) /. 1 = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) and
(Cage (C,n)) /. 2 = (Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))) and
N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) and
N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) by JORDAN9:def_1;
A4: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
4 <= len (Gauge (C,n)) by JORDAN8:10;
then A5: 1 <= len (Gauge (C,n)) by XXREAL_0:2;
i + 0 <= i + 1 by XREAL_1:6;
then i <= len (Gauge (C,n)) by A2, XXREAL_0:2;
then A6: [i,(len (Gauge (C,n)))] in Indices (Gauge (C,n)) by A1, A4, A5, MATRIX_1:36;
A7: 2 |^ n <> 0 by NEWTON:83;
thus N-bound (L~ (Cage (C,n))) = (N-min (L~ (Cage (C,n)))) `2 by EUCLID:52
.= ((Cage (C,n)) /. 1) `2 by JORDAN9:32
.= |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((len (Gauge (C,n))) - 2)))]| `2 by A3, A4, A6, JORDAN8:def_1
.= (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((len (Gauge (C,n))) - 2)) by EUCLID:52
.= (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((2 |^ n) + 3) - 2)) by JORDAN8:def_1
.= ((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (2 |^ n))) + (((N-bound C) - (S-bound C)) / (2 |^ n))
.= ((S-bound C) + ((N-bound C) - (S-bound C))) + (((N-bound C) - (S-bound C)) / (2 |^ n)) by A7, XCMPLX_1:87
.= (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n)) ; ::_thesis: verum
end;
theorem Th7: :: JORDAN10:7
for i, j being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st i < j holds
N-bound (L~ (Cage (C,j))) < N-bound (L~ (Cage (C,i)))
proof
let i, j be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st i < j holds
N-bound (L~ (Cage (C,j))) < N-bound (L~ (Cage (C,i)))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( i < j implies N-bound (L~ (Cage (C,j))) < N-bound (L~ (Cage (C,i))) )
assume A1: i < j ; ::_thesis: N-bound (L~ (Cage (C,j))) < N-bound (L~ (Cage (C,i)))
defpred S1[ Element of NAT ] means ( i < $1 implies N-bound (L~ (Cage (C,$1))) < N-bound (L~ (Cage (C,i))) );
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; ::_thesis: S1[n + 1]
set j = n + 1;
set a = N-bound C;
set s = S-bound C;
A4: ((N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ (n + 1)))) - ((N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n))) = (0 + (((N-bound C) - (S-bound C)) / (2 |^ (n + 1)))) - (((N-bound C) - (S-bound C)) / (2 |^ n))
.= (((N-bound C) - (S-bound C)) / ((2 |^ n) * 2)) - ((((N-bound C) - (S-bound C)) / (2 |^ n)) / (2 / 2)) by NEWTON:6
.= (((N-bound C) - (S-bound C)) / ((2 |^ n) * 2)) - ((((N-bound C) - (S-bound C)) * 2) / ((2 |^ n) * 2)) by XCMPLX_1:84
.= (((N-bound C) - (S-bound C)) - ((2 * (N-bound C)) - (2 * (S-bound C)))) / ((2 |^ n) * 2) by XCMPLX_1:120
.= ((S-bound C) - (N-bound C)) / ((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))) = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n)) & N-bound (L~ (Cage (C,(n + 1)))) = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ (n + 1))) ) by Th6;
(S-bound C) - (N-bound C) < 0 by SPRECT_1:32, XREAL_1:49;
then 0 > ((N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ (n + 1)))) - ((N-bound C) + (((N-bound C) - (S-bound C)) / (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 ; ::_thesis: N-bound (L~ (Cage (C,(n + 1)))) < N-bound (L~ (Cage (C,i)))
then i <= n by NAT_1:13;
hence N-bound (L~ (Cage (C,(n + 1)))) < N-bound (L~ (Cage (C,i))) by A3, A7, XXREAL_0:1, XXREAL_0:2; ::_thesis: verum
end;
A8: S1[ 0 ] by NAT_1:2;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A8, A2);
hence N-bound (L~ (Cage (C,j))) < N-bound (L~ (Cage (C,i))) by A1; ::_thesis: verum
end;
registration
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2);
let n be Element of NAT ;
cluster Cl (RightComp (Cage (C,n))) -> compact ;
coherence
Cl (RightComp (Cage (C,n))) is compact by GOBRD14:32;
end;
theorem Th8: :: JORDAN10:8
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-min C in RightComp (Cage (C,n))
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-min C in RightComp (Cage (C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: N-min C in RightComp (Cage (C,n))
set f = Cage (C,n);
set G = Gauge (C,n);
consider k being Element of NAT such that
A1: 1 <= k and
A2: k + 1 <= len (Gauge (C,n)) and
A3: ( (Cage (C,n)) /. 1 = (Gauge (C,n)) * (k,(width (Gauge (C,n)))) & (Cage (C,n)) /. 2 = (Gauge (C,n)) * ((k + 1),(width (Gauge (C,n)))) ) and
A4: N-min C in cell ((Gauge (C,n)),k,((width (Gauge (C,n))) -' 1)) and
N-min C <> (Gauge (C,n)) * (k,((width (Gauge (C,n))) -' 1)) by JORDAN9:def_1;
A5: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
A6: 1 <= k + 1 by NAT_1:11;
then A7: 1 <= len (Gauge (C,n)) by A2, XXREAL_0:2;
then A8: [(k + 1),(len (Gauge (C,n)))] in Indices (Gauge (C,n)) by A2, A5, A6, MATRIX_1:36;
L~ (Cage (C,n)) <> {} ;
then A9: ( Cage (C,n) is_sequence_on Gauge (C,n) & 1 + 1 <= len (Cage (C,n)) ) by GOBRD14:2, JORDAN9:def_1;
then right_cell ((Cage (C,n)),1,(Gauge (C,n))) is closed by GOBRD13:30;
then Fr (right_cell ((Cage (C,n)),1,(Gauge (C,n)))) = (right_cell ((Cage (C,n)),1,(Gauge (C,n)))) \ (Int (right_cell ((Cage (C,n)),1,(Gauge (C,n))))) by TOPS_1:43;
then A10: (Fr (right_cell ((Cage (C,n)),1,(Gauge (C,n))))) \/ (Int (right_cell ((Cage (C,n)),1,(Gauge (C,n))))) = right_cell ((Cage (C,n)),1,(Gauge (C,n))) by TOPS_1:16, XBOOLE_1:45;
A11: k < len (Gauge (C,n)) by A2, NAT_1:13;
then [k,(len (Gauge (C,n)))] in Indices (Gauge (C,n)) by A1, A5, A7, MATRIX_1:36;
then A12: cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1)) = right_cell ((Cage (C,n)),1,(Gauge (C,n))) by A3, A9, A5, A8, GOBRD13:24;
A13: Int (right_cell ((Cage (C,n)),1)) c= RightComp (Cage (C,n)) by GOBOARD9:def_2;
Int (right_cell ((Cage (C,n)),1,(Gauge (C,n)))) c= Int (right_cell ((Cage (C,n)),1)) by A9, GOBRD13:33, TOPS_1:19;
then A14: Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) c= RightComp (Cage (C,n)) by A12, A13, XBOOLE_1:1;
RightComp (Cage (C,n)) misses L~ (Cage (C,n)) by SPRECT_3:25;
then A15: (RightComp (Cage (C,n))) /\ (L~ (Cage (C,n))) = {} by XBOOLE_0:def_7;
A16: Fr (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) c= (RightComp (Cage (C,n))) \/ (L~ (Cage (C,n)))
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in Fr (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) or q in (RightComp (Cage (C,n))) \/ (L~ (Cage (C,n))) )
assume A17: q in Fr (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) ; ::_thesis: q in (RightComp (Cage (C,n))) \/ (L~ (Cage (C,n)))
then reconsider s = q as Point of (TOP-REAL 2) ;
4 <= len (Gauge (C,n)) by JORDAN8:10;
then 4 - 1 <= (len (Gauge (C,n))) - 1 by XREAL_1:13;
then 0 <= (len (Gauge (C,n))) - 1 by XXREAL_0:2;
then A18: (len (Gauge (C,n))) -' 1 = (len (Gauge (C,n))) - 1 by XREAL_0:def_2;
A19: (len (Gauge (C,n))) - 1 < (len (Gauge (C,n))) - 0 by XREAL_1:15;
then Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) <> {} by A5, A11, A18, GOBOARD9:14;
then consider p being set such that
A20: p in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) by XBOOLE_0:def_1;
reconsider p = p as Point of (TOP-REAL 2) by A20;
percases ( q in L~ (Cage (C,n)) or not q in L~ (Cage (C,n)) ) ;
suppose q in L~ (Cage (C,n)) ; ::_thesis: q in (RightComp (Cage (C,n))) \/ (L~ (Cage (C,n)))
hence q in (RightComp (Cage (C,n))) \/ (L~ (Cage (C,n))) by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA21: not q in L~ (Cage (C,n)) ; ::_thesis: q in (RightComp (Cage (C,n))) \/ (L~ (Cage (C,n)))
A22: LSeg (p,s) c= (L~ (Cage (C,n))) `
proof
3 <= (len (Gauge (C,n))) -' 1 by GOBRD14:7;
then A23: 1 <= (len (Gauge (C,n))) -' 1 by XXREAL_0:2;
then A24: Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) = { |[x,y]| where x, y is Real : ( ((Gauge (C,n)) * (k,1)) `1 < x & x < ((Gauge (C,n)) * ((k + 1),1)) `1 & ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 < y & y < ((Gauge (C,n)) * (1,(((len (Gauge (C,n))) -' 1) + 1))) `2 ) } by A1, A5, A11, A18, A19, GOBOARD6:26;
A25: cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1)) = { |[m,o]| where m, o is Real : ( ((Gauge (C,n)) * (k,1)) `1 <= m & m <= ((Gauge (C,n)) * ((k + 1),1)) `1 & ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 <= o & o <= ((Gauge (C,n)) * (1,(((len (Gauge (C,n))) -' 1) + 1))) `2 ) } by A1, A5, A11, A18, A19, A23, GOBRD11:32;
Fr (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) c= cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1)) by A9, A12, GOBRD13:30, TOPS_1:35;
then q in cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1)) by A17;
then consider m, o being Real such that
A26: s = |[m,o]| and
A27: ((Gauge (C,n)) * (k,1)) `1 <= m and
A28: m <= ((Gauge (C,n)) * ((k + 1),1)) `1 and
A29: ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 <= o and
A30: o <= ((Gauge (C,n)) * (1,(((len (Gauge (C,n))) -' 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: ((Gauge (C,n)) * (k,1)) `1 < x and
A34: x < ((Gauge (C,n)) * ((k + 1),1)) `1 and
A35: ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 < y and
A36: y < ((Gauge (C,n)) * (1,(((len (Gauge (C,n))) -' 1) + 1))) `2 by A20, A24;
A37: p `1 = x by A32, EUCLID:52;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in LSeg (p,s) or a in (L~ (Cage (C,n))) ` )
assume A38: a in LSeg (p,s) ; ::_thesis: a in (L~ (Cage (C,n))) `
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__::_thesis:_(_(_b_=_s_&_a_in_(L~_(Cage_(C,n)))_`_)_or_(_b_<>_s_&_a_in_(L~_(Cage_(C,n)))_`_)_)
percases ( b = s or b <> s ) ;
case b = s ; ::_thesis: a in (L~ (Cage (C,n))) `
hence a in (L~ (Cage (C,n))) ` by A21, SUBSET_1:29; ::_thesis: verum
end;
caseA42: b <> s ; ::_thesis: a in (L~ (Cage (C,n))) `
now__::_thesis:_(_(_s_`1_<_p_`1_&_s_`2_<_p_`2_&_b_in_Int_(cell_((Gauge_(C,n)),k,((len_(Gauge_(C,n)))_-'_1)))_)_or_(_s_`1_<_p_`1_&_s_`2_>_p_`2_&_b_in_Int_(cell_((Gauge_(C,n)),k,((len_(Gauge_(C,n)))_-'_1)))_)_or_(_s_`1_<_p_`1_&_s_`2_=_p_`2_&_b_in_Int_(cell_((Gauge_(C,n)),k,((len_(Gauge_(C,n)))_-'_1)))_)_or_(_s_`1_>_p_`1_&_s_`2_<_p_`2_&_b_in_Int_(cell_((Gauge_(C,n)),k,((len_(Gauge_(C,n)))_-'_1)))_)_or_(_s_`1_>_p_`1_&_s_`2_>_p_`2_&_b_in_Int_(cell_((Gauge_(C,n)),k,((len_(Gauge_(C,n)))_-'_1)))_)_or_(_s_`1_>_p_`1_&_s_`2_=_p_`2_&_b_in_Int_(cell_((Gauge_(C,n)),k,((len_(Gauge_(C,n)))_-'_1)))_)_or_(_s_`1_=_p_`1_&_s_`2_>_p_`2_&_b_in_Int_(cell_((Gauge_(C,n)),k,((len_(Gauge_(C,n)))_-'_1)))_)_or_(_s_`1_=_p_`1_&_s_`2_<_p_`2_&_b_in_Int_(cell_((Gauge_(C,n)),k,((len_(Gauge_(C,n)))_-'_1)))_)_or_(_s_`1_=_p_`1_&_s_`2_=_p_`2_&_b_in_Int_(cell_((Gauge_(C,n)),k,((len_(Gauge_(C,n)))_-'_1)))_)_)
percases ( ( s `1 < p `1 & s `2 < p `2 ) or ( s `1 < p `1 & s `2 > p `2 ) or ( s `1 < p `1 & s `2 = p `2 ) or ( s `1 > p `1 & s `2 < p `2 ) or ( s `1 > p `1 & s `2 > p `2 ) or ( s `1 > p `1 & s `2 = p `2 ) or ( s `1 = p `1 & s `2 > p `2 ) or ( s `1 = p `1 & s `2 < p `2 ) or ( s `1 = p `1 & s `2 = p `2 ) ) by XXREAL_0:1;
caseA43: ( s `1 < p `1 & s `2 < p `2 ) ; ::_thesis: b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1)))
then s `2 < b `2 by A38, A42, TOPREAL6:30;
then A44: ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 < b `2 by A29, A31, XXREAL_0:2;
b `1 <= p `1 by A38, A43, TOPREAL6:29;
then A45: b `1 < ((Gauge (C,n)) * ((k + 1),1)) `1 by A34, A37, XXREAL_0:2;
b `2 <= p `2 by A38, A43, TOPREAL6:30;
then A46: b `2 < ((Gauge (C,n)) * (1,(((len (Gauge (C,n))) -' 1) + 1))) `2 by A36, A40, XXREAL_0:2;
s `1 < b `1 by A38, A42, A43, TOPREAL6:29;
then ((Gauge (C,n)) * (k,1)) `1 < b `1 by A27, A41, XXREAL_0:2;
hence b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) by A24, A39, A45, A44, A46; ::_thesis: verum
end;
caseA47: ( s `1 < p `1 & s `2 > p `2 ) ; ::_thesis: b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1)))
then b `2 < s `2 by A38, A42, TOPREAL6:30;
then A48: b `2 < ((Gauge (C,n)) * (1,(((len (Gauge (C,n))) -' 1) + 1))) `2 by A30, A31, XXREAL_0:2;
b `1 <= p `1 by A38, A47, TOPREAL6:29;
then A49: b `1 < ((Gauge (C,n)) * ((k + 1),1)) `1 by A34, A37, XXREAL_0:2;
p `2 <= b `2 by A38, A47, TOPREAL6:30;
then A50: ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 < b `2 by A35, A40, XXREAL_0:2;
s `1 < b `1 by A38, A42, A47, TOPREAL6:29;
then ((Gauge (C,n)) * (k,1)) `1 < b `1 by A27, A41, XXREAL_0:2;
hence b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) by A24, A39, A49, A50, A48; ::_thesis: verum
end;
caseA51: ( s `1 < p `1 & s `2 = p `2 ) ; ::_thesis: b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1)))
then b `1 <= p `1 by A38, TOPREAL6:29;
then A52: b `1 < ((Gauge (C,n)) * ((k + 1),1)) `1 by A34, A37, XXREAL_0:2;
s `1 < b `1 by A38, A42, A51, TOPREAL6:29;
then A53: ((Gauge (C,n)) * (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 ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) by A24, A39, A35, A36, A40, A53, A52; ::_thesis: verum
end;
caseA54: ( s `1 > p `1 & s `2 < p `2 ) ; ::_thesis: b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1)))
then s `2 < b `2 by A38, A42, TOPREAL6:30;
then A55: ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 < b `2 by A29, A31, XXREAL_0:2;
b `1 >= p `1 by A38, A54, TOPREAL6:29;
then A56: ((Gauge (C,n)) * (k,1)) `1 < b `1 by A33, A37, XXREAL_0:2;
b `2 <= p `2 by A38, A54, TOPREAL6:30;
then A57: b `2 < ((Gauge (C,n)) * (1,(((len (Gauge (C,n))) -' 1) + 1))) `2 by A36, A40, XXREAL_0:2;
s `1 > b `1 by A38, A42, A54, TOPREAL6:29;
then b `1 < ((Gauge (C,n)) * ((k + 1),1)) `1 by A28, A41, XXREAL_0:2;
hence b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) by A24, A39, A56, A55, A57; ::_thesis: verum
end;
caseA58: ( s `1 > p `1 & s `2 > p `2 ) ; ::_thesis: b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1)))
then s `2 > b `2 by A38, A42, TOPREAL6:30;
then A59: b `2 < ((Gauge (C,n)) * (1,(((len (Gauge (C,n))) -' 1) + 1))) `2 by A30, A31, XXREAL_0:2;
b `1 >= p `1 by A38, A58, TOPREAL6:29;
then A60: ((Gauge (C,n)) * (k,1)) `1 < b `1 by A33, A37, XXREAL_0:2;
b `2 >= p `2 by A38, A58, TOPREAL6:30;
then A61: ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 < b `2 by A35, A40, XXREAL_0:2;
s `1 > b `1 by A38, A42, A58, TOPREAL6:29;
then b `1 < ((Gauge (C,n)) * ((k + 1),1)) `1 by A28, A41, XXREAL_0:2;
hence b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) by A24, A39, A60, A61, A59; ::_thesis: verum
end;
caseA62: ( s `1 > p `1 & s `2 = p `2 ) ; ::_thesis: b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1)))
then b `1 >= p `1 by A38, TOPREAL6:29;
then A63: ((Gauge (C,n)) * (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 < ((Gauge (C,n)) * ((k + 1),1)) `1 by A28, A41, XXREAL_0:2;
b `2 = p `2 by A38, A62, GOBOARD7:6;
hence b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) by A24, A39, A35, A36, A40, A63, A64; ::_thesis: verum
end;
caseA65: ( s `1 = p `1 & s `2 > p `2 ) ; ::_thesis: b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1)))
then b `2 >= p `2 by A38, TOPREAL6:30;
then A66: ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 < b `2 by A35, A40, XXREAL_0:2;
s `2 > b `2 by A38, A42, A65, TOPREAL6:30;
then A67: b `2 < ((Gauge (C,n)) * (1,(((len (Gauge (C,n))) -' 1) + 1))) `2 by A30, A31, XXREAL_0:2;
b `1 = p `1 by A38, A65, GOBOARD7:5;
hence b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) by A24, A39, A33, A34, A37, A66, A67; ::_thesis: verum
end;
caseA68: ( s `1 = p `1 & s `2 < p `2 ) ; ::_thesis: b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1)))
then b `2 <= p `2 by A38, TOPREAL6:30;
then A69: b `2 < ((Gauge (C,n)) * (1,(((len (Gauge (C,n))) -' 1) + 1))) `2 by A36, A40, XXREAL_0:2;
s `2 < b `2 by A38, A42, A68, TOPREAL6:30;
then A70: ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 < b `2 by A29, A31, XXREAL_0:2;
b `1 = p `1 by A38, A68, GOBOARD7:5;
hence b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) by A24, A39, A33, A34, A37, A70, A69; ::_thesis: verum
end;
case ( s `1 = p `1 & s `2 = p `2 ) ; ::_thesis: b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1)))
then p = s by TOPREAL3:6;
then LSeg (p,s) = {p} by RLTOPSP1:70;
hence b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) by A20, A38, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
then not b in L~ (Cage (C,n)) by A15, A14, XBOOLE_0:def_4;
hence a in (L~ (Cage (C,n))) ` by SUBSET_1:29; ::_thesis: verum
end;
end;
end;
hence a in (L~ (Cage (C,n))) ` ; ::_thesis: verum
end;
A71: s in LSeg (p,s) by RLTOPSP1:68;
now__::_thesis:_ex_a_being_Point_of_(TOP-REAL_2)_st_
(_a_in_{p}_&_a_in_LSeg_(p,s)_)
take a = p; ::_thesis: ( a in {p} & a in LSeg (p,s) )
thus ( a in {p} & a in LSeg (p,s) ) by RLTOPSP1:68, TARSKI:def_1; ::_thesis: verum
end;
then A72: {p} meets LSeg (p,s) by XBOOLE_0:3;
( RightComp (Cage (C,n)) is_a_component_of (L~ (Cage (C,n))) ` & {p} c= RightComp (Cage (C,n)) ) by A14, A20, GOBOARD9:def_2, ZFMISC_1:31;
then LSeg (p,s) c= RightComp (Cage (C,n)) by A22, A72, GOBOARD9:4;
hence q in (RightComp (Cage (C,n))) \/ (L~ (Cage (C,n))) by A71, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
C misses L~ (Cage (C,n)) by Th5;
then ( N-min C in C & C /\ (L~ (Cage (C,n))) = {} ) by SPRECT_1:11, XBOOLE_0:def_7;
then A73: not N-min C in L~ (Cage (C,n)) by XBOOLE_0:def_4;
RightComp (Cage (C,n)) c= (RightComp (Cage (C,n))) \/ (L~ (Cage (C,n))) by XBOOLE_1:7;
then Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) c= (RightComp (Cage (C,n))) \/ (L~ (Cage (C,n))) by A14, XBOOLE_1:1;
then right_cell ((Cage (C,n)),1,(Gauge (C,n))) c= (RightComp (Cage (C,n))) \/ (L~ (Cage (C,n))) by A12, A16, A10, XBOOLE_1:8;
hence N-min C in RightComp (Cage (C,n)) by A73, A4, A5, A12, XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th9: :: JORDAN10:9
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C meets RightComp (Cage (C,n))
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C meets RightComp (Cage (C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: C meets RightComp (Cage (C,n))
( 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 C meets RightComp (Cage (C,n)) by XBOOLE_0:def_7; ::_thesis: verum
end;
theorem Th10: :: JORDAN10:10
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C misses LeftComp (Cage (C,n))
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C misses LeftComp (Cage (C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: C misses LeftComp (Cage (C,n))
set f = Cage (C,n);
assume A1: C meets LeftComp (Cage (C,n)) ; ::_thesis: contradiction
RightComp (Cage (C,n)) is_a_component_of (L~ (Cage (C,n))) ` by GOBOARD9:def_2;
then A2: ex R being Subset of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) st
( R = RightComp (Cage (C,n)) & R is a_component ) by CONNSP_1:def_6;
C misses L~ (Cage (C,n)) by Th5;
then A3: C /\ (L~ (Cage (C,n))) = {} by XBOOLE_0:def_7;
C c= the carrier of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `))
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in C or c in the carrier of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) )
assume A4: c in C ; ::_thesis: c in the carrier of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `))
then not c in L~ (Cage (C,n)) by A3, XBOOLE_0:def_4;
then c in (L~ (Cage (C,n))) ` by A4, SUBSET_1:29;
hence c in the carrier of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) by PRE_TOPC:8; ::_thesis: verum
end;
then reconsider C1 = C as Subset of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) ;
LeftComp (Cage (C,n)) is_a_component_of (L~ (Cage (C,n))) ` by GOBOARD9:def_1;
then A5: ex L being Subset of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) st
( L = LeftComp (Cage (C,n)) & L is a_component ) by CONNSP_1:def_6;
( C meets RightComp (Cage (C,n)) & C1 is connected ) by Th9, CONNSP_1:23;
hence contradiction by A1, A5, A2, JORDAN2C:92, SPRECT_4:6; ::_thesis: verum
end;
theorem Th11: :: JORDAN10:11
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C c= RightComp (Cage (C,n))
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C c= RightComp (Cage (C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: C c= RightComp (Cage (C,n))
set f = Cage (C,n);
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in C or c in RightComp (Cage (C,n)) )
assume A1: c in C ; ::_thesis: c in RightComp (Cage (C,n))
C misses L~ (Cage (C,n)) by Th5;
then C /\ (L~ (Cage (C,n))) = {} by XBOOLE_0:def_7;
then A2: not c in L~ (Cage (C,n)) by A1, XBOOLE_0:def_4;
C misses LeftComp (Cage (C,n)) by Th10;
then C /\ (LeftComp (Cage (C,n))) = {} by XBOOLE_0:def_7;
then not c in LeftComp (Cage (C,n)) by A1, XBOOLE_0:def_4;
hence c in RightComp (Cage (C,n)) by A1, A2, GOBRD14:18; ::_thesis: verum
end;
theorem Th12: :: JORDAN10:12
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C c= BDD (L~ (Cage (C,n)))
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C c= BDD (L~ (Cage (C,n)))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: C c= BDD (L~ (Cage (C,n)))
( C c= RightComp (Cage (C,n)) & RightComp (Cage (C,n)) c= BDD (L~ (Cage (C,n))) ) by Th11, GOBRD14:35, JORDAN2C:22;
hence C c= BDD (L~ (Cage (C,n))) by XBOOLE_1:1; ::_thesis: verum
end;
theorem Th13: :: JORDAN10:13
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds UBD (L~ (Cage (C,n))) c= UBD C
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds UBD (L~ (Cage (C,n))) c= UBD C
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: UBD (L~ (Cage (C,n))) c= UBD C
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UBD (L~ (Cage (C,n))) or x in UBD C )
A2: 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_5;
assume x in UBD (L~ (Cage (C,n))) ; ::_thesis: x in UBD C
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~ (Cage (C,n)) } 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~ (Cage (C,n)) by A4;
reconsider B1 = B as Subset of (Euclid 2) by TOPREAL3:8;
A7: B1 misses RightComp (Cage (C,n)) by A6, GOBRD14:35, JORDAN2C:118;
then A8: B1 /\ (RightComp (Cage (C,n))) = {} by XBOOLE_0:def_7;
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~ (Cage (C,n))) ` by A6, JORDAN2C:def_3;
then consider B2 being Subset of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) 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 (Cage (C,n)) 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B or a in C ` )
assume A16: a in B ; ::_thesis: a in C `
then not a in C by A12, A8, XBOOLE_0:def_4;
hence a in C ` by A16, XBOOLE_0:def_5; ::_thesis: verum
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 x in UBD C by A1, A13, A15, TARSKI:def_4; ::_thesis: verum
end;
definition
let C be compact non horizontal non vertical Subset of (TOP-REAL 2);
func UBD-Family C -> set equals :: JORDAN10:def 1
{ (UBD (L~ (Cage (C,n)))) where n is Element of NAT : verum } ;
coherence
{ (UBD (L~ (Cage (C,n)))) where n is Element of NAT : verum } is set ;
func BDD-Family C -> set equals :: JORDAN10:def 2
{ (Cl (BDD (L~ (Cage (C,n))))) where n is Element of NAT : verum } ;
coherence
{ (Cl (BDD (L~ (Cage (C,n))))) where n is Element of NAT : verum } is set ;
end;
:: deftheorem defines UBD-Family JORDAN10:def_1_:_
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds UBD-Family C = { (UBD (L~ (Cage (C,n)))) where n is Element of NAT : verum } ;
:: deftheorem defines BDD-Family JORDAN10:def_2_:_
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD-Family C = { (Cl (BDD (L~ (Cage (C,n))))) where n is Element of NAT : verum } ;
definition
let C be compact non horizontal non vertical Subset of (TOP-REAL 2);
:: original: UBD-Family
redefine func UBD-Family C -> Subset-Family of (TOP-REAL 2);
coherence
UBD-Family C is Subset-Family of (TOP-REAL 2)
proof
{ (UBD (L~ (Cage (C,i)))) where i is Element of NAT : verum } c= bool the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (UBD (L~ (Cage (C,i)))) where i is Element of NAT : verum } or x in bool the carrier of (TOP-REAL 2) )
assume x in { (UBD (L~ (Cage (C,i)))) where i is Element of NAT : verum } ; ::_thesis: x in bool the carrier of (TOP-REAL 2)
then ex i being Element of NAT st x = UBD (L~ (Cage (C,i))) ;
hence x in bool the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
hence UBD-Family C is Subset-Family of (TOP-REAL 2) ; ::_thesis: verum
end;
:: original: BDD-Family
redefine func BDD-Family C -> Subset-Family of (TOP-REAL 2);
coherence
BDD-Family C is Subset-Family of (TOP-REAL 2)
proof
{ (Cl (BDD (L~ (Cage (C,i))))) where i is Element of NAT : verum } c= bool the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (Cl (BDD (L~ (Cage (C,i))))) where i is Element of NAT : verum } or x in bool the carrier of (TOP-REAL 2) )
assume x in { (Cl (BDD (L~ (Cage (C,i))))) where i is Element of NAT : verum } ; ::_thesis: x in bool the carrier of (TOP-REAL 2)
then ex i being Element of NAT st x = Cl (BDD (L~ (Cage (C,i)))) ;
hence x in bool the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
hence BDD-Family C is Subset-Family of (TOP-REAL 2) ; ::_thesis: verum
end;
end;
registration
let C be compact non horizontal non vertical Subset of (TOP-REAL 2);
cluster UBD-Family C -> non empty ;
coherence
not UBD-Family C is empty
proof
UBD (L~ (Cage (C,0))) in UBD-Family C ;
hence not UBD-Family C is empty ; ::_thesis: verum
end;
cluster BDD-Family C -> non empty ;
coherence
not BDD-Family C is empty
proof
Cl (BDD (L~ (Cage (C,0)))) in BDD-Family C ;
hence not BDD-Family C is empty ; ::_thesis: verum
end;
end;
theorem Th14: :: JORDAN10:14
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds union (UBD-Family C) = UBD C
proof
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: union (UBD-Family C) = UBD C
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 ; ::_thesis: ( X in UBD-Family C implies X c= UBD C )
assume X in UBD-Family C ; ::_thesis: X c= UBD C
then ex n being Element of NAT st X = UBD (L~ (Cage (C,n))) ;
hence X c= UBD C by Th13; ::_thesis: verum
end;
hence union (UBD-Family C) c= UBD C by ZFMISC_1:76; :: according to XBOOLE_0:def_10 ::_thesis: UBD C c= union (UBD-Family C)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UBD C or x in union (UBD-Family C) )
assume A2: x in UBD C ; ::_thesis: x in union (UBD-Family 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 being Subset of (TOP-REAL 2) 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 = 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;
( not L~ f is empty & TopStruct(# the carrier of (TOP-REAL 2), the topology 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 min_dist_min (P1,C1) > 0 by JGRAPH_1:38;
then (min_dist_min (P1,C1)) / 2 > 0 by XREAL_1:139;
then consider n being Element of NAT such that
1 < n and
A13: ( dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < (min_dist_min (P1,C1)) / 2 & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < (min_dist_min (P1,C1)) / 2 ) by GOBRD14:11;
set G = Gauge (C,n);
set g = Cage (C,n);
A14: UBD (L~ (Cage (C,n))) in UBD-Family C ;
A15: now__::_thesis:_not_(L~_(Cage_(C,n)))_/\_P_<>_{}
assume (L~ (Cage (C,n))) /\ P <> {} ; ::_thesis: contradiction
then consider a being set such that
A16: a in (L~ (Cage (C,n))) /\ P by XBOOLE_0:def_1;
a in L~ (Cage (C,n)) by A16, XBOOLE_0:def_4;
then consider i being Element of NAT such that
A17: ( 1 <= i & i + 1 <= len (Cage (C,n)) ) and
A18: a in LSeg ((Cage (C,n)),i) by SPPOL_2:13;
right_cell ((Cage (C,n)),i,(Gauge (C,n))) meets C by A17, JORDAN9:31;
then consider c being set such that
A19: c in (right_cell ((Cage (C,n)),i,(Gauge (C,n)))) /\ C by XBOOLE_0:4;
reconsider c = 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: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
then consider i1, j1, i2, j2 being Element of NAT such that
A22: [i1,j1] in Indices (Gauge (C,n)) and
A23: (Cage (C,n)) /. i = (Gauge (C,n)) * (i1,j1) and
A24: [i2,j2] in Indices (Gauge (C,n)) and
A25: (Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (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 ((Cage (C,n)),i,(Gauge (C,n)))) /\ (right_cell ((Cage (C,n)),i,(Gauge (C,n)))) = LSeg ((Cage (C,n)),i) by A17, A21, GOBRD13:29;
then A27: a in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by A18, XBOOLE_0:def_4;
a in P by A16, XBOOLE_0:def_4;
then A28: dist (a9,c) >= min_dist_min (P1,C1) by A20, WEIERSTR:34;
reconsider A = a as Point of (TOP-REAL 2) by A16;
set e = E-bound C;
set w = W-bound C;
set p = N-bound C;
set s = S-bound C;
A29: 4 <= len (Gauge (C,n)) by JORDAN8:10;
then A30: 1 <= len (Gauge (C,n)) by XXREAL_0:2;
A31: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
then A32: 1 <= width (Gauge (C,n)) by A29, XXREAL_0:2;
A33: [1,1] in Indices (Gauge (C,n)) by A31, A30, MATRIX_1:36;
A34: c in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by A19, XBOOLE_0:def_4;
now__::_thesis:_(_(_i1_=_i2_&_j1_+_1_=_j2_&_dist_(A,c9)_<=_(((N-bound_C)_-_(S-bound_C))_/_(2_|^_n))_+_(((E-bound_C)_-_(W-bound_C))_/_(2_|^_n))_)_or_(_i1_+_1_=_i2_&_j1_=_j2_&_dist_(A,c9)_<=_(((N-bound_C)_-_(S-bound_C))_/_(2_|^_n))_+_(((E-bound_C)_-_(W-bound_C))_/_(2_|^_n))_)_or_(_i1_=_i2_+_1_&_j1_=_j2_&_dist_(A,c9)_<=_(((N-bound_C)_-_(S-bound_C))_/_(2_|^_n))_+_(((E-bound_C)_-_(W-bound_C))_/_(2_|^_n))_)_or_(_i1_=_i2_&_j1_=_j2_+_1_&_dist_(A,c9)_<=_(((N-bound_C)_-_(S-bound_C))_/_(2_|^_n))_+_(((E-bound_C)_-_(W-bound_C))_/_(2_|^_n))_)_)
percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A26;
caseA35: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n))
then A36: i1 < len (Gauge (C,n)) by A17, A22, A23, A24, A25, Th1;
then A37: i1 + 1 <= len (Gauge (C,n)) by NAT_1:13;
A38: 1 <= i1 by A22, MATRIX_1:38;
then 1 <= i1 + 1 by NAT_1:13;
then A39: [(i1 + 1),1] in Indices (Gauge (C,n)) by A32, A37, MATRIX_1:36;
[i1,1] in Indices (Gauge (C,n)) by A32, A38, A36, MATRIX_1:36;
then A40: ( dist (((Gauge (C,n)) * (i1,1)),((Gauge (C,n)) * ((i1 + 1),1))) = (((Gauge (C,n)) * ((i1 + 1),1)) `1) - (((Gauge (C,n)) * (i1,1)) `1) & dist (((Gauge (C,n)) * (i1,1)),((Gauge (C,n)) * ((i1 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ n) ) by A39, GOBRD14:5, GOBRD14:10;
A41: j1 + 1 <= width (Gauge (C,n)) by A24, A35, MATRIX_1:38;
then A42: j1 < width (Gauge (C,n)) by NAT_1:13;
A43: 1 <= j1 by A22, MATRIX_1:38;
then 1 <= j1 + 1 by NAT_1:13;
then A44: [1,(j1 + 1)] in Indices (Gauge (C,n)) by A30, A41, MATRIX_1:36;
A45: right_cell ((Cage (C,n)),i,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,j1) by A17, A21, A22, A23, A24, A25, A35, GOBRD13:22
.= { |[r,t]| where r, t is Real : ( ((Gauge (C,n)) * (i1,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= t & t <= ((Gauge (C,n)) * (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: ( ((Gauge (C,n)) * (i1,1)) `1 <= aa & aa <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= ab & ab <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) by A27;
A48: ( A `1 = aa & A `2 = ab ) by A46, EUCLID:52;
[1,j1] in Indices (Gauge (C,n)) by A30, A43, A42, MATRIX_1:36;
then A49: ( dist (((Gauge (C,n)) * (1,j1)),((Gauge (C,n)) * (1,(j1 + 1)))) = (((Gauge (C,n)) * (1,(j1 + 1))) `2) - (((Gauge (C,n)) * (1,j1)) `2) & dist (((Gauge (C,n)) * (1,j1)),((Gauge (C,n)) * (1,(j1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n) ) by A44, GOBRD14:6, GOBRD14:9;
consider r, t being Real such that
A50: c = |[r,t]| and
A51: ( ((Gauge (C,n)) * (i1,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= t & t <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) by A34, A45;
( c9 `1 = r & c9 `2 = t ) by A50, EUCLID:52;
hence dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) by A51, A47, A48, A49, A40, TOPREAL6:95; ::_thesis: verum
end;
caseA52: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n))
then A53: i1 + 1 <= len (Gauge (C,n)) by A24, MATRIX_1:38;
then A54: i1 < len (Gauge (C,n)) by NAT_1:13;
A55: 1 <= i1 by A22, MATRIX_1:38;
then 1 <= i1 + 1 by NAT_1:13;
then A56: [(i1 + 1),1] in Indices (Gauge (C,n)) by A32, A53, MATRIX_1:36;
[i1,1] in Indices (Gauge (C,n)) by A32, A55, A54, MATRIX_1:36;
then A57: ( dist (((Gauge (C,n)) * (i1,1)),((Gauge (C,n)) * ((i1 + 1),1))) = (((Gauge (C,n)) * ((i1 + 1),1)) `1) - (((Gauge (C,n)) * (i1,1)) `1) & dist (((Gauge (C,n)) * (i1,1)),((Gauge (C,n)) * ((i1 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ n) ) by A56, GOBRD14:5, GOBRD14:10;
A58: j2 <= width (Gauge (C,n)) by A24, MATRIX_1:38;
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 (Gauge (C,n))) - 1 < (width (Gauge (C,n))) - 0 by XREAL_1:15;
then A62: j2 -' 1 < width (Gauge (C,n)) by A60, A58, XREAL_1:15;
then A63: [1,(j2 -' 1)] in Indices (Gauge (C,n)) by A30, A61, MATRIX_1:36;
A64: right_cell ((Cage (C,n)),i,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,(j2 -' 1)) by A17, A21, A22, A23, A24, A25, A52, GOBRD13:24
.= { |[r,t]| where r, t is Real : ( ((Gauge (C,n)) * (i1,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,(j2 -' 1))) `2 <= t & t <= ((Gauge (C,n)) * (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: ( ((Gauge (C,n)) * (i1,1)) `1 <= aa & aa <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,(j2 -' 1))) `2 <= ab & ab <= ((Gauge (C,n)) * (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 (Gauge (C,n)) by A30, A60, A58, MATRIX_1:36;
then A68: ( dist (((Gauge (C,n)) * (1,(j2 -' 1))),((Gauge (C,n)) * (1,((j2 -' 1) + 1)))) = (((Gauge (C,n)) * (1,((j2 -' 1) + 1))) `2) - (((Gauge (C,n)) * (1,(j2 -' 1))) `2) & dist (((Gauge (C,n)) * (1,(j2 -' 1))),((Gauge (C,n)) * (1,((j2 -' 1) + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n) ) by A63, GOBRD14:6, GOBRD14:9;
consider r, t being Real such that
A69: c = |[r,t]| and
A70: ( ((Gauge (C,n)) * (i1,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,(j2 -' 1))) `2 <= t & t <= ((Gauge (C,n)) * (1,((j2 -' 1) + 1))) `2 ) by A34, A64;
( c9 `1 = r & c9 `2 = t ) by A69, EUCLID:52;
hence dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) by A70, A66, A67, A68, A57, TOPREAL6:95; ::_thesis: verum
end;
caseA71: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n))
A72: 1 <= j1 + 1 by NAT_1:12;
A73: j1 < width (Gauge (C,n)) by A17, A22, A23, A24, A25, A71, Th4;
then j1 + 1 <= width (Gauge (C,n)) by NAT_1:13;
then A74: [1,(j1 + 1)] in Indices (Gauge (C,n)) by A30, A72, MATRIX_1:36;
A75: 1 <= j1 by A22, MATRIX_1:38;
then [1,j1] in Indices (Gauge (C,n)) by A30, A73, MATRIX_1:36;
then A76: ( dist (((Gauge (C,n)) * (1,j1)),((Gauge (C,n)) * (1,(j1 + 1)))) = (((Gauge (C,n)) * (1,(j1 + 1))) `2) - (((Gauge (C,n)) * (1,j1)) `2) & dist (((Gauge (C,n)) * (1,j1)),((Gauge (C,n)) * (1,(j1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n) ) by A74, GOBRD14:6, GOBRD14:9;
A77: i2 + 1 <= len (Gauge (C,n)) by A22, A71, MATRIX_1:38;
then A78: i2 < len (Gauge (C,n)) by NAT_1:13;
A79: 1 <= i2 by A24, MATRIX_1:38;
then 1 <= i2 + 1 by NAT_1:13;
then A80: [(i2 + 1),1] in Indices (Gauge (C,n)) by A32, A77, MATRIX_1:36;
A81: right_cell ((Cage (C,n)),i,(Gauge (C,n))) = cell ((Gauge (C,n)),i2,j1) by A17, A21, A22, A23, A24, A25, A71, GOBRD13:26
.= { |[r,t]| where r, t is Real : ( ((Gauge (C,n)) * (i2,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i2 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= t & t <= ((Gauge (C,n)) * (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: ( ((Gauge (C,n)) * (i2,1)) `1 <= aa & aa <= ((Gauge (C,n)) * ((i2 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= ab & ab <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) by A27;
A84: ( A `1 = aa & A `2 = ab ) by A82, EUCLID:52;
[i2,1] in Indices (Gauge (C,n)) by A32, A79, A78, MATRIX_1:36;
then A85: ( dist (((Gauge (C,n)) * (i2,1)),((Gauge (C,n)) * ((i2 + 1),1))) = (((Gauge (C,n)) * ((i2 + 1),1)) `1) - (((Gauge (C,n)) * (i2,1)) `1) & dist (((Gauge (C,n)) * (i2,1)),((Gauge (C,n)) * ((i2 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ n) ) by A80, GOBRD14:5, GOBRD14:10;
consider r, t being Real such that
A86: c = |[r,t]| and
A87: ( ((Gauge (C,n)) * (i2,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i2 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= t & t <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) by A34, A81;
( c9 `1 = r & c9 `2 = t ) by A86, EUCLID:52;
hence dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) by A87, A83, A84, A76, A85, TOPREAL6:95; ::_thesis: verum
end;
caseA88: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n))
then A89: j2 + 1 <= width (Gauge (C,n)) by A22, MATRIX_1:38;
then A90: j2 < width (Gauge (C,n)) by NAT_1:13;
A91: 1 <= j2 by A24, MATRIX_1:38;
then 1 <= j2 + 1 by NAT_1:13;
then A92: [1,(j2 + 1)] in Indices (Gauge (C,n)) by A30, A89, MATRIX_1:36;
[1,j2] in Indices (Gauge (C,n)) by A30, A91, A90, MATRIX_1:36;
then A93: ( dist (((Gauge (C,n)) * (1,j2)),((Gauge (C,n)) * (1,(j2 + 1)))) = (((Gauge (C,n)) * (1,(j2 + 1))) `2) - (((Gauge (C,n)) * (1,j2)) `2) & dist (((Gauge (C,n)) * (1,j2)),((Gauge (C,n)) * (1,(j2 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n) ) by A92, GOBRD14:6, GOBRD14:9;
A94: i1 <= len (Gauge (C,n)) by A22, MATRIX_1:38;
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 (Gauge (C,n))) - 1 < (len (Gauge (C,n))) - 0 by XREAL_1:15;
then A98: i1 -' 1 < len (Gauge (C,n)) by A96, A94, XREAL_1:15;
then A99: [(i1 -' 1),1] in Indices (Gauge (C,n)) by A32, A97, MATRIX_1:36;
A100: right_cell ((Cage (C,n)),i,(Gauge (C,n))) = cell ((Gauge (C,n)),(i1 -' 1),j2) by A17, A21, A22, A23, A24, A25, A88, GOBRD13:28
.= { |[r,t]| where r, t is Real : ( ((Gauge (C,n)) * ((i1 -' 1),1)) `1 <= r & r <= ((Gauge (C,n)) * (((i1 -' 1) + 1),1)) `1 & ((Gauge (C,n)) * (1,j2)) `2 <= t & t <= ((Gauge (C,n)) * (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: ( ((Gauge (C,n)) * ((i1 -' 1),1)) `1 <= aa & aa <= ((Gauge (C,n)) * (((i1 -' 1) + 1),1)) `1 & ((Gauge (C,n)) * (1,j2)) `2 <= ab & ab <= ((Gauge (C,n)) * (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 (Gauge (C,n)) by A32, A96, A94, MATRIX_1:36;
then A104: ( dist (((Gauge (C,n)) * ((i1 -' 1),1)),((Gauge (C,n)) * (((i1 -' 1) + 1),1))) = (((Gauge (C,n)) * (((i1 -' 1) + 1),1)) `1) - (((Gauge (C,n)) * ((i1 -' 1),1)) `1) & dist (((Gauge (C,n)) * ((i1 -' 1),1)),((Gauge (C,n)) * (((i1 -' 1) + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ n) ) by A99, GOBRD14:5, GOBRD14:10;
consider r, t being Real such that
A105: c = |[r,t]| and
A106: ( ((Gauge (C,n)) * ((i1 -' 1),1)) `1 <= r & r <= ((Gauge (C,n)) * (((i1 -' 1) + 1),1)) `1 & ((Gauge (C,n)) * (1,j2)) `2 <= t & t <= ((Gauge (C,n)) * (1,(j2 + 1))) `2 ) by A34, A100;
( c9 `1 = r & c9 `2 = t ) by A105, EUCLID:52;
hence dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) by A106, A102, A103, A93, A104, TOPREAL6:95; ::_thesis: verum
end;
end;
end;
then A107: dist (a9,c) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) by TOPREAL6:def_1;
1 + 1 <= len (Gauge (C,n)) by A29, XXREAL_0:2;
then [(1 + 1),1] in Indices (Gauge (C,n)) by A32, MATRIX_1:36;
then A108: dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * ((1 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ n) by A33, GOBRD14:10;
1 + 1 <= width (Gauge (C,n)) by A31, A29, XXREAL_0:2;
then [1,(1 + 1)] in Indices (Gauge (C,n)) by A30, MATRIX_1:36;
then dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,(1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n) by A33, GOBRD14:9;
then (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) < ((min_dist_min (P1,C1)) / 2) + ((min_dist_min (P1,C1)) / 2) by A13, A108, XREAL_1:8;
hence contradiction by A28, A107, XXREAL_0:2; ::_thesis: verum
end;
A109: P c= (L~ (Cage (C,n))) `
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in P or a in (L~ (Cage (C,n))) ` )
assume A110: a in P ; ::_thesis: a in (L~ (Cage (C,n))) `
then not a in L~ (Cage (C,n)) by A15, XBOOLE_0:def_4;
hence a in (L~ (Cage (C,n))) ` by A110, SUBSET_1:29; ::_thesis: verum
end;
( 0 < n or 0 = n ) by NAT_1:2;
then N-bound (L~ (Cage (C,0))) >= N-bound (L~ (Cage (C,n))) by Th7;
then ( (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) & q `2 > N-bound (L~ (Cage (C,n))) ) by A5, JORDAN9:32, XXREAL_0:2;
then q in LeftComp (Cage (C,n)) by JORDAN2C:113;
then q in UBD (L~ (Cage (C,n))) by GOBRD14:36;
then A111: {q} c= UBD (L~ (Cage (C,n))) by ZFMISC_1:31;
A112: P is_an_arc_of p,q by A7, TOPREAL4:2;
now__::_thesis:_ex_a_being_Point_of_(TOP-REAL_2)_st_
(_a_in_{q}_&_a_in_P_)
take a = q; ::_thesis: ( a in {q} & a in P )
thus ( a in {q} & a in P ) by A112, TARSKI:def_1, TOPREAL1:1; ::_thesis: verum
end;
then A113: {q} meets P by XBOOLE_0:3;
UBD (L~ (Cage (C,n))) is_outside_component_of L~ (Cage (C,n)) by JORDAN2C:68;
then ex E being Subset of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) st
( E = UBD (L~ (Cage (C,n))) & E is a_component & E is not bounded Subset of (Euclid 2) ) by JORDAN2C:14;
then UBD (L~ (Cage (C,n))) is_a_component_of (L~ (Cage (C,n))) ` by CONNSP_1:def_6;
then P c= UBD (L~ (Cage (C,n))) by A109, A112, A111, A113, GOBOARD9:4, JORDAN6:10;
hence x in union (UBD-Family C) by A12, A14, TARSKI:def_4; ::_thesis: verum
end;
theorem Th15: :: JORDAN10:15
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C c= meet (BDD-Family C)
proof
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: C c= meet (BDD-Family C)
for Z being set st Z in BDD-Family C holds
C c= Z
proof
let Z be set ; ::_thesis: ( Z in BDD-Family C implies C c= Z )
assume Z in BDD-Family C ; ::_thesis: C c= Z
then consider k being Element of 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 C c= Z by A1, XBOOLE_1:1; ::_thesis: verum
end;
hence C c= meet (BDD-Family C) by SETFAM_1:5; ::_thesis: verum
end;
theorem Th16: :: JORDAN10:16
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C misses LeftComp (Cage (C,n))
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C misses LeftComp (Cage (C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: BDD C misses LeftComp (Cage (C,n))
set f = Cage (C,n);
assume (BDD C) /\ (LeftComp (Cage (C,n))) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider x being Point of (TOP-REAL 2) such that
A1: x in (BDD C) /\ (LeftComp (Cage (C,n))) by SUBSET_1:4;
BDD C misses UBD C by JORDAN2C:24;
then A2: (BDD C) /\ (UBD C) = {} by XBOOLE_0:def_7;
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 (Cage (C,n)) by A1, XBOOLE_0:def_4;
UBD (L~ (Cage (C,n))) in { (UBD (L~ (Cage (C,k)))) where k is Element of NAT : verum } ;
then not x in UBD (L~ (Cage (C,n))) by A3, TARSKI:def_4;
hence contradiction by A4, GOBRD14:36; ::_thesis: verum
end;
theorem Th17: :: JORDAN10:17
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C c= RightComp (Cage (C,n))
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C c= RightComp (Cage (C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: BDD C c= RightComp (Cage (C,n))
set f = Cage (C,n);
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in BDD C or x in RightComp (Cage (C,n)) )
LeftComp (Cage (C,n)) is_outside_component_of L~ (Cage (C,n)) by GOBRD14:34;
then A1: ( UBD (L~ (Cage (C,n))) = union { E where E is Subset of (TOP-REAL 2) : E is_outside_component_of L~ (Cage (C,n)) } & LeftComp (Cage (C,n)) in { E where E is Subset of (TOP-REAL 2) : E is_outside_component_of L~ (Cage (C,n)) } ) by JORDAN2C:def_5;
assume A2: x in BDD C ; ::_thesis: x in RightComp (Cage (C,n))
A3: now__::_thesis:_not_x_in_Cl_(LeftComp_(Cage_(C,n)))
assume x in Cl (LeftComp (Cage (C,n))) ; ::_thesis: contradiction
then BDD C meets LeftComp (Cage (C,n)) by A2, PRE_TOPC:def_7;
hence contradiction by Th16; ::_thesis: verum
end;
BDD C misses UBD C by JORDAN2C:24;
then (BDD C) /\ (UBD C) = {} by XBOOLE_0:def_7;
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~ (Cage (C,n))) in { (UBD (L~ (Cage (C,k)))) where k is Element of NAT : verum } ;
then not x in UBD (L~ (Cage (C,n))) by A4, TARSKI:def_4;
then A5: not x in LeftComp (Cage (C,n)) by A1, TARSKI:def_4;
L~ (Cage (C,n)) = (Cl (LeftComp (Cage (C,n)))) \ (LeftComp (Cage (C,n))) by GOBRD14:20;
then not x in L~ (Cage (C,n)) by A3, XBOOLE_0:def_5;
hence x in RightComp (Cage (C,n)) by A2, A5, GOBRD14:18; ::_thesis: verum
end;
theorem Th18: :: JORDAN10:18
for n being Element of NAT
for P being Subset of (TOP-REAL 2)
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st P is_inside_component_of C holds
P misses L~ (Cage (C,n))
proof
let n be Element of NAT ; ::_thesis: for P being Subset of (TOP-REAL 2)
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st P is_inside_component_of C holds
P misses L~ (Cage (C,n))
let P be Subset of (TOP-REAL 2); ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st P is_inside_component_of C holds
P misses L~ (Cage (C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( P is_inside_component_of C implies P misses L~ (Cage (C,n)) )
set f = Cage (C,n);
assume P is_inside_component_of C ; ::_thesis: P misses L~ (Cage (C,n))
then A1: P c= BDD C by JORDAN2C:22;
assume P /\ (L~ (Cage (C,n))) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider x being Point of (TOP-REAL 2) such that
A2: x in P /\ (L~ (Cage (C,n))) 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 (Cage (C,n)) by Th17;
x in L~ (Cage (C,n)) by A2, XBOOLE_0:def_4;
hence contradiction by A3, A4, GOBRD14:18; ::_thesis: verum
end;
theorem Th19: :: JORDAN10:19
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C misses L~ (Cage (C,n))
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C misses L~ (Cage (C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: BDD C misses L~ (Cage (C,n))
assume not BDD C misses L~ (Cage (C,n)) ; ::_thesis: contradiction
then consider x being set 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))) = {} by XBOOLE_0:def_7;
hence contradiction by A3, A5, A2, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th20: :: JORDAN10:20
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds COMPLEMENT (UBD-Family C) = BDD-Family C
proof
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: COMPLEMENT (UBD-Family C) = BDD-Family C
for P being Subset of (TOP-REAL 2) holds
( P in BDD-Family C iff P ` in UBD-Family C )
proof
let P be Subset of (TOP-REAL 2); ::_thesis: ( P in BDD-Family C iff P ` in UBD-Family C )
thus ( P in BDD-Family C implies P ` in UBD-Family C ) ::_thesis: ( P ` in UBD-Family C implies P in BDD-Family C )
proof
assume P in BDD-Family C ; ::_thesis: P ` in UBD-Family C
then consider k being Element of NAT 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))) ` by XBOOLE_0:def_7;
( 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 P ` in UBD-Family C ; ::_thesis: verum
end;
assume P ` in UBD-Family C ; ::_thesis: P in BDD-Family C
then consider k being Element of NAT 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)))) ` by XBOOLE_0:def_7;
then (P `) ` = Cl (RightComp (Cage (C,k))) by A6, SUBSET_1:25;
then P = Cl (BDD (L~ (Cage (C,k)))) by GOBRD14:37;
hence P in BDD-Family C ; ::_thesis: verum
end;
hence COMPLEMENT (UBD-Family C) = BDD-Family C by SETFAM_1:def_7; ::_thesis: verum
end;
theorem :: JORDAN10:21
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds meet (BDD-Family C) = C \/ (BDD C)
proof
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: meet (BDD-Family C) = C \/ (BDD C)
thus meet (BDD-Family C) c= C \/ (BDD C) :: according to XBOOLE_0:def_10 ::_thesis: C \/ (BDD C) c= meet (BDD-Family C)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet (BDD-Family C) or x in C \/ (BDD C) )
assume A1: x in meet (BDD-Family C) ; ::_thesis: x in C \/ (BDD 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;
percases ( not x in C or x in C ) ;
supposeA3: not x in C ; ::_thesis: x in C \/ (BDD 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 x in C \/ (BDD C) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x in C ; ::_thesis: x in C \/ (BDD C)
hence x in C \/ (BDD C) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
BDD C misses UBD C by JORDAN2C:24;
then A5: (BDD C) /\ (UBD C) = {} by XBOOLE_0:def_7;
A6: BDD C c= meet (BDD-Family C)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in BDD C or x in meet (BDD-Family C) )
assume A7: x in BDD C ; ::_thesis: x in meet (BDD-Family 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 ; ::_thesis: ( Y in BDD-Family C implies x in Y )
assume Y in BDD-Family C ; ::_thesis: x in Y
then consider n being Element of NAT such that
A9: Y = Cl (BDD (L~ (Cage (C,n)))) and
verum ;
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))) = {} by XBOOLE_0:def_7;
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 x in Y by A9, A13; ::_thesis: verum
end;
hence x in meet (BDD-Family C) by SETFAM_1:def_1; ::_thesis: verum
end;
C c= meet (BDD-Family C) by Th15;
hence C \/ (BDD C) c= meet (BDD-Family C) by A6, XBOOLE_1:8; ::_thesis: verum
end;