:: Some Properties of Cells and Gauges
:: by Adam Grabowski , Artur Korni{\l}owicz and Andrzej Trybulec
::
:: Received October 13, 2000
:: Copyright (c) 2000-2021 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;
begin
reserve C for Simple_closed_curve,
i, j, n for Nat,
p for Point of TOP-REAL 2;
theorem :: JORDAN1C:1
[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;
theorem :: JORDAN1C:2
[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;
theorem :: JORDAN1C:3
for S being Subset of TOP-REAL 2 st S is bounded
holds proj1.:S is real-bounded;
theorem :: JORDAN1C:4
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);
theorem :: JORDAN1C:5
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;
theorem :: JORDAN1C:6
for C being compact Subset of TOP-REAL 2 holds BDD C <> {}
implies W-bound C <= W-bound BDD C;
theorem :: JORDAN1C:7
for C being compact Subset of TOP-REAL 2 holds BDD C <> {}
implies E-bound C >= E-bound BDD C;
theorem :: JORDAN1C:8
for C being compact Subset of TOP-REAL 2 holds BDD C <> {}
implies S-bound C <= S-bound BDD C;
theorem :: JORDAN1C:9
for C being compact Subset of TOP-REAL 2 holds BDD C <> {}
implies N-bound C >= N-bound BDD C;
theorem :: JORDAN1C:10
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;
theorem :: JORDAN1C:11
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);
theorem :: JORDAN1C:12
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);
theorem :: JORDAN1C:13
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;
theorem :: JORDAN1C:14
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);
theorem :: JORDAN1C:15
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;
theorem :: JORDAN1C:16
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);
theorem :: JORDAN1C:17
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;
theorem :: JORDAN1C:18
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;
theorem :: JORDAN1C:19
for C being compact Subset of TOP-REAL 2 holds p in BDD C implies p`2
<> N-bound BDD C;
theorem :: JORDAN1C:20
for C being compact Subset of TOP-REAL 2 holds p in BDD C implies p`1
<> E-bound BDD C;
theorem :: JORDAN1C:21
for C being compact Subset of TOP-REAL 2 holds p in BDD C implies p`2
<> S-bound BDD C;
theorem :: JORDAN1C:22
for C being compact Subset of TOP-REAL 2 holds p in BDD C
implies p`1 <> W-bound BDD C;
theorem :: JORDAN1C:23
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;
theorem :: JORDAN1C:24
for C being Subset of TOP-REAL 2 st C is bounded holds UBD C is non
empty;