:: Some Properties of Cells and Gauges
:: by Adam Grabowski , Artur Korni{\l}owicz and Andrzej Trybulec
::
:: Received October 13, 2000
:: Copyright (c) 2000-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, TOPREAL2, SUBSET_1, PRE_TOPC, EUCLID, INT_1, ARYTM_3,
ARYTM_1, CARD_1, RELAT_1, PCOMPS_1, STRUCT_0, XXREAL_0, MATRIX_1,
JORDAN8, METRIC_1, MCART_1, TREES_1, FINSEQ_1, PSCOMP_1, NEWTON,
GOBOARD5, TARSKI, JORDAN2C, XXREAL_2, REAL_1, COMPLEX1, XXREAL_1,
XBOOLE_0, RCOMP_1, FUNCT_1, TOPREAL1, SPPOL_1, TOPS_1, SEQ_4, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, COMPLEX1, REAL_1, RELSET_1, INT_1, XXREAL_2, SEQ_4, STRUCT_0,
NAT_D, FINSEQ_1, MATRIX_0, RCOMP_1, TOPS_1, FUNCT_2, PRE_TOPC, NEWTON,
COMPTS_1, EUCLID, PCOMPS_1, METRIC_1, METRIC_6, RLTOPSP1, TOPREAL1,
TOPREAL2, GOBOARD5, JORDAN8, JORDAN2C, SPPOL_1, PSCOMP_1, TOPREAL6,
SEQ_2;
constructors REAL_1, RCOMP_1, NEWTON, TOPS_1, CONNSP_1, COMPTS_1, TBSP_1,
TOPREAL2, GOBOARD1, SPPOL_1, GOBOARD5, PSCOMP_1, JORDAN2C, TOPREAL6,
JORDAN8, NAT_D, SEQ_4, RELSET_1, FUNCSDOM, PCOMPS_1, SEQ_2, SQUARE_1,
COMSEQ_2;
registrations RELSET_1, XREAL_0, NAT_1, INT_1, MEMBERED, SEQ_2, STRUCT_0,
PRE_TOPC, COMPTS_1, EUCLID, TOPREAL1, TOPREAL2, PSCOMP_1, WAYBEL_2,
TOPREAL5, JORDAN2C, TOPREAL6, JORDAN8, VALUED_0, SPRECT_1, NEWTON,
ORDINAL1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0;
expansions TARSKI, XBOOLE_0;
theorems EUCLID, JORDAN8, PSCOMP_1, JORDAN1A, NAT_1, TOPREAL6, GOBOARD5,
GOBRD14, JORDAN2C, GOBOARD6, TOPS_1, INT_1, TOPREAL5, JORDAN9, METRIC_1,
PCOMPS_1, ABSVALUE, SPRECT_1, RELAT_1, SEQ_4, METRIC_6, TOPREAL3,
UNIFORM1, JCT_MISC, FUNCT_1, XBOOLE_0, XCMPLX_1, XREAL_1, COMPLEX1,
NEWTON, TOPREAL1, XXREAL_0, PRE_TOPC, MATRIX_0, XXREAL_2, NAT_D,
MEASURE6;
begin
reserve C for Simple_closed_curve,
i, j, n for Nat,
p for Point of TOP-REAL 2;
Lm1: now
let r be Real, j;
thus [\ r + j /] - j = [\ r /] + j - j by INT_1:28
.= [\ r /];
end;
Lm2: for a, b, c being Real st a <> 0 & b <> 0 holds (a/b)*((c/a) * b)
= c
proof
let a, b, c be Real;
assume that
A1: a <> 0 and
A2: b <> 0;
(a/b)*((c/a) * b) = (a/b)*b * (c/a) .= a * (c/a) by A2,XCMPLX_1:87
.= c by A1,XCMPLX_1:87;
hence thesis;
end;
Lm3: for p being Point of TOP-REAL 2 holds p is Point of Euclid 2
proof
let p be Point of TOP-REAL 2;
TopSpaceMetr Euclid 2 = the TopStruct of TOP-REAL 2 by EUCLID:def 8;
then the TopStruct of TOP-REAL 2 = TopStruct (#the carrier of Euclid 2,
Family_open_set Euclid 2#) by PCOMPS_1:def 5;
hence thesis;
end;
Lm4: for r being Real st r > 0 holds 2*(r/4) < r
proof
let r be Real;
A1: 2*(r/4) = r/2;
assume r > 0;
hence thesis by A1,XREAL_1:216;
end;
theorem Th1:
[i,j] in Indices Gauge(C,n) & [i+1,j] in Indices Gauge(C,n)
implies dist(Gauge(C,n)*(1,1),Gauge(C,n)*(2,1)) = Gauge(C,n)*(i+1,j)`1 - Gauge(
C,n)*(i,j)`1
proof
set G = Gauge(C,n);
assume that
A1: [i,j] in Indices G and
A2: [i+1,j] in Indices G;
A3: j <= width G by A1,MATRIX_0:32;
1 <= j by A1,MATRIX_0:32;
then
A4: 1 <= width G by A3,XXREAL_0:2;
A5: len G >= 4 by JORDAN8:10;
then 2 <= len G by XXREAL_0:2;
then
A6: [2,1] in Indices G by A4,MATRIX_0:30;
A7: dist(G*(i,j),G*(i+1,j)) = (E-bound C - W-bound C)/2|^n by A1,A2,GOBRD14:10;
1 <= len G by A5,XXREAL_0:2;
then [1,1] in Indices G by A4,MATRIX_0:30;
then dist(G*(1,1),G*(1+1,1)) = dist(G*(i,j),G*(i+1,j)) by A6,A7,GOBRD14:10
.= G*(i+1,j)`1 - G*(i,j)`1 by A1,A2,GOBRD14:5;
hence thesis;
end;
theorem Th2:
[i,j] in Indices Gauge(C,n) & [i,j+1] in Indices Gauge(C,n)
implies dist(Gauge(C,n)*(1,1),Gauge(C,n)*(1,2)) = Gauge(C,n)*(i,j+1)`2 - Gauge(
C,n)*(i,j)`2
proof
set G = Gauge(C,n);
assume that
A1: [i,j] in Indices G and
A2: [i,j+1] in Indices G;
A3: 1 <= j+1 by A2,MATRIX_0:32;
len G >= 4 by JORDAN8:10;
then
A4: 1 <= len G by XXREAL_0:2;
2|^n + 3 >= 3 by NAT_1:11;
then width G >= 3 by JORDAN1A:28;
then 2 <= width G by XXREAL_0:2;
then
A5: [1,2] in Indices G by A4,MATRIX_0:30;
j + 1 <= width G by A2,MATRIX_0:32;
then 1 <= width G by A3,XXREAL_0:2;
then
A6: [1,1] in Indices G by A4,MATRIX_0:30;
dist(G*(i,j),G*(i,j+1)) = (N-bound C - S-bound C)/2|^n by A1,A2,GOBRD14:9;
then dist(G*(1,1),G*(1,1+1)) = dist(G*(i,j),G*(i,j+1)) by A6,A5,GOBRD14:9
.= G*(i,j+1)`2 - G*(i,j)`2 by A1,A2,GOBRD14:6;
hence thesis;
end;
TopSpaceMetr Euclid 2 = the TopStruct of TOP-REAL 2 by EUCLID:def 8;
then
Lm5: the TopStruct of TOP-REAL 2 = TopStruct (#the carrier of Euclid 2,
Family_open_set Euclid 2#) by PCOMPS_1:def 5;
Lm6: for r being Real, q being Point of Euclid 2 st 1 <= i & i+1 <= len
Gauge (C,n) & 1 <= j & j+1 <= width Gauge (C,n) & r > 0 & p = q & dist(Gauge(C,
n)*(1,1),Gauge(C,n)*(1,2)) < r/4 & dist(Gauge(C,n)*(1,1),Gauge(C,n)*(2,1)) < r/
4 & p in cell (Gauge(C,n),i,j) holds cell(Gauge(C,n),i,j) c= Ball (q,r)
proof
let r be Real, q be Point of Euclid 2;
assume that
A1: 1 <= i and
A2: i+1 <= len Gauge (C,n) and
A3: 1 <= j and
A4: j+1 <= width Gauge (C,n) and
A5: r > 0 and
A6: p = q and
A7: dist(Gauge(C,n)*(1,1),Gauge(C,n)*(1,2)) < r/4 and
A8: dist(Gauge(C,n)*(1,1),Gauge(C,n)*(2,1)) < r/4 and
A9: p in cell (Gauge(C,n),i,j);
set G = Gauge(C,n);
set I = i, J = j, l = r/4;
let x be object;
assume
A10: x in cell(Gauge(C,n),i,j);
then reconsider Q = q, X = x as Point of TOP-REAL 2 by Lm5;
A11: Q`1 <= G*(I+1,J)`1 by A1,A2,A3,A4,A6,A9,JORDAN9:17;
A12: G*(I,J)`2 <= Q`2 by A1,A2,A3,A4,A6,A9,JORDAN9:17;
A13: G*(I,J)`1 <= X`1 by A1,A2,A3,A4,A10,JORDAN9:17;
j < j+1 by XREAL_1:29;
then
A14: j <= width G by A4,XXREAL_0:2;
i < i + 1 by XREAL_1:29;
then
A15: i <= len G by A2,XXREAL_0:2;
then
A16: [i,j] in Indices G by A1,A3,A14,MATRIX_0:30;
A17: X`2 <= G*(I,J+1)`2 by A1,A2,A3,A4,A10,JORDAN9:17;
A18: G*(I,J)`2 <= X`2 by A1,A2,A3,A4,A10,JORDAN9:17;
A19: Q`2 <= G*(I,J+1)`2 by A1,A2,A3,A4,A6,A9,JORDAN9:17;
A20: X`1 <= G*(I+1,J)`1 by A1,A2,A3,A4,A10,JORDAN9:17;
1 <= j+1 by A3,XREAL_1:29;
then [i,j+1] in Indices G by A1,A4,A15,MATRIX_0:30;
then
A21: G*(I,J+1)`2 - G*(I,J)`2 < l by A7,A16,Th2;
1 <= 1 + i by NAT_1:11;
then [i+1,j] in Indices G by A2,A3,A14,MATRIX_0:30;
then G*(I+1,J)`1 - G*(I,J)`1 < l by A8,A16,Th1;
then
A22: (G*(I+1,J)`1 - G*(I,J)`1 ) + ( G*(I,J+1)`2 - G*(I,J)`2 ) <= l + l by A21,
XREAL_1:7;
G*(I,J)`1 <= Q`1 by A1,A2,A3,A4,A6,A9,JORDAN9:17;
then dist (Q,X) <= (G*(I+1,J)`1 - G*(I,J)`1 ) + ( G*(I,J+1)`2 - G*(I,J)`2 )
by A11,A12,A19,A13,A20,A18,A17,TOPREAL6:95;
then
A23: dist (p,X) <= l + l by A6,A22,XXREAL_0:2;
reconsider x9 = x as Point of Euclid 2 by A10,Lm3;
2*(r/4) < r by A5,Lm4;
then dist (X, p) < r by A23,XXREAL_0:2;
then dist (x9, q) < r by A6,TOPREAL6:def 1;
hence thesis by METRIC_1:11;
end;
theorem Th3:
for S being Subset of TOP-REAL 2 st S is bounded
holds proj1.:S is real-bounded
proof
let S be Subset of TOP-REAL 2;
assume S is bounded;
then reconsider C = S as bounded Subset of Euclid 2 by JORDAN2C:11;
consider r being Real, x being Point of Euclid 2 such that
A1: 0 < r and
A2: C c= Ball(x,r) by METRIC_6:def 3;
reconsider P = Ball(x,r) as Subset of TOP-REAL 2 by TOPREAL3:8;
reconsider p = x as Point of TOP-REAL 2 by TOPREAL3:8;
set t = max(|.p`1-r.|,|.p`1+r.|);
now
assume that
A3: |.p`1-r.| <= 0 and
A4: |.p`1+r.| <= 0;
|.p`1-r.| = 0 by A3,COMPLEX1:46;
then |.r-p`1.| = 0 by UNIFORM1:11;
then
A5: r-p`1 = 0 by ABSVALUE:2;
|.p`1+r.| = 0 by A4,COMPLEX1:46;
hence contradiction by A1,A5,ABSVALUE:2;
end;
then
A6: t > 0 by XXREAL_0:30;
A7: proj1.:P = ].p`1-r,p`1+r.[ by TOPREAL6:43;
for s being Real st s in proj1.:S holds |.s.| < t
proof
let s being Real;
proj1.:S c= proj1.:P by A2,RELAT_1:123;
hence thesis by A7,JCT_MISC:3;
end;
hence thesis by A6,SEQ_4:4;
end;
theorem
for C1 being non empty compact Subset of TOP-REAL 2, C2, S being non
empty Subset of TOP-REAL 2 holds S = C1 \/ C2 & proj1.:C2 is non empty
bounded_below implies W-bound S = min(W-bound C1, W-bound C2)
proof
let C1 be non empty compact Subset of TOP-REAL 2, C2, S be non empty Subset
of TOP-REAL 2;
assume that
A1: S = C1 \/ C2 and
A2: proj1.:C2 is non empty bounded_below;
set P1 = proj1.:C1, P2 = proj1.:C2, PS = proj1.:S;
A3: W-bound C1 = lower_bound P1 by SPRECT_1:43;
A4: W-bound C2 = lower_bound P2 by SPRECT_1:43;
thus W-bound S = lower_bound PS by SPRECT_1:43
.= lower_bound(P1 \/ P2) by A1,RELAT_1:120
.= min(W-bound C1, W-bound C2) by A2,A3,A4,SEQ_4:142;
end;
Lm7: for X being Subset of TOP-REAL 2 holds p in X & X is bounded
implies lower_bound
(proj1|X) <= p`1 & p`1 <= upper_bound (proj1|X)
proof
set T = TOP-REAL 2;
let X be Subset of TOP-REAL 2;
assume that
A1: p in X and
A2: X is bounded;
reconsider X as non empty Subset of TOP-REAL 2 by A1;
A3: the carrier of T|X = X by PRE_TOPC:8;
A4: (proj1|X).:X = proj1.:X by RELAT_1:129;
A5: proj1.:X is real-bounded by A2,Th3;
then (proj1|X).:X is bounded_below by A4,XXREAL_2:def 11;
then
A6: proj1|X is bounded_below by A3,MEASURE6:def 10;
(proj1|X).:X is bounded_above by A4,A5,XXREAL_2:def 11;
then proj1|X is bounded_above by A3,MEASURE6:def 11;
then reconsider f = proj1|X as bounded RealMap of T|X by A6;
reconsider p9 = p as Point of T|X by A1,PRE_TOPC:8;
A7: (proj1|X).p9 = p`1 by A1,PSCOMP_1:22;
then lower_bound f <= p`1 by PSCOMP_1:1;
hence thesis by A7,PSCOMP_1:4;
end;
Lm8: for X being Subset of TOP-REAL 2 holds p in X & X is bounded
implies lower_bound
(proj2|X) <= p`2 & p`2 <= upper_bound (proj2|X)
proof
set T = TOP-REAL 2;
let X be Subset of TOP-REAL 2;
assume that
A1: p in X and
A2: X is bounded;
reconsider X as non empty Subset of TOP-REAL 2 by A1;
A3: the carrier of T|X = X by PRE_TOPC:8;
A4: (proj2|X).:X = proj2.:X by RELAT_1:129;
A5: proj2.:X is real-bounded by A2,JCT_MISC:14;
then (proj2|X).:X is bounded_below by A4,XXREAL_2:def 11;
then
A6: proj2|X is bounded_below by A3,MEASURE6:def 10;
(proj2|X).:X is bounded_above by A4,A5,XXREAL_2:def 11;
then proj2|X is bounded_above by A3,MEASURE6:def 11;
then reconsider f = proj2|X as bounded RealMap of T|X by A6;
reconsider p9 = p as Point of T|X by A1,PRE_TOPC:8;
A7: (proj2|X).p9 = p`2 by A1,PSCOMP_1:23;
then lower_bound f <= p`2 by PSCOMP_1:1;
hence thesis by A7,PSCOMP_1:4;
end;
theorem Th5:
for X being Subset of TOP-REAL 2 holds p in X & X is bounded
implies W-bound X <= p`1 & p`1 <= E-bound X & S-bound X <= p`2 & p`2 <= N-bound
X
proof
let X be Subset of TOP-REAL 2;
assume that
A1: p in X and
A2: X is bounded;
W-bound X = lower_bound (proj1|X) by PSCOMP_1:def 7;
hence W-bound X <= p`1 by A1,A2,Lm7;
E-bound X = upper_bound (proj1|X) by PSCOMP_1:def 9;
hence E-bound X >= p`1 by A1,A2,Lm7;
S-bound X = lower_bound (proj2|X) by PSCOMP_1:def 10;
hence S-bound X <= p`2 by A1,A2,Lm8;
N-bound X = upper_bound (proj2|X) by PSCOMP_1:def 8;
hence thesis by A1,A2,Lm8;
end;
Lm9: for C being Subset of TOP-REAL 2 st C is bounded for h being Real
st BDD C <> {} & h > W-bound BDD C & (for p st p in BDD C holds p`1 >= h) holds
contradiction
proof
let C be Subset of TOP-REAL 2 such that
A1: C is bounded;
set X = proj1|BDD C;
let h be Real;
assume that
A2: BDD C <> {} and
A3: h > W-bound BDD C and
A4: for p st p in BDD C holds p`1 >= h;
reconsider T = (TOP-REAL 2)|BDD C as non empty TopSpace by A2;
the carrier of T = BDD C by PRE_TOPC:8;
then X.:the carrier of T = proj1.:BDD C by RELAT_1:129;
then X.:the carrier of T is real-bounded by A1,Th3,JORDAN2C:106;
then X.:the carrier of T is bounded_below by XXREAL_2:def 11;
then reconsider X as bounded_below RealMap of T by MEASURE6:def 10;
A5: for p being Point of T holds X.p >= h
proof
let p be Point of T;
A6: the carrier of T = BDD C by PRE_TOPC:8;
then p in BDD C;
then reconsider p9 = p as Point of TOP-REAL 2;
X.p = proj1.p9 by A6,FUNCT_1:49;
then X.p = p9`1 by PSCOMP_1:def 5;
hence thesis by A4,A6;
end;
lower_bound X = W-bound BDD C by PSCOMP_1:def 7;
hence thesis by A3,A5,PSCOMP_1:2;
end;
Lm10: for C being Subset of TOP-REAL 2 st C is bounded for h being Real
st BDD C <> {} & h < E-bound BDD C & (for p st p in BDD C holds p`1 <= h) holds
contradiction
proof
let C be Subset of TOP-REAL 2 such that
A1: C is bounded;
set X = proj1|BDD C;
let h be Real;
assume that
A2: BDD C <> {} and
A3: h < E-bound BDD C and
A4: for p st p in BDD C holds p`1 <= h;
reconsider T = (TOP-REAL 2)|BDD C as non empty TopSpace by A2;
the carrier of T = BDD C by PRE_TOPC:8;
then X.:the carrier of T = proj1.:BDD C by RELAT_1:129;
then X.:the carrier of T is real-bounded by A1,Th3,JORDAN2C:106;
then X.:the carrier of T is bounded_above by XXREAL_2:def 11;
then reconsider X as bounded_above RealMap of T by MEASURE6:def 11;
A5: for p being Point of T holds X.p <= h
proof
let p be Point of T;
A6: the carrier of T = BDD C by PRE_TOPC:8;
then p in BDD C;
then reconsider p9 = p as Point of TOP-REAL 2;
X.p = proj1.p9 by A6,FUNCT_1:49;
then X.p = p9`1 by PSCOMP_1:def 5;
hence thesis by A4,A6;
end;
upper_bound X = E-bound BDD C by PSCOMP_1:def 9;
hence thesis by A3,A5,PSCOMP_1:5;
end;
Lm11: for C being Subset of TOP-REAL 2 st C is bounded for h being Real
st BDD C <> {} & h < N-bound BDD C & (for p st p in BDD C holds p`2 <= h) holds
contradiction
proof
let C be Subset of TOP-REAL 2 such that
A1: C is bounded;
set X = proj2|BDD C;
let h be Real;
assume that
A2: BDD C <> {} and
A3: h < N-bound BDD C and
A4: for p st p in BDD C holds p`2 <= h;
reconsider T = (TOP-REAL 2)|BDD C as non empty TopSpace by A2;
the carrier of T = BDD C by PRE_TOPC:8;
then X.:the carrier of T = proj2.:BDD C by RELAT_1:129;
then X.:the carrier of T is real-bounded by A1,JCT_MISC:14,JORDAN2C:106;
then X.:the carrier of T is bounded_above by XXREAL_2:def 11;
then reconsider X as bounded_above RealMap of T by MEASURE6:def 11;
A5: for p being Point of T holds X.p <= h
proof
let p be Point of T;
A6: the carrier of T = BDD C by PRE_TOPC:8;
then p in BDD C;
then reconsider p9 = p as Point of TOP-REAL 2;
X.p = proj2.p9 by A6,FUNCT_1:49;
then X.p = p9`2 by PSCOMP_1:def 6;
hence thesis by A4,A6;
end;
upper_bound X = N-bound BDD C by PSCOMP_1:def 8;
hence thesis by A3,A5,PSCOMP_1:5;
end;
Lm12: for C being Subset of TOP-REAL 2 st C is bounded for h being Real
st BDD C <> {} & h > S-bound BDD C & (for p st p in BDD C holds p`2 >= h) holds
contradiction
proof
let C be Subset of TOP-REAL 2 such that
A1: C is bounded;
set X = proj2|BDD C;
let h be Real;
assume that
A2: BDD C <> {} and
A3: h > S-bound BDD C and
A4: for p st p in BDD C holds p`2 >= h;
reconsider T = (TOP-REAL 2)|BDD C as non empty TopSpace by A2;
the carrier of T = BDD C by PRE_TOPC:8;
then X.:the carrier of T = proj2.:BDD C by RELAT_1:129;
then X.:the carrier of T is real-bounded by A1,JCT_MISC:14,JORDAN2C:106;
then X.:the carrier of T is bounded_below by XXREAL_2:def 11;
then reconsider X as bounded_below RealMap of T by MEASURE6:def 10;
A5: for p being Point of T holds X.p >= h
proof
let p be Point of T;
A6: the carrier of T = BDD C by PRE_TOPC:8;
then p in BDD C;
then reconsider p9 = p as Point of TOP-REAL 2;
X.p = proj2.p9 by A6,FUNCT_1:49;
then X.p = p9`2 by PSCOMP_1:def 6;
hence thesis by A4,A6;
end;
lower_bound X = S-bound BDD C by PSCOMP_1:def 10;
hence thesis by A3,A5,PSCOMP_1:2;
end;
Lm13: now
let C be Subset of TOP-REAL 2;
assume C is bounded;
then UBD C is_outside_component_of C by JORDAN2C:68;
hence UBD C is non empty by JORDAN2C:def 3;
end;
theorem Th6:
for C being compact Subset of TOP-REAL 2 holds BDD C <> {}
implies W-bound C <= W-bound BDD C
proof
let C be compact Subset of TOP-REAL 2;
set WC = W-bound C, WB = W-bound BDD C;
set hal = (WB + WC)/2;
assume that
A1: BDD C <> {} and
A2: WC > WB;
A3: hal < WC by A2,XREAL_1:226;
now
per cases;
suppose
for q1 being Point of TOP-REAL 2 st q1 in BDD C holds q1`1 >= hal;
hence contradiction by A1,A2,Lm9,XREAL_1:226;
end;
suppose
ex q1 being Point of TOP-REAL 2 st q1 in BDD C & q1`1 < hal;
then consider q1 being Point of TOP-REAL 2 such that
A4: q1 in BDD C and
A5: q1`1 < hal;
set Q = |[(WC + q1`1)/2,q1`2]|;
set WH = west_halfline Q;
A6: Q`1 = (WC + q1`1)/2 by EUCLID:52;
A7: q1`1 < WC by A3,A5,XXREAL_0:2;
WH misses C
proof
A8: Q`1 < WC by A7,A6,XREAL_1:226;
assume WH meets C;
then consider y being object such that
A9: y in WH /\ C by XBOOLE_0:4;
A10: y in C by A9,XBOOLE_0:def 4;
A11: y in WH by A9,XBOOLE_0:def 4;
reconsider y as Point of TOP-REAL 2 by A9;
y`1 <= Q`1 by A11,TOPREAL1:def 13;
then y`1 < WC by A8,XXREAL_0:2;
hence thesis by A10,PSCOMP_1:24;
end;
then
A12: WH c= UBD C by JORDAN2C:126;
A13: q1`2 = Q`2 by EUCLID:52;
q1`1 < Q`1 by A7,A6,XREAL_1:226;
then q1 in WH by A13,TOPREAL1:def 13;
then q1 in BDD C /\ UBD C by A4,A12,XBOOLE_0:def 4;
then BDD C meets UBD C;
hence contradiction by JORDAN2C:24;
end;
end;
hence thesis;
end;
theorem Th7:
for C being compact Subset of TOP-REAL 2 holds BDD C <> {}
implies E-bound C >= E-bound BDD C
proof
let C be compact Subset of TOP-REAL 2;
set WC = E-bound BDD C, WB = E-bound C;
set hal = (WB + WC)/2;
assume that
A1: BDD C <> {} and
A2: WC > WB;
A3: hal > WB by A2,XREAL_1:226;
now
per cases;
suppose
for q1 being Point of TOP-REAL 2 st q1 in BDD C holds q1`1 <= hal;
hence contradiction by A1,A2,Lm10,XREAL_1:226;
end;
suppose
ex q1 being Point of TOP-REAL 2 st q1 in BDD C & q1`1 > hal;
then consider q1 being Point of TOP-REAL 2 such that
A4: q1 in BDD C and
A5: q1`1 > hal;
set Q = |[(WB + q1`1)/2,q1`2]|;
set WH = east_halfline Q;
A6: Q`1 = (WB + q1`1)/2 by EUCLID:52;
A7: q1`1 > WB by A3,A5,XXREAL_0:2;
WH misses C
proof
A8: Q`1 > WB by A7,A6,XREAL_1:226;
assume WH /\ C <> {};
then consider y being object such that
A9: y in WH /\ C by XBOOLE_0:def 1;
A10: y in C by A9,XBOOLE_0:def 4;
A11: y in WH by A9,XBOOLE_0:def 4;
reconsider y as Point of TOP-REAL 2 by A9;
y`1 >= Q`1 by A11,TOPREAL1:def 11;
then y`1 > WB by A8,XXREAL_0:2;
hence thesis by A10,PSCOMP_1:24;
end;
then
A12: WH c= UBD C by JORDAN2C:127;
A13: q1`2 = Q`2 by EUCLID:52;
q1`1 > Q`1 by A7,A6,XREAL_1:226;
then q1 in WH by A13,TOPREAL1:def 11;
then q1 in BDD C /\ UBD C by A4,A12,XBOOLE_0:def 4;
then BDD C meets UBD C;
hence contradiction by JORDAN2C:24;
end;
end;
hence thesis;
end;
theorem Th8:
for C being compact Subset of TOP-REAL 2 holds BDD C <> {}
implies S-bound C <= S-bound BDD C
proof
let C be compact Subset of TOP-REAL 2;
set WC = S-bound C, WB = S-bound BDD C;
set hal = (WB + WC)/2;
assume that
A1: BDD C <> {} and
A2: WC > WB;
A3: hal < WC by A2,XREAL_1:226;
now
per cases;
suppose
for q1 being Point of TOP-REAL 2 st q1 in BDD C holds q1`2 >= hal;
hence contradiction by A1,A2,Lm12,XREAL_1:226;
end;
suppose
ex q1 being Point of TOP-REAL 2 st q1 in BDD C & q1`2 < hal;
then consider q1 being Point of TOP-REAL 2 such that
A4: q1 in BDD C and
A5: q1`2 < hal;
set Q = |[q1`1,(WC + q1`2)/2]|;
set WH = south_halfline Q;
A6: Q`2 = (WC + q1`2)/2 by EUCLID:52;
A7: q1`2 < WC by A3,A5,XXREAL_0:2;
WH misses C
proof
A8: Q`2 < WC by A7,A6,XREAL_1:226;
assume WH /\ C <> {};
then consider y being object such that
A9: y in WH /\ C by XBOOLE_0:def 1;
A10: y in C by A9,XBOOLE_0:def 4;
A11: y in WH by A9,XBOOLE_0:def 4;
reconsider y as Point of TOP-REAL 2 by A9;
y`2 <= Q`2 by A11,TOPREAL1:def 12;
then y`2 < WC by A8,XXREAL_0:2;
hence thesis by A10,PSCOMP_1:24;
end;
then
A12: WH c= UBD C by JORDAN2C:128;
A13: q1`1 = Q`1 by EUCLID:52;
q1`2 < Q`2 by A7,A6,XREAL_1:226;
then q1 in WH by A13,TOPREAL1:def 12;
then q1 in BDD C /\ UBD C by A4,A12,XBOOLE_0:def 4;
then BDD C meets UBD C;
hence contradiction by JORDAN2C:24;
end;
end;
hence thesis;
end;
theorem Th9:
for C being compact Subset of TOP-REAL 2 holds BDD C <> {}
implies N-bound C >= N-bound BDD C
proof
let C be compact Subset of TOP-REAL 2;
set WC = N-bound BDD C, WB = N-bound C;
set hal = (WB + WC)/2;
assume that
A1: BDD C <> {} and
A2: WC > WB;
A3: hal > WB by A2,XREAL_1:226;
now
per cases;
suppose
for q1 being Point of TOP-REAL 2 st q1 in BDD C holds q1`2 <= hal;
hence contradiction by A1,A2,Lm11,XREAL_1:226;
end;
suppose
ex q1 being Point of TOP-REAL 2 st q1 in BDD C & q1`2 > hal;
then consider q1 being Point of TOP-REAL 2 such that
A4: q1 in BDD C and
A5: q1`2 > hal;
set Q = |[q1`1,(WB + q1`2)/2]|;
set WH = north_halfline Q;
A6: Q`2 = (WB + q1`2)/2 by EUCLID:52;
A7: q1`2 > WB by A3,A5,XXREAL_0:2;
WH misses C
proof
A8: Q`2 > WB by A7,A6,XREAL_1:226;
assume WH /\ C <> {};
then consider y being object such that
A9: y in WH /\ C by XBOOLE_0:def 1;
A10: y in C by A9,XBOOLE_0:def 4;
A11: y in WH by A9,XBOOLE_0:def 4;
reconsider y as Point of TOP-REAL 2 by A9;
y`2 >= Q`2 by A11,TOPREAL1:def 10;
then y`2 > WB by A8,XXREAL_0:2;
hence thesis by A10,PSCOMP_1:24;
end;
then
A12: WH c= UBD C by JORDAN2C:129;
A13: q1`1 = Q`1 by EUCLID:52;
q1`2 > Q`2 by A7,A6,XREAL_1:226;
then q1 in WH by A13,TOPREAL1:def 10;
then q1 in BDD C /\ UBD C by A4,A12,XBOOLE_0:def 4;
then BDD C meets UBD C;
hence contradiction by JORDAN2C:24;
end;
end;
hence thesis;
end;
theorem Th10:
for C being compact non vertical Subset of TOP-REAL 2 for I
being Integer st p in BDD C & I = [\ ((p`1 - W-bound C) / (E-bound C - W-bound
C) * 2|^n) + 2 /] holds 1 < I
proof
let C be compact non vertical Subset of TOP-REAL 2;
set W = W-bound C, E = E-bound C;
set pW = p`1 - W, EW = E - W;
let I be Integer;
assume that
A1: p in BDD C and
A2: I = [\ (pW / EW * 2|^n) + 2 /];
A3: W <= W-bound BDD C by A1,Th6;
BDD C is bounded by JORDAN2C:106;
then p`1 >= W-bound BDD C by A1,Th5;
then p`1 >= W by A3,XXREAL_0:2;
then
A4: pW >= 0 by XREAL_1:48;
set K = [\ pW / EW * 2|^n /];
pW / EW * 2|^n - 1 < K by INT_1:def 6;
then
A5: pW / EW * 2|^n - 1 + 2 < K + 2 by XREAL_1:6;
EW > 0 by SPRECT_1:31,XREAL_1:50;
then pW / EW * 2|^n + 1 >= 0 + 1 by A4,XREAL_1:6;
then 1 < K + 2 by A5,XXREAL_0:2;
hence thesis by A2,INT_1:28;
end;
theorem Th11:
for C being compact non vertical Subset of TOP-REAL 2 for I
being Integer st p in BDD C & I = [\ ((p`1 - W-bound C) / (E-bound C - W-bound
C) * 2|^n) + 2 /] holds I + 1 <= len Gauge (C, n)
proof
let C be compact non vertical Subset of TOP-REAL 2;
set W = W-bound C, E = E-bound C;
set EW = E-W, pW = p`1 - W;
let I be Integer;
assume that
A1: p in BDD C and
A2: I = [\ (pW / EW * 2|^n) + 2 /];
A3: E >= E-bound BDD C by A1,Th7;
BDD C is bounded by JORDAN2C:106;
then p`1 <= E-bound BDD C by A1,Th5;
then p`1 <= E by A3,XXREAL_0:2;
then
A4: p`1 - W <= EW by XREAL_1:9;
EW > 0 by SPRECT_1:31,XREAL_1:50;
then pW / EW <= 1 by A4,XREAL_1:185;
then pW / EW * 2|^n <= 1 * 2|^n by XREAL_1:64;
then
A5: pW / EW * 2|^n + 3 <= 2|^n + 3 by XREAL_1:7;
I <= (pW / EW * 2|^n) + 2 by A2,INT_1:def 6;
then
A6: I + 1 <= (pW / EW * 2|^n) + 2 + 1 by XREAL_1:6;
len Gauge (C, n) = 2|^n + 3 by JORDAN8:def 1;
hence thesis by A5,A6,XXREAL_0:2;
end;
theorem Th12:
for C being compact non horizontal Subset of TOP-REAL 2 for J
being Integer st p in BDD C & J = [\ ((p`2 - S-bound C) / (N-bound C - S-bound
C) * 2|^n) + 2 /] holds 1 < J & J+1 <= width Gauge (C, n)
proof
let C be compact non horizontal Subset of TOP-REAL 2;
set W = S-bound C, E = N-bound C;
set EW = E-W, pW = p`2 - W;
let I be Integer;
assume that
A1: p in BDD C and
A2: I = [\ (pW / EW * 2|^n) + 2 /];
A3: EW > 0 by SPRECT_1:32,XREAL_1:50;
set K = [\ pW / EW * 2|^n /];
pW / EW * 2|^n - 1 < K by INT_1:def 6;
then
A4: pW / EW * 2|^n - 1 + 2 < K + 2 by XREAL_1:6;
A5: W <= S-bound BDD C by A1,Th8;
BDD C is bounded by JORDAN2C:106;
then p`2 >= S-bound BDD C by A1,Th5;
then p`2 >= W by A5,XXREAL_0:2;
then pW >= 0 by XREAL_1:48;
then pW / EW * 2|^n + 1 >= 0 + 1 by A3,XREAL_1:6;
then 1 < K + 2 by A4,XXREAL_0:2;
hence 1 < I by A2,INT_1:28;
A6: len Gauge (C, n) = width Gauge (C, n) by JORDAN8:def 1;
A7: E >= N-bound BDD C by A1,Th9;
BDD C is bounded by JORDAN2C:106;
then p`2 <= N-bound BDD C by A1,Th5;
then p`2 <= E by A7,XXREAL_0:2;
then p`2 - W <= EW by XREAL_1:9;
then pW / EW <= 1 by A3,XREAL_1:185;
then pW / EW * 2|^n <= 1 * 2|^n by XREAL_1:64;
then
A8: pW / EW * 2|^n + 3 <= 2|^n + 3 by XREAL_1:7;
I <= (pW / EW * 2|^n) + 2 by A2,INT_1:def 6;
then
A9: I + 1 <= (pW / EW * 2|^n) + 2 + 1 by XREAL_1:6;
len Gauge (C, n) = 2|^n + 3 by JORDAN8:def 1;
hence thesis by A6,A8,A9,XXREAL_0:2;
end;
theorem Th13:
for I being Integer st I = [\ ((p`1 - W-bound C) / (E-bound C -
W-bound C) * 2|^n) + 2 /] holds (W-bound C) + (((E-bound C)-(W-bound C))/(2|^n)
)*(I-2) <= p`1
proof
set W = W-bound C, EW = E-bound C - W-bound C;
set PW = p`1 - W;
set KI = [\ (PW / EW * 2|^n) /];
let I be Integer;
A1: EW > 0 by TOPREAL5:17,XREAL_1:50;
2|^n > 0 by NEWTON:83;
then
A2: (EW/(2|^n))*(PW / EW * 2|^n) = PW by A1,Lm2;
assume I = [\ (PW / EW * 2|^n) + 2 /];
then
A3: I - 2 = [\ (PW / EW * 2|^n) /] by Lm1;
KI <= PW / EW * 2|^n by INT_1:def 6;
then
A4: (EW/(2|^n))*KI <= (EW/(2|^n))*(PW / EW * 2|^n) by A1,XREAL_1:64;
W + PW = p`1;
hence thesis by A3,A2,A4,XREAL_1:6;
end;
theorem Th14:
for I being Integer st I = [\ ((p`1 - W-bound C) / (E-bound C -
W-bound C) * 2|^n) + 2 /] holds p`1 < (W-bound C) + (((E-bound C)-(W-bound C))/
(2|^n))*(I-1)
proof
set W = W-bound C, E = E-bound C;
set EW = E - W, PW = p`1 - W;
let I be Integer;
set KI = I - 1;
A1: 2|^n > 0 by NEWTON:83;
assume I = [\ (PW / EW * 2|^n) + 2 /];
then I > (PW / EW * 2|^n) + 2 - 1 by INT_1:def 6;
then
A2: I - 1 > (PW / EW * 2|^n) + 1 - 1 by XREAL_1:9;
A3: EW > 0 by TOPREAL5:17,XREAL_1:50;
then EW/(2|^n) > 0 by A1,XREAL_1:139;
then
A4: (EW/(2|^n))*KI > (EW/(2|^n))*(PW / EW * 2|^n) by A2,XREAL_1:68;
A5: W + PW = p`1;
(EW/(2|^n))*(PW / EW * 2|^n) = PW by A3,A1,Lm2;
hence thesis by A5,A4,XREAL_1:6;
end;
theorem Th15:
for J being Integer st J = [\ ((p`2 - S-bound C) / (N-bound C -
S-bound C) * 2|^n) + 2 /] holds (S-bound C) + ((N-bound C - S-bound C)/(2|^n))*
(J-2) <= p`2
proof
set W = S-bound C, EW = N-bound C - S-bound C;
set PW = p`2 - W;
set KI = [\ (PW / EW * 2|^n) /];
let I be Integer;
A1: EW > 0 by TOPREAL5:16,XREAL_1:50;
2|^n > 0 by NEWTON:83;
then
A2: (EW/(2|^n))*(PW / EW * 2|^n) = PW by A1,Lm2;
assume I = [\ (PW / EW * 2|^n) + 2 /];
then
A3: I - 2 = [\ (PW / EW * 2|^n) /] by Lm1;
KI <= PW / EW * 2|^n by INT_1:def 6;
then
A4: (EW/(2|^n))*KI <= (EW/(2|^n))*(PW / EW * 2|^n) by A1,XREAL_1:64;
W + PW = p`2;
hence thesis by A3,A2,A4,XREAL_1:6;
end;
theorem Th16:
for J being Integer st J = [\ ((p`2 - S-bound C) / (N-bound C -
S-bound C) * 2|^n) + 2 /] holds p`2 < (S-bound C) + ((N-bound C - S-bound C)/(2
|^n))*(J-1)
proof
set W = S-bound C, E = N-bound C;
set EW = E - W, PW = p`2 - W;
let I be Integer;
set KI = I - 1;
A1: 2|^n > 0 by NEWTON:83;
assume I = [\ (PW / EW * 2|^n) + 2 /];
then I > (PW / EW * 2|^n) + 2 - 1 by INT_1:def 6;
then
A2: I - 1 > (PW / EW * 2|^n) + 1 - 1 by XREAL_1:9;
A3: W + PW = p`2;
A4: EW > 0 by TOPREAL5:16,XREAL_1:50;
then
A5: EW/(2|^n) > 0 by A1,XREAL_1:139;
(EW/(2|^n)) * (PW / EW * 2|^n) = PW by A4,A1,Lm2;
then (EW/(2|^n))*KI > PW by A2,A5,XREAL_1:68;
hence thesis by A3,XREAL_1:6;
end;
theorem Th17:
for C being closed Subset of TOP-REAL 2, p being Point of Euclid
2 st p in BDD C ex r being Real st r > 0 & Ball(p,r) c= BDD C
proof
let C be closed Subset of TOP-REAL 2, p be Point of Euclid 2;
set W = Int BDD C;
assume p in BDD C;
then p in W by TOPS_1:23;
then consider r being Real such that
A1: r > 0 and
A2: Ball(p,r) c= BDD C by GOBOARD6:5;
reconsider r as Real;
take r;
thus thesis by A1,A2;
end;
theorem
for p, q being Point of TOP-REAL 2, r being Real st dist(Gauge(
C,n)*(1,1),Gauge(C,n)*(1,2)) < r & dist(Gauge(C,n)*(1,1),Gauge(C,n)*(2,1)) < r
& p in cell (Gauge (C, n), i, j) & q in cell (Gauge (C, n), i, j) & 1 <= i & i+
1 <= len Gauge (C,n) & 1 <= j & j+1 <= width Gauge(C,n) holds dist (p,q) < 2 *
r
proof
set G = Gauge (C, n);
let p, q be Point of TOP-REAL 2, r be Real;
assume that
A1: dist(G*(1,1),G*(1,2)) < r and
A2: dist(G*(1,1),G*(2,1)) < r and
A3: p in cell (G, i, j) and
A4: q in cell (G, i, j) and
A5: 1 <= i and
A6: i+1 <= len G and
A7: 1 <= j and
A8: j+1 <= width G;
A9: p`1 <= G*(i+1,j)`1 by A3,A5,A6,A7,A8,JORDAN9:17;
A10: p`2 <= G*(i,j+1)`2 by A3,A5,A6,A7,A8,JORDAN9:17;
A11: G*(i,j)`2 <= p`2 by A3,A5,A6,A7,A8,JORDAN9:17;
j <= j+1 by NAT_1:11;
then
A12: j <= width G by A8,XXREAL_0:2;
i <= i+1 by NAT_1:11;
then
A13: i <= len G by A6,XXREAL_0:2;
then
A14: [i,j] in Indices G by A5,A7,A12,MATRIX_0:30;
A15: q`2 <= G*(i,j+1)`2 by A4,A5,A6,A7,A8,JORDAN9:17;
A16: G*(i,j)`2 <= q`2 by A4,A5,A6,A7,A8,JORDAN9:17;
A17: q`1 <= G*(i+1,j)`1 by A4,A5,A6,A7,A8,JORDAN9:17;
A18: G*(i,j)`1 <= q`1 by A4,A5,A6,A7,A8,JORDAN9:17;
1 <= j+1 by NAT_1:11;
then [i,j+1] in Indices G by A5,A8,A13,MATRIX_0:30;
then
A19: G*(i,j+1)`2 - G*(i,j)`2 < r by A1,A14,Th2;
1 <= i+1 by NAT_1:11;
then [i+1,j] in Indices G by A6,A7,A12,MATRIX_0:30;
then G*(i+1,j)`1 - G*(i,j)`1 < r by A2,A14,Th1;
then
A20: (G*(i+1,j)`1 - G*(i,j)`1 ) + ( G*(i,j+1)`2 - G*(i,j)`2 ) < r + r by A19,
XREAL_1:8;
G*(i,j)`1 <= p`1 by A3,A5,A6,A7,A8,JORDAN9:17;
then dist (p,q) <= (G*(i+1,j)`1 - G*(i,j)`1 ) + ( G*(i,j+1)`2 - G*(i,j)`2 )
by A9,A11,A10,A18,A17,A16,A15,TOPREAL6:95;
hence thesis by A20,XXREAL_0:2;
end;
theorem
for C being compact Subset of TOP-REAL 2 holds p in BDD C implies p`2
<> N-bound BDD C
proof
reconsider P = p as Point of Euclid 2 by Lm3;
let C be compact Subset of TOP-REAL 2;
A1: BDD C is bounded by JORDAN2C:106;
assume p in BDD C;
then consider r being Real such that
A2: r > 0 and
A3: Ball(P,r) c= BDD C by Th17;
set EX = |[p`1, p`2 + r/2]|;
0 < r/2 by A2,XREAL_1:139;
then
A4: p`2 + r/2 > p`2 + 0 by XREAL_1:6;
assume
A5: p`2 = N-bound BDD C;
A6: not EX in BDD C
proof
assume EX in BDD C;
then EX`2 <= N-bound BDD C by A1,Th5;
hence thesis by A5,A4,EUCLID:52;
end;
A7: P = |[p`1,p`2]| by EUCLID:53;
r/2 < r by A2,XREAL_1:216;
then EX in Ball(P,r) by A2,A7,GOBOARD6:8;
hence thesis by A3,A6;
end;
theorem
for C being compact Subset of TOP-REAL 2 holds p in BDD C implies p`1
<> E-bound BDD C
proof
reconsider P = p as Point of Euclid 2 by Lm3;
let C be compact Subset of TOP-REAL 2;
A1: BDD C is bounded by JORDAN2C:106;
assume p in BDD C;
then consider r being Real such that
A2: r > 0 and
A3: Ball(P,r) c= BDD C by Th17;
set EX = |[p`1 + r/2, p`2]|;
0 < r/2 by A2,XREAL_1:139;
then
A4: p`1 + r/2 > p`1 + 0 by XREAL_1:6;
assume
A5: p`1 = E-bound BDD C;
A6: not EX in BDD C
proof
assume EX in BDD C;
then EX`1 <= E-bound BDD C by A1,Th5;
hence thesis by A5,A4,EUCLID:52;
end;
A7: P = |[p`1,p`2]| by EUCLID:53;
r/2 < r by A2,XREAL_1:216;
then EX in Ball(P,r) by A2,A7,GOBOARD6:7;
hence thesis by A3,A6;
end;
theorem
for C being compact Subset of TOP-REAL 2 holds p in BDD C implies p`2
<> S-bound BDD C
proof
reconsider P = p as Point of Euclid 2 by Lm3;
let C be compact Subset of TOP-REAL 2;
A1: BDD C is bounded by JORDAN2C:106;
assume p in BDD C;
then consider r being Real such that
A2: r > 0 and
A3: Ball(P,r) c= BDD C by Th17;
set EX = |[p`1, p`2 - r/2]|;
0 < r/2 by A2,XREAL_1:139;
then p`2 + r/2 > p`2 + 0 by XREAL_1:6;
then
A4: p`2 - r/2 < p`2 by XREAL_1:19;
assume
A5: p`2 = S-bound BDD C;
A6: not EX in BDD C
proof
assume EX in BDD C;
then EX`2 >= S-bound BDD C by A1,Th5;
hence thesis by A5,A4,EUCLID:52;
end;
A7: P = |[p`1,p`2]| by EUCLID:53;
r/2 < r by A2,XREAL_1:216;
then EX in Ball(P,r) by A2,A7,GOBOARD6:10;
hence thesis by A3,A6;
end;
theorem Th22:
for C being compact Subset of TOP-REAL 2 holds p in BDD C
implies p`1 <> W-bound BDD C
proof
reconsider P = p as Point of Euclid 2 by Lm3;
let C be compact Subset of TOP-REAL 2;
A1: BDD C is bounded by JORDAN2C:106;
assume p in BDD C;
then consider r being Real such that
A2: r > 0 and
A3: Ball(P,r) c= BDD C by Th17;
set EX = |[p`1 - r/2, p`2]|;
0 < r/2 by A2,XREAL_1:139;
then p`1 + r/2 > p`1 + 0 by XREAL_1:6;
then
A4: p`1 - r/2 < p`1 by XREAL_1:19;
assume
A5: p`1 = W-bound BDD C;
A6: not EX in BDD C
proof
assume EX in BDD C;
then EX`1 >= W-bound BDD C by A1,Th5;
hence thesis by A5,A4,EUCLID:52;
end;
A7: P = |[p`1,p`2]| by EUCLID:53;
r/2 < r by A2,XREAL_1:216;
then EX in Ball(P,r) by A2,A7,GOBOARD6:9;
hence thesis by A3,A6;
end;
theorem
p in BDD C implies ex n,i,j being Nat st 1 < i & i < len
Gauge(C,n) & 1 < j & j < width Gauge(C,n) & p`1 <> (Gauge(C,n)*(i,j))`1 & p in
cell(Gauge(C,n),i,j) & cell(Gauge(C,n),i,j) c= BDD C
proof
reconsider P = p as Point of Euclid 2 by Lm3;
set W = W-bound C, E = E-bound C, S = S-bound C, N = N-bound C;
set EW = E-W, NS = N-S;
assume
A1: p in BDD C;
then consider r being Real such that
A2: r > 0 and
A3: Ball(P,r) c= BDD C by Th17;
set l = r/4;
l > 0 by A2,XREAL_1:139;
then consider n being Nat such that
1 < n and
A4: dist(Gauge(C,n)*(1,1),Gauge(C,n)*(1,2)) < l and
A5: dist(Gauge(C,n)*(1,1),Gauge(C,n)*(2,1)) < l by GOBRD14:11;
set I = [\ ((p`1 - W) / EW * 2|^n) + 2 /], J = [\ ((p`2 - S) / NS * 2|^n) +
2 /];
A6: 1 < J by A1,Th12;
set G = Gauge(C,n);
A7: I+1 <= len G by A1,Th11;
A8: J+1 <= width G by A1,Th12;
take n;
A9: 1 < I by A1,Th10;
then reconsider I, J as Element of NAT by A6,INT_1:3;
A10: I < I + 1 by XREAL_1:29;
then
A11: I <= len G by A7,XXREAL_0:2;
1 <= J + 1 by NAT_1:11;
then [I,J+1] in Indices G by A9,A8,A11,MATRIX_0:30;
then G*(I,J+1) = |[W+(EW/(2|^n))*(I-2), S+(NS/(2|^n))*(J+1-2)]| by
JORDAN8:def 1;
then
A12: G*(I,J+1)`2 = S+(NS/(2|^n))*(J-1) by EUCLID:52;
then
A13: p`2 < G*(I,J+1)`2 by Th16;
A14: J < J + 1 by XREAL_1:29;
then
A15: J <= width G by A8,XXREAL_0:2;
then [I,J] in Indices G by A9,A6,A11,MATRIX_0:30;
then
A16: G*(I,J) = |[W+(EW/(2|^n))*(I-2), S+(NS/(2|^n))*(J-2)]| by JORDAN8:def 1;
then G*(I,J)`1 = W+(EW/(2|^n))*(I-2) by EUCLID:52;
then
A17: G*(I,J)`1 <= p`1 by Th13;
1 <= I + 1 by NAT_1:11;
then [I+1,J] in Indices G by A7,A6,A15,MATRIX_0:30;
then G*(I+1,J) = |[W+(EW/(2|^n))*(I+1-2), S+(NS/(2|^n))*(J-2)]| by
JORDAN8:def 1;
then G*(I+1,J)`1 = W+(EW/(2|^n))*(I-1) by EUCLID:52;
then
A18: p`1 < G*(I+1,J)`1 by Th14;
G*(I,J)`2 = S+(NS/(2|^n))*(J-2) by A16,EUCLID:52;
then
A19: G*(I,J)`2 <= p`2 by Th15;
A20: S + (NS/(2|^n))*(J-1) > p`2 by Th16;
then
A21: p in cell(G,I,J) by A9,A7,A6,A8,A17,A19,A18,A12,JORDAN9:17;
per cases;
suppose
A22: p`1 <> G*(I,J)`1;
take I, J;
thus 1 < I & I < len G & 1 < J & J < width G by A1,A7,A8,A10,A14,Th10,Th12,
XXREAL_0:2;
cell(G,I,J) c= Ball(P,r) by A2,A4,A5,A9,A7,A6,A8,A21,Lm6;
hence thesis by A3,A9,A7,A6,A8,A20,A17,A19,A18,A12,A22,JORDAN9:17;
end;
suppose
A23: p`1 = G*(I,J)`1;
then
A24: p`1 <= G*(I-'1+1,J)`1 by A9,XREAL_1:235;
A25: I-'1+1 <= len G by A9,A11,XREAL_1:235;
A26: 1 <= J by A1,Th12;
A27: 1 <= I-'1 by A1,Th10,NAT_D:49;
then I-'1 < I by NAT_D:51;
then
A28: p`1 > G*(I-'1,J)`1 by A11,A15,A23,A27,A26,GOBOARD5:3;
take I-'1, J;
A29: J + 1 <= width G by A1,Th12;
A30: 1 <= I-'1 by A1,Th10,NAT_D:49;
then
A31: I-'1 < I by NAT_D:51;
len G = width G by JORDAN8:def 1;
then
A32: J <= len G by A8,A14,XXREAL_0:2;
I-'1 <> 1
proof
assume I-'1 = 1;
then 1 = I - 1 by NAT_D:39;
then G*(I,J)`1 = W-bound C by A6,A32,JORDAN8:11;
then p`1 <= W-bound BDD C by A1,A23,Th6;
then
A33: p`1 < W-bound BDD C by A1,Th22,XXREAL_0:1;
BDD C is bounded by JORDAN2C:106;
hence thesis by A1,A33,Th5;
end;
hence 1 < I-'1 & I-'1 < len G & 1 < J & J < width G by A1,A14,A11,A30,A29
,A31,Th12,XXREAL_0:1,2;
A34: I-'1+1 <= len G by A9,A11,XREAL_1:235;
A35: J + 1 <= width G by A1,Th12;
A36: p`1 <= G*(I-'1+1,J)`1 by A9,A23,XREAL_1:235;
A37: 1 <= J by A1,Th12;
A38: I-'1+1 = I by A9,XREAL_1:235;
then
A39: G*(I-'1,J)`2 = G*(I,J)`2 by A11,A30,A37,A29,JORDAN9:16;
A40: G*(I-'1,J+1)`2 = G*(I,J+1)`2 by A11,A38,A30,A37,A29,JORDAN9:16;
p`1 > G*(I-'1,J)`1 by A11,A15,A23,A30,A37,A31,GOBOARD5:3;
then p in cell (G,I-'1,J) by A19,A13,A30,A34,A37,A29,A36,A39,A40,JORDAN9:17
;
then cell(G,I-'1,J) c= Ball(P,r) by A2,A4,A5,A27,A25,A26,A35,Lm6;
hence thesis by A3,A19,A13,A39,A40,A27,A25,A26,A35,A24,A28,JORDAN9:17;
end;
end;
theorem
for C being Subset of TOP-REAL 2 st C is bounded holds UBD C is non
empty by Lm13;