:: GOBOARD6 semantic presentation

REAL is V157() V158() V159() V163() set
NAT is V157() V158() V159() V160() V161() V162() V163() Element of K6(REAL)
K6(REAL) is set
COMPLEX is V157() V163() set
omega is V157() V158() V159() V160() V161() V162() V163() set
K6(omega) is set
1 is non empty natural V11() real ext-real positive non negative V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
K7(1,1) is set
K6(K7(1,1)) is set
K7(K7(1,1),1) is set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is set
K7(K7(REAL,REAL),REAL) is set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty natural V11() real ext-real positive non negative V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
K7(2,2) is set
K7(K7(2,2),REAL) is set
K6(K7(K7(2,2),REAL)) is set
K6(NAT) is set
RAT is V157() V158() V159() V160() V163() set
INT is V157() V158() V159() V160() V161() V163() set
K6(K7(REAL,REAL)) is set
TOP-REAL 2 is non empty TopSpace-like V111() V136() V137() V138() V139() V140() V141() V142() strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
K246( the carrier of (TOP-REAL 2)) is M11( the carrier of (TOP-REAL 2))
K6( the carrier of (TOP-REAL 2)) is set
K7(COMPLEX,COMPLEX) is set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(RAT,RAT) is set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is set
K7(K7(NAT,NAT),NAT) is set
K6(K7(K7(NAT,NAT),NAT)) is set
{} is empty V157() V158() V159() V160() V161() V162() V163() set
the empty V157() V158() V159() V160() V161() V162() V163() set is empty V157() V158() V159() V160() V161() V162() V163() set
0 is empty natural V11() real ext-real non positive non negative V33() V156() V157() V158() V159() V160() V161() V162() V163() Element of NAT
Euclid 2 is non empty strict Reflexive discerning V88() triangle Discerning MetrStruct
REAL 2 is non empty FinSequence-membered M11( REAL )
K247(2,REAL) is FinSequence-membered M11( REAL )
Pitag_dist 2 is V16() V19(K7((REAL 2),(REAL 2))) V20( REAL ) V21() V30(K7((REAL 2),(REAL 2)), REAL ) Element of K6(K7(K7((REAL 2),(REAL 2)),REAL))
K7((REAL 2),(REAL 2)) is set
K7(K7((REAL 2),(REAL 2)),REAL) is set
K6(K7(K7((REAL 2),(REAL 2)),REAL)) is set
MetrStruct(# (REAL 2),(Pitag_dist 2) #) is strict MetrStruct
the carrier of (Euclid 2) is non empty set
n is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
n `1 is V11() real ext-real Element of REAL
n `2 is V11() real ext-real Element of REAL
A is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
n + A is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(n + A) `1 is V11() real ext-real Element of REAL
A `1 is V11() real ext-real Element of REAL
(n `1) + (A `1) is V11() real ext-real Element of REAL
(n + A) `2 is V11() real ext-real Element of REAL
A `2 is V11() real ext-real Element of REAL
(n `2) + (A `2) is V11() real ext-real Element of REAL
|[((n `1) + (A `1)),((n `2) + (A `2))]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
n is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
n `1 is V11() real ext-real Element of REAL
n `2 is V11() real ext-real Element of REAL
A is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
n - A is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(n - A) `1 is V11() real ext-real Element of REAL
A `1 is V11() real ext-real Element of REAL
(n `1) - (A `1) is V11() real ext-real Element of REAL
K38((A `1)) is V11() real ext-real set
K36((n `1),K38((A `1))) is V11() real ext-real set
(n - A) `2 is V11() real ext-real Element of REAL
A `2 is V11() real ext-real Element of REAL
(n `2) - (A `2) is V11() real ext-real Element of REAL
K38((A `2)) is V11() real ext-real set
K36((n `2),K38((A `2))) is V11() real ext-real set
|[((n `1) - (A `1)),((n `2) - (A `2))]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
n is V11() real ext-real Element of REAL
A is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
n * A is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(n * A) `1 is V11() real ext-real Element of REAL
A `1 is V11() real ext-real Element of REAL
n * (A `1) is V11() real ext-real Element of REAL
(n * A) `2 is V11() real ext-real Element of REAL
A `2 is V11() real ext-real Element of REAL
n * (A `2) is V11() real ext-real Element of REAL
|[(n * (A `1)),(n * (A `2))]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
n is non empty Reflexive MetrStruct
the carrier of n is non empty set
A is Element of the carrier of n
p is V11() real ext-real set
Ball (A,p) is Element of K6( the carrier of n)
K6( the carrier of n) is set
{ b₁ where b₁ is Element of the carrier of n : not p <= dist (A,b₁) } is set
dist (A,A) is V11() real ext-real Element of REAL
n is Reflexive discerning V88() triangle MetrStruct
TopSpaceMetr n is strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr n) is set
K6( the carrier of (TopSpaceMetr n)) is set
the carrier of n is set
A is Element of K6( the carrier of (TopSpaceMetr n))
p is V11() real ext-real set
p9 is Element of the carrier of n
Ball (p9,p) is Element of K6( the carrier of n)
K6( the carrier of n) is set
Family_open_set n is Element of K6(K6( the carrier of n))
K6(K6( the carrier of n)) is set
TopStruct(# the carrier of n,(Family_open_set n) #) is strict TopStruct
n is natural V11() real ext-real set
Euclid n is non empty strict Reflexive discerning V88() triangle Discerning MetrStruct
REAL n is non empty FinSequence-membered M11( REAL )
K247(n,REAL) is FinSequence-membered M11( REAL )
Pitag_dist n is V16() V19(K7((REAL n),(REAL n))) V20( REAL ) V21() V30(K7((REAL n),(REAL n)), REAL ) Element of K6(K7(K7((REAL n),(REAL n)),REAL))
K7((REAL n),(REAL n)) is set
K7(K7((REAL n),(REAL n)),REAL) is set
K6(K7(K7((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
TOP-REAL n is non empty TopSpace-like V111() V136() V137() V138() V139() V140() V141() V142() strict RLTopStruct
the carrier of (TOP-REAL n) is non empty set
A is Element of the carrier of (Euclid n)
p is V42(n) FinSequence-like V148() Element of the carrier of (TOP-REAL n)
p9 is V11() real ext-real set
Ball (A,p9) is Element of K6( the carrier of (Euclid n))
K6( the carrier of (Euclid n)) is set
K6( the carrier of (TOP-REAL n)) is set
the topology of (TOP-REAL n) is non empty Element of K6(K6( the carrier of (TOP-REAL n)))
K6(K6( the carrier of (TOP-REAL n))) is set
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like TopStruct
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K6( the carrier of (TopSpaceMetr (Euclid n))) is set
s is Element of K6( the carrier of (TOP-REAL n))
s1 is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
n is natural V11() real ext-real set
TOP-REAL n is non empty TopSpace-like V111() V136() V137() V138() V139() V140() V141() V142() strict RLTopStruct
the carrier of (TOP-REAL n) is non empty set
K6( the carrier of (TOP-REAL n)) is set
Euclid n is non empty strict Reflexive discerning V88() triangle Discerning MetrStruct
REAL n is non empty FinSequence-membered M11( REAL )
K247(n,REAL) is FinSequence-membered M11( REAL )
Pitag_dist n is V16() V19(K7((REAL n),(REAL n))) V20( REAL ) V21() V30(K7((REAL n),(REAL n)), REAL ) Element of K6(K7(K7((REAL n),(REAL n)),REAL))
K7((REAL n),(REAL n)) is set
K7(K7((REAL n),(REAL n)),REAL) is set
K6(K7(K7((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
A is V11() real ext-real Element of REAL
p is Element of K6( the carrier of (TOP-REAL n))
p9 is Element of the carrier of (Euclid n)
Ball (p9,A) is Element of K6( the carrier of (Euclid n))
K6( the carrier of (Euclid n)) is set
the topology of (TOP-REAL n) is non empty Element of K6(K6( the carrier of (TOP-REAL n)))
K6(K6( the carrier of (TOP-REAL n))) is set
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like TopStruct
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K6( the carrier of (TopSpaceMetr (Euclid n))) is set
s is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
n is non empty Reflexive discerning V88() triangle Discerning MetrStruct
the carrier of n is non empty set
TopSpaceMetr n is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is set
A is Element of the carrier of n
p is Element of K6( the carrier of (TopSpaceMetr n))
Int p is open Element of K6( the carrier of (TopSpaceMetr n))
p9 is V11() real ext-real set
Ball (A,p9) is Element of K6( the carrier of n)
K6( the carrier of n) is set
s is V11() real ext-real set
Ball (A,s) is Element of K6( the carrier of n)
p9 is V11() real ext-real set
Ball (A,p9) is Element of K6( the carrier of n)
Family_open_set n is Element of K6(K6( the carrier of n))
K6(K6( the carrier of n)) is set
TopStruct(# the carrier of n,(Family_open_set n) #) is non empty strict TopStruct
s is Element of K6( the carrier of (TopSpaceMetr n))
n is TopSpace-like TopStruct
the carrier of n is set
K6( the carrier of n) is set
the topology of n is non empty Element of K6(K6( the carrier of n))
K6(K6( the carrier of n)) is set
TopStruct(# the carrier of n, the topology of n #) is strict TopSpace-like TopStruct
the carrier of TopStruct(# the carrier of n, the topology of n #) is set
K6( the carrier of TopStruct(# the carrier of n, the topology of n #)) is set
A is Element of K6( the carrier of n)
Int A is open Element of K6( the carrier of n)
p is Element of K6( the carrier of TopStruct(# the carrier of n, the topology of n #))
Int p is open Element of K6( the carrier of TopStruct(# the carrier of n, the topology of n #))
p9 is Element of K6( the carrier of TopStruct(# the carrier of n, the topology of n #))
s is Element of K6( the carrier of n)
n is natural V11() real ext-real set
Euclid n is non empty strict Reflexive discerning V88() triangle Discerning MetrStruct
REAL n is non empty FinSequence-membered M11( REAL )
K247(n,REAL) is FinSequence-membered M11( REAL )
Pitag_dist n is V16() V19(K7((REAL n),(REAL n))) V20( REAL ) V21() V30(K7((REAL n),(REAL n)), REAL ) Element of K6(K7(K7((REAL n),(REAL n)),REAL))
K7((REAL n),(REAL n)) is set
K7(K7((REAL n),(REAL n)),REAL) is set
K6(K7(K7((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
TOP-REAL n is non empty TopSpace-like V111() V136() V137() V138() V139() V140() V141() V142() strict RLTopStruct
the carrier of (TOP-REAL n) is non empty set
K6( the carrier of (TOP-REAL n)) is set
A is Element of the carrier of (Euclid n)
p is Element of K6( the carrier of (TOP-REAL n))
Int p is open Element of K6( the carrier of (TOP-REAL n))
the topology of (TOP-REAL n) is non empty Element of K6(K6( the carrier of (TOP-REAL n)))
K6(K6( the carrier of (TOP-REAL n))) is set
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like TopStruct
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K6( the carrier of (TopSpaceMetr (Euclid n))) is set
p9 is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
Int p9 is open Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
s is V11() real ext-real set
Ball (A,s) is Element of K6( the carrier of (Euclid n))
K6( the carrier of (Euclid n)) is set
s is V11() real ext-real set
Ball (A,s) is Element of K6( the carrier of (Euclid n))
K6( the carrier of (Euclid n)) is set
s1 is V11() real ext-real set
Ball (A,s1) is Element of K6( the carrier of (Euclid n))
n is V11() real ext-real Element of REAL
A is V11() real ext-real Element of REAL
|[n,A]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
n - p is V11() real ext-real Element of REAL
K38(p) is V11() real ext-real set
K36(n,K38(p)) is V11() real ext-real set
(n - p) ^2 is V11() real ext-real Element of REAL
K37((n - p),(n - p)) is V11() real ext-real set
p9 is V11() real ext-real Element of REAL
|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
A - p9 is V11() real ext-real Element of REAL
K38(p9) is V11() real ext-real set
K36(A,K38(p9)) is V11() real ext-real set
(A - p9) ^2 is V11() real ext-real Element of REAL
K37((A - p9),(A - p9)) is V11() real ext-real set
((n - p) ^2) + ((A - p9) ^2) is V11() real ext-real Element of REAL
sqrt (((n - p) ^2) + ((A - p9) ^2)) is V11() real ext-real Element of REAL
s is Element of the carrier of (Euclid 2)
s1 is Element of the carrier of (Euclid 2)
dist (s,s1) is V11() real ext-real Element of REAL
|[n,A]| `1 is V11() real ext-real Element of REAL
|[n,A]| `2 is V11() real ext-real Element of REAL
|[p,p9]| `1 is V11() real ext-real Element of REAL
|[p,p9]| `2 is V11() real ext-real Element of REAL
(Pitag_dist 2) . (s,s1) is set
n is V11() real ext-real Element of REAL
A is V11() real ext-real Element of REAL
|[n,A]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
n + p is V11() real ext-real Element of REAL
|[(n + p),A]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
p9 is V11() real ext-real Element of REAL
s is Element of the carrier of (Euclid 2)
Ball (s,p9) is Element of K6( the carrier of (Euclid 2))
K6( the carrier of (Euclid 2)) is set
s1 is Element of the carrier of (Euclid 2)
dist (s,s1) is V11() real ext-real Element of REAL
n - (n + p) is V11() real ext-real Element of REAL
K38((n + p)) is V11() real ext-real set
K36(n,K38((n + p))) is V11() real ext-real set
(n - (n + p)) ^2 is V11() real ext-real Element of REAL
K37((n - (n + p)),(n - (n + p))) is V11() real ext-real set
A - A is V11() real ext-real Element of REAL
K38(A) is V11() real ext-real set
K36(A,K38(A)) is V11() real ext-real set
(A - A) ^2 is V11() real ext-real Element of REAL
K37((A - A),(A - A)) is V11() real ext-real set
((n - (n + p)) ^2) + ((A - A) ^2) is V11() real ext-real Element of REAL
sqrt (((n - (n + p)) ^2) + ((A - A) ^2)) is V11() real ext-real Element of REAL
- (n - (n + p)) is V11() real ext-real Element of REAL
(- (n - (n + p))) ^2 is V11() real ext-real Element of REAL
K37((- (n - (n + p))),(- (n - (n + p)))) is V11() real ext-real set
sqrt ((- (n - (n + p))) ^2) is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
A is V11() real ext-real Element of REAL
|[n,A]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
A + p is V11() real ext-real Element of REAL
|[n,(A + p)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
p9 is V11() real ext-real Element of REAL
s is Element of the carrier of (Euclid 2)
Ball (s,p9) is Element of K6( the carrier of (Euclid 2))
K6( the carrier of (Euclid 2)) is set
s1 is Element of the carrier of (Euclid 2)
dist (s,s1) is V11() real ext-real Element of REAL
n - n is V11() real ext-real Element of REAL
K38(n) is V11() real ext-real set
K36(n,K38(n)) is V11() real ext-real set
(n - n) ^2 is V11() real ext-real Element of REAL
K37((n - n),(n - n)) is V11() real ext-real set
A - (A + p) is V11() real ext-real Element of REAL
K38((A + p)) is V11() real ext-real set
K36(A,K38((A + p))) is V11() real ext-real set
(A - (A + p)) ^2 is V11() real ext-real Element of REAL
K37((A - (A + p)),(A - (A + p))) is V11() real ext-real set
((n - n) ^2) + ((A - (A + p)) ^2) is V11() real ext-real Element of REAL
sqrt (((n - n) ^2) + ((A - (A + p)) ^2)) is V11() real ext-real Element of REAL
- (A - (A + p)) is V11() real ext-real Element of REAL
(- (A - (A + p))) ^2 is V11() real ext-real Element of REAL
K37((- (A - (A + p))),(- (A - (A + p)))) is V11() real ext-real set
sqrt ((- (A - (A + p))) ^2) is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
A is V11() real ext-real Element of REAL
|[n,A]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
n - p is V11() real ext-real Element of REAL
K38(p) is V11() real ext-real set
K36(n,K38(p)) is V11() real ext-real set
|[(n - p),A]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
p9 is V11() real ext-real Element of REAL
s is Element of the carrier of (Euclid 2)
Ball (s,p9) is Element of K6( the carrier of (Euclid 2))
K6( the carrier of (Euclid 2)) is set
s1 is Element of the carrier of (Euclid 2)
dist (s,s1) is V11() real ext-real Element of REAL
n - (n - p) is V11() real ext-real Element of REAL
K38((n - p)) is V11() real ext-real set
K36(n,K38((n - p))) is V11() real ext-real set
(n - (n - p)) ^2 is V11() real ext-real Element of REAL
K37((n - (n - p)),(n - (n - p))) is V11() real ext-real set
A - A is V11() real ext-real Element of REAL
K38(A) is V11() real ext-real set
K36(A,K38(A)) is V11() real ext-real set
(A - A) ^2 is V11() real ext-real Element of REAL
K37((A - A),(A - A)) is V11() real ext-real set
((n - (n - p)) ^2) + ((A - A) ^2) is V11() real ext-real Element of REAL
sqrt (((n - (n - p)) ^2) + ((A - A) ^2)) is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
A is V11() real ext-real Element of REAL
|[n,A]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
A - p is V11() real ext-real Element of REAL
K38(p) is V11() real ext-real set
K36(A,K38(p)) is V11() real ext-real set
|[n,(A - p)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
p9 is V11() real ext-real Element of REAL
s is Element of the carrier of (Euclid 2)
Ball (s,p9) is Element of K6( the carrier of (Euclid 2))
K6( the carrier of (Euclid 2)) is set
s1 is Element of the carrier of (Euclid 2)
dist (s,s1) is V11() real ext-real Element of REAL
A - (A - p) is V11() real ext-real Element of REAL
K38((A - p)) is V11() real ext-real set
K36(A,K38((A - p))) is V11() real ext-real set
(A - (A - p)) ^2 is V11() real ext-real Element of REAL
K37((A - (A - p)),(A - (A - p))) is V11() real ext-real set
n - n is V11() real ext-real Element of REAL
K38(n) is V11() real ext-real set
K36(n,K38(n)) is V11() real ext-real set
(n - n) ^2 is V11() real ext-real Element of REAL
K37((n - n),(n - n)) is V11() real ext-real set
((A - (A - p)) ^2) + ((n - n) ^2) is V11() real ext-real Element of REAL
sqrt (((A - (A - p)) ^2) + ((n - n) ^2)) is V11() real ext-real Element of REAL
n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
n + 1 is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
A is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
A + 1 is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
p is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))
len p is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
width p is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
p * (n,A) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
p * ((n + 1),(A + 1)) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(p * (n,A)) + (p * ((n + 1),(A + 1))) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
p * (n,(A + 1)) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
p * ((n + 1),A) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(p * (n,(A + 1))) + (p * ((n + 1),A)) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(p * ((n + 1),(A + 1))) `1 is V11() real ext-real Element of REAL
p * ((n + 1),1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(p * ((n + 1),1)) `1 is V11() real ext-real Element of REAL
(p * ((n + 1),A)) `1 is V11() real ext-real Element of REAL
(p * ((n + 1),(A + 1))) `2 is V11() real ext-real Element of REAL
p * (1,(A + 1)) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(p * (1,(A + 1))) `2 is V11() real ext-real Element of REAL
(p * (n,(A + 1))) `2 is V11() real ext-real Element of REAL
(p * (n,A)) `2 is V11() real ext-real Element of REAL
p * (1,A) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(p * (1,A)) `2 is V11() real ext-real Element of REAL
(p * ((n + 1),A)) `2 is V11() real ext-real Element of REAL
((p * (n,A)) + (p * ((n + 1),(A + 1)))) `2 is V11() real ext-real Element of REAL
((p * (n,A)) `2) + ((p * ((n + 1),(A + 1))) `2) is V11() real ext-real Element of REAL
((p * (n,(A + 1))) + (p * ((n + 1),A))) `2 is V11() real ext-real Element of REAL
(p * (n,A)) `1 is V11() real ext-real Element of REAL
p * (n,1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(p * (n,1)) `1 is V11() real ext-real Element of REAL
(p * (n,(A + 1))) `1 is V11() real ext-real Element of REAL
((p * (n,A)) + (p * ((n + 1),(A + 1)))) `1 is V11() real ext-real Element of REAL
((p * (n,A)) `1) + ((p * ((n + 1),(A + 1))) `1) is V11() real ext-real Element of REAL
((p * (n,(A + 1))) + (p * ((n + 1),A))) `1 is V11() real ext-real Element of REAL
|[(((p * (n,(A + 1))) + (p * ((n + 1),A))) `1),(((p * (n,(A + 1))) + (p * ((n + 1),A))) `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
the topology of (TOP-REAL 2) is non empty Element of K6(K6( the carrier of (TOP-REAL 2)))
K6(K6( the carrier of (TOP-REAL 2))) is set
TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) is non empty strict TopSpace-like TopStruct
TopSpaceMetr (Euclid 2) is non empty strict TopSpace-like TopStruct
Family_open_set (Euclid 2) is Element of K6(K6( the carrier of (Euclid 2)))
K6( the carrier of (Euclid 2)) is set
K6(K6( the carrier of (Euclid 2))) is set
TopStruct(# the carrier of (Euclid 2),(Family_open_set (Euclid 2)) #) is non empty strict TopStruct
n is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))
v_strip (n,0) is Element of K6( the carrier of (TOP-REAL 2))
Int (v_strip (n,0)) is open Element of K6( the carrier of (TOP-REAL 2))
n * (1,1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(n * (1,1)) `1 is V11() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() real ext-real Element of REAL : not (n * (1,1)) `1 <= b₁ } is set
width n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
{ |[b₁,b₂]| where b₁, b₂ is V11() real ext-real Element of REAL : b₁ <= (n * (1,1)) `1 } is set
A is set
p is Element of the carrier of (Euclid 2)
p9 is V11() real ext-real set
Ball (p,p9) is Element of K6( the carrier of (Euclid 2))
s is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
s `1 is V11() real ext-real Element of REAL
s `2 is V11() real ext-real Element of REAL
|[(s `1),(s `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
s1 is V11() real ext-real Element of REAL
s1 / 2 is V11() real ext-real Element of REAL
K39(2) is non empty V11() real ext-real positive non negative set
K37(s1,K39(2)) is V11() real ext-real set
(s `1) + (s1 / 2) is V11() real ext-real Element of REAL
(s `2) + 0 is V11() real ext-real Element of REAL
|[((s `1) + (s1 / 2)),((s `2) + 0)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
Ball (p,s1) is Element of K6( the carrier of (Euclid 2))
r9 is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
|[r9,r]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
A is set
p is V11() real ext-real Element of REAL
p9 is V11() real ext-real Element of REAL
|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
s is Element of the carrier of (Euclid 2)
((n * (1,1)) `1) - p is V11() real ext-real Element of REAL
K38(p) is V11() real ext-real set
K36(((n * (1,1)) `1),K38(p)) is V11() real ext-real set
Ball (s,(((n * (1,1)) `1) - p)) is Element of K6( the carrier of (Euclid 2))
s1 is set
{ b₁ where b₁ is Element of the carrier of (Euclid 2) : not ((n * (1,1)) `1) - p <= dist (s,b<sub>1</sub>) } is set
G is Element of the carrier of (Euclid 2)
dist (s,G) is V11() real ext-real Element of REAL
r9 is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
r9 `1 is V11() real ext-real Element of REAL
p - (r9 `1) is V11() real ext-real Element of REAL
K38((r9 `1)) is V11() real ext-real set
K36(p,K38((r9 `1))) is V11() real ext-real set
(p - (r9 `1)) ^2 is V11() real ext-real Element of REAL
K37((p - (r9 `1)),(p - (r9 `1))) is V11() real ext-real set
((p - (r9 `1)) ^2) + 0 is V11() real ext-real Element of REAL
r9 `2 is V11() real ext-real Element of REAL
p9 - (r9 `2) is V11() real ext-real Element of REAL
K38((r9 `2)) is V11() real ext-real set
K36(p9,K38((r9 `2))) is V11() real ext-real set
(p9 - (r9 `2)) ^2 is V11() real ext-real Element of REAL
K37((p9 - (r9 `2)),(p9 - (r9 `2))) is V11() real ext-real set
((p - (r9 `1)) ^2) + ((p9 - (r9 `2)) ^2) is V11() real ext-real Element of REAL
sqrt ((p - (r9 `1)) ^2) is V11() real ext-real Element of REAL
sqrt (((p - (r9 `1)) ^2) + ((p9 - (r9 `2)) ^2)) is V11() real ext-real Element of REAL
|[(r9 `1),(r9 `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
abs (p - (r9 `1)) is V11() real ext-real Element of REAL
(r9 `1) - p is V11() real ext-real Element of REAL
K36((r9 `1),K38(p)) is V11() real ext-real set
- (p - (r9 `1)) is V11() real ext-real Element of REAL
abs (- (p - (r9 `1))) is V11() real ext-real Element of REAL
s1 is Element of K6( the carrier of (TOP-REAL 2))
n is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))
len n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
v_strip (n,(len n)) is Element of K6( the carrier of (TOP-REAL 2))
Int (v_strip (n,(len n))) is open Element of K6( the carrier of (TOP-REAL 2))
n * ((len n),1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(n * ((len n),1)) `1 is V11() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() real ext-real Element of REAL : not b<sub>1</sub> <= (n * ((len n),1)) `1 } is set
width n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
{ |[b₁,b₂]| where b₁, b₂ is V11() real ext-real Element of REAL : (n * ((len n),1)) `1 <= b<sub>1</sub> } is set
A is set
p is Element of the carrier of (Euclid 2)
p9 is V11() real ext-real set
Ball (p,p9) is Element of K6( the carrier of (Euclid 2))
s is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
s `1 is V11() real ext-real Element of REAL
s `2 is V11() real ext-real Element of REAL
|[(s `1),(s `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
s1 is V11() real ext-real Element of REAL
s1 / 2 is V11() real ext-real Element of REAL
K39(2) is non empty V11() real ext-real positive non negative set
K37(s1,K39(2)) is V11() real ext-real set
(s `1) - (s1 / 2) is V11() real ext-real Element of REAL
K38((s1 / 2)) is V11() real ext-real set
K36((s `1),K38((s1 / 2))) is V11() real ext-real set
(s `2) + 0 is V11() real ext-real Element of REAL
|[((s `1) - (s1 / 2)),((s `2) + 0)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
Ball (p,s1) is Element of K6( the carrier of (Euclid 2))
r9 is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
|[r9,r]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
((n * ((len n),1)) `1) + (s1 / 2) is V11() real ext-real Element of REAL
A is set
p is V11() real ext-real Element of REAL
p9 is V11() real ext-real Element of REAL
|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
s is Element of the carrier of (Euclid 2)
p - ((n * ((len n),1)) `1) is V11() real ext-real Element of REAL
K38(((n * ((len n),1)) `1)) is V11() real ext-real set
K36(p,K38(((n * ((len n),1)) `1))) is V11() real ext-real set
Ball (s,(p - ((n * ((len n),1)) `1))) is Element of K6( the carrier of (Euclid 2))
s1 is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of (Euclid 2) : not p - ((n * ((len n),1)) `1) <= dist (s,b₁) } is set
G is Element of the carrier of (Euclid 2)
dist (s,G) is V11() real ext-real Element of REAL
r9 is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
r9 `1 is V11() real ext-real Element of REAL
p - (r9 `1) is V11() real ext-real Element of REAL
K38((r9 `1)) is V11() real ext-real set
K36(p,K38((r9 `1))) is V11() real ext-real set
(p - (r9 `1)) ^2 is V11() real ext-real Element of REAL
K37((p - (r9 `1)),(p - (r9 `1))) is V11() real ext-real set
((p - (r9 `1)) ^2) + 0 is V11() real ext-real Element of REAL
r9 `2 is V11() real ext-real Element of REAL
p9 - (r9 `2) is V11() real ext-real Element of REAL
K38((r9 `2)) is V11() real ext-real set
K36(p9,K38((r9 `2))) is V11() real ext-real set
(p9 - (r9 `2)) ^2 is V11() real ext-real Element of REAL
K37((p9 - (r9 `2)),(p9 - (r9 `2))) is V11() real ext-real set
((p - (r9 `1)) ^2) + ((p9 - (r9 `2)) ^2) is V11() real ext-real Element of REAL
sqrt ((p - (r9 `1)) ^2) is V11() real ext-real Element of REAL
sqrt (((p - (r9 `1)) ^2) + ((p9 - (r9 `2)) ^2)) is V11() real ext-real Element of REAL
|[(r9 `1),(r9 `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
abs (p - (r9 `1)) is V11() real ext-real Element of REAL
s1 is Element of K6( the carrier of (TOP-REAL 2))
n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
n + 1 is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
A is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))
len A is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
v_strip (A,n) is Element of K6( the carrier of (TOP-REAL 2))
Int (v_strip (A,n)) is open Element of K6( the carrier of (TOP-REAL 2))
A * (n,1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(A * (n,1)) `1 is V11() real ext-real Element of REAL
A * ((n + 1),1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(A * ((n + 1),1)) `1 is V11() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() real ext-real Element of REAL : ( not b<sub>1</sub> <= (A * (n,1)) `1 & not (A * ((n + 1),1)) `1 <= b<sub>1</sub> ) } is set
width A is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() real ext-real Element of REAL : ( (A * (n,1)) `1 <= b₁ & b₁ <= (A * ((n + 1),1)) `1 ) } is set
p is set
p9 is Element of the carrier of (Euclid 2)
s is V11() real ext-real set
Ball (p9,s) is Element of K6( the carrier of (Euclid 2))
s1 is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
s1 `1 is V11() real ext-real Element of REAL
s1 `2 is V11() real ext-real Element of REAL
|[(s1 `1),(s1 `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
G is V11() real ext-real Element of REAL
G / 2 is V11() real ext-real Element of REAL
K39(2) is non empty V11() real ext-real positive non negative set
K37(G,K39(2)) is V11() real ext-real set
(s1 `1) - (G / 2) is V11() real ext-real Element of REAL
K38((G / 2)) is V11() real ext-real set
K36((s1 `1),K38((G / 2))) is V11() real ext-real set
(s1 `2) + 0 is V11() real ext-real Element of REAL
|[((s1 `1) - (G / 2)),((s1 `2) + 0)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
Ball (p9,G) is Element of K6( the carrier of (Euclid 2))
r is V11() real ext-real Element of REAL
rr is V11() real ext-real Element of REAL
|[r,rr]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
((A * (n,1)) `1) + (G / 2) is V11() real ext-real Element of REAL
(s1 `1) + (G / 2) is V11() real ext-real Element of REAL
|[((s1 `1) + (G / 2)),((s1 `2) + 0)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
rr is V11() real ext-real Element of REAL
rr9 is V11() real ext-real Element of REAL
|[rr,rr9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
p is set
p9 is V11() real ext-real Element of REAL
s is V11() real ext-real Element of REAL
|[p9,s]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
((A * ((n + 1),1)) `1) - p9 is V11() real ext-real Element of REAL
K38(p9) is V11() real ext-real set
K36(((A * ((n + 1),1)) `1),K38(p9)) is V11() real ext-real set
p9 - ((A * (n,1)) `1) is V11() real ext-real Element of REAL
K38(((A * (n,1)) `1)) is V11() real ext-real set
K36(p9,K38(((A * (n,1)) `1))) is V11() real ext-real set
min ((p9 - ((A * (n,1)) `1)),(((A * ((n + 1),1)) `1) - p9)) is V11() real ext-real Element of REAL
s1 is Element of the carrier of (Euclid 2)
Ball (s1,(min ((p9 - ((A * (n,1)) `1)),(((A * ((n + 1),1)) `1) - p9)))) is Element of K6( the carrier of (Euclid 2))
G is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of (Euclid 2) : not min ((p9 - ((A * (n,1)) `1)),(((A * ((n + 1),1)) `1) - p9)) <= dist (s1,b<sub>1</sub>) } is set
r9 is Element of the carrier of (Euclid 2)
dist (s1,r9) is V11() real ext-real Element of REAL
r is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
r `1 is V11() real ext-real Element of REAL
p9 - (r `1) is V11() real ext-real Element of REAL
K38((r `1)) is V11() real ext-real set
K36(p9,K38((r `1))) is V11() real ext-real set
(p9 - (r `1)) ^2 is V11() real ext-real Element of REAL
K37((p9 - (r `1)),(p9 - (r `1))) is V11() real ext-real set
((p9 - (r `1)) ^2) + 0 is V11() real ext-real Element of REAL
r `2 is V11() real ext-real Element of REAL
s - (r `2) is V11() real ext-real Element of REAL
K38((r `2)) is V11() real ext-real set
K36(s,K38((r `2))) is V11() real ext-real set
(s - (r `2)) ^2 is V11() real ext-real Element of REAL
K37((s - (r `2)),(s - (r `2))) is V11() real ext-real set
((p9 - (r `1)) ^2) + ((s - (r `2)) ^2) is V11() real ext-real Element of REAL
sqrt ((p9 - (r `1)) ^2) is V11() real ext-real Element of REAL
sqrt (((p9 - (r `1)) ^2) + ((s - (r `2)) ^2)) is V11() real ext-real Element of REAL
|[(r `1),(r `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
abs (p9 - (r `1)) is V11() real ext-real Element of REAL
(r `1) - p9 is V11() real ext-real Element of REAL
K36((r `1),K38(p9)) is V11() real ext-real set
- (p9 - (r `1)) is V11() real ext-real Element of REAL
abs (- (p9 - (r `1))) is V11() real ext-real Element of REAL
G is Element of K6( the carrier of (TOP-REAL 2))
n is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))
h_strip (n,0) is Element of K6( the carrier of (TOP-REAL 2))
Int (h_strip (n,0)) is open Element of K6( the carrier of (TOP-REAL 2))
n * (1,1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(n * (1,1)) `2 is V11() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() real ext-real Element of REAL : not (n * (1,1)) `2 <= b₂ } is set
len n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
{ |[b₁,b₂]| where b₁, b₂ is V11() real ext-real Element of REAL : b₂ <= (n * (1,1)) `2 } is set
A is set
p is Element of the carrier of (Euclid 2)
p9 is V11() real ext-real set
Ball (p,p9) is Element of K6( the carrier of (Euclid 2))
s is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
s `1 is V11() real ext-real Element of REAL
s `2 is V11() real ext-real Element of REAL
|[(s `1),(s `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(s `1) + 0 is V11() real ext-real Element of REAL
s1 is V11() real ext-real Element of REAL
s1 / 2 is V11() real ext-real Element of REAL
K39(2) is non empty V11() real ext-real positive non negative set
K37(s1,K39(2)) is V11() real ext-real set
(s `2) + (s1 / 2) is V11() real ext-real Element of REAL
|[((s `1) + 0),((s `2) + (s1 / 2))]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
Ball (p,s1) is Element of K6( the carrier of (Euclid 2))
r9 is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
|[r9,r]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
A is set
p is V11() real ext-real Element of REAL
p9 is V11() real ext-real Element of REAL
|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
s is Element of the carrier of (Euclid 2)
((n * (1,1)) `2) - p9 is V11() real ext-real Element of REAL
K38(p9) is V11() real ext-real set
K36(((n * (1,1)) `2),K38(p9)) is V11() real ext-real set
Ball (s,(((n * (1,1)) `2) - p9)) is Element of K6( the carrier of (Euclid 2))
s1 is set
{ b₁ where b₁ is Element of the carrier of (Euclid 2) : not ((n * (1,1)) `2) - p9 <= dist (s,b<sub>1</sub>) } is set
G is Element of the carrier of (Euclid 2)
dist (s,G) is V11() real ext-real Element of REAL
r9 is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
r9 `2 is V11() real ext-real Element of REAL
p9 - (r9 `2) is V11() real ext-real Element of REAL
K38((r9 `2)) is V11() real ext-real set
K36(p9,K38((r9 `2))) is V11() real ext-real set
(p9 - (r9 `2)) ^2 is V11() real ext-real Element of REAL
K37((p9 - (r9 `2)),(p9 - (r9 `2))) is V11() real ext-real set
((p9 - (r9 `2)) ^2) + 0 is V11() real ext-real Element of REAL
r9 `1 is V11() real ext-real Element of REAL
p - (r9 `1) is V11() real ext-real Element of REAL
K38((r9 `1)) is V11() real ext-real set
K36(p,K38((r9 `1))) is V11() real ext-real set
(p - (r9 `1)) ^2 is V11() real ext-real Element of REAL
K37((p - (r9 `1)),(p - (r9 `1))) is V11() real ext-real set
((p - (r9 `1)) ^2) + ((p9 - (r9 `2)) ^2) is V11() real ext-real Element of REAL
sqrt ((p9 - (r9 `2)) ^2) is V11() real ext-real Element of REAL
sqrt (((p - (r9 `1)) ^2) + ((p9 - (r9 `2)) ^2)) is V11() real ext-real Element of REAL
|[(r9 `1),(r9 `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
abs (p9 - (r9 `2)) is V11() real ext-real Element of REAL
(r9 `2) - p9 is V11() real ext-real Element of REAL
K36((r9 `2),K38(p9)) is V11() real ext-real set
- (p9 - (r9 `2)) is V11() real ext-real Element of REAL
abs (- (p9 - (r9 `2))) is V11() real ext-real Element of REAL
s1 is Element of K6( the carrier of (TOP-REAL 2))
n is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))
width n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
h_strip (n,(width n)) is Element of K6( the carrier of (TOP-REAL 2))
Int (h_strip (n,(width n))) is open Element of K6( the carrier of (TOP-REAL 2))
n * (1,(width n)) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(n * (1,(width n))) `2 is V11() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() real ext-real Element of REAL : not b<sub>2</sub> <= (n * (1,(width n))) `2 } is set
len n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
{ |[b₁,b₂]| where b₁, b₂ is V11() real ext-real Element of REAL : (n * (1,(width n))) `2 <= b<sub>2</sub> } is set
A is set
p is Element of the carrier of (Euclid 2)
p9 is V11() real ext-real set
Ball (p,p9) is Element of K6( the carrier of (Euclid 2))
s is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
s `1 is V11() real ext-real Element of REAL
s `2 is V11() real ext-real Element of REAL
|[(s `1),(s `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(s `1) + 0 is V11() real ext-real Element of REAL
s1 is V11() real ext-real Element of REAL
s1 / 2 is V11() real ext-real Element of REAL
K39(2) is non empty V11() real ext-real positive non negative set
K37(s1,K39(2)) is V11() real ext-real set
(s `2) - (s1 / 2) is V11() real ext-real Element of REAL
K38((s1 / 2)) is V11() real ext-real set
K36((s `2),K38((s1 / 2))) is V11() real ext-real set
|[((s `1) + 0),((s `2) - (s1 / 2))]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
Ball (p,s1) is Element of K6( the carrier of (Euclid 2))
r9 is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
|[r9,r]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
((n * (1,(width n))) `2) + (s1 / 2) is V11() real ext-real Element of REAL
A is set
p is V11() real ext-real Element of REAL
p9 is V11() real ext-real Element of REAL
|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
s is Element of the carrier of (Euclid 2)
p9 - ((n * (1,(width n))) `2) is V11() real ext-real Element of REAL
K38(((n * (1,(width n))) `2)) is V11() real ext-real set
K36(p9,K38(((n * (1,(width n))) `2))) is V11() real ext-real set
Ball (s,(p9 - ((n * (1,(width n))) `2))) is Element of K6( the carrier of (Euclid 2))
s1 is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of (Euclid 2) : not p9 - ((n * (1,(width n))) `2) <= dist (s,b₁) } is set
G is Element of the carrier of (Euclid 2)
dist (s,G) is V11() real ext-real Element of REAL
r9 is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
r9 `2 is V11() real ext-real Element of REAL
p9 - (r9 `2) is V11() real ext-real Element of REAL
K38((r9 `2)) is V11() real ext-real set
K36(p9,K38((r9 `2))) is V11() real ext-real set
(p9 - (r9 `2)) ^2 is V11() real ext-real Element of REAL
K37((p9 - (r9 `2)),(p9 - (r9 `2))) is V11() real ext-real set
((p9 - (r9 `2)) ^2) + 0 is V11() real ext-real Element of REAL
r9 `1 is V11() real ext-real Element of REAL
p - (r9 `1) is V11() real ext-real Element of REAL
K38((r9 `1)) is V11() real ext-real set
K36(p,K38((r9 `1))) is V11() real ext-real set
(p - (r9 `1)) ^2 is V11() real ext-real Element of REAL
K37((p - (r9 `1)),(p - (r9 `1))) is V11() real ext-real set
((p - (r9 `1)) ^2) + ((p9 - (r9 `2)) ^2) is V11() real ext-real Element of REAL
sqrt ((p9 - (r9 `2)) ^2) is V11() real ext-real Element of REAL
sqrt (((p - (r9 `1)) ^2) + ((p9 - (r9 `2)) ^2)) is V11() real ext-real Element of REAL
|[(r9 `1),(r9 `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
abs (p9 - (r9 `2)) is V11() real ext-real Element of REAL
s1 is Element of K6( the carrier of (TOP-REAL 2))
n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
n + 1 is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
A is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))
width A is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
h_strip (A,n) is Element of K6( the carrier of (TOP-REAL 2))
Int (h_strip (A,n)) is open Element of K6( the carrier of (TOP-REAL 2))
A * (1,n) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(A * (1,n)) `2 is V11() real ext-real Element of REAL
A * (1,(n + 1)) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(A * (1,(n + 1))) `2 is V11() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() real ext-real Element of REAL : ( not b<sub>2</sub> <= (A * (1,n)) `2 & not (A * (1,(n + 1))) `2 <= b<sub>2</sub> ) } is set
len A is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() real ext-real Element of REAL : ( (A * (1,n)) `2 <= b₂ & b₂ <= (A * (1,(n + 1))) `2 ) } is set
p is set
p9 is Element of the carrier of (Euclid 2)
s is V11() real ext-real set
Ball (p9,s) is Element of K6( the carrier of (Euclid 2))
s1 is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
s1 `1 is V11() real ext-real Element of REAL
s1 `2 is V11() real ext-real Element of REAL
|[(s1 `1),(s1 `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(s1 `1) + 0 is V11() real ext-real Element of REAL
G is V11() real ext-real Element of REAL
G / 2 is V11() real ext-real Element of REAL
K39(2) is non empty V11() real ext-real positive non negative set
K37(G,K39(2)) is V11() real ext-real set
(s1 `2) - (G / 2) is V11() real ext-real Element of REAL
K38((G / 2)) is V11() real ext-real set
K36((s1 `2),K38((G / 2))) is V11() real ext-real set
|[((s1 `1) + 0),((s1 `2) - (G / 2))]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
Ball (p9,G) is Element of K6( the carrier of (Euclid 2))
r is V11() real ext-real Element of REAL
rr is V11() real ext-real Element of REAL
|[r,rr]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
((A * (1,n)) `2) + (G / 2) is V11() real ext-real Element of REAL
(s1 `2) + (G / 2) is V11() real ext-real Element of REAL
|[((s1 `1) + 0),((s1 `2) + (G / 2))]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
rr is V11() real ext-real Element of REAL
rr9 is V11() real ext-real Element of REAL
|[rr,rr9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
p is set
p9 is V11() real ext-real Element of REAL
s is V11() real ext-real Element of REAL
|[p9,s]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
((A * (1,(n + 1))) `2) - s is V11() real ext-real Element of REAL
K38(s) is V11() real ext-real set
K36(((A * (1,(n + 1))) `2),K38(s)) is V11() real ext-real set
s - ((A * (1,n)) `2) is V11() real ext-real Element of REAL
K38(((A * (1,n)) `2)) is V11() real ext-real set
K36(s,K38(((A * (1,n)) `2))) is V11() real ext-real set
min ((s - ((A * (1,n)) `2)),(((A * (1,(n + 1))) `2) - s)) is V11() real ext-real Element of REAL
s1 is Element of the carrier of (Euclid 2)
Ball (s1,(min ((s - ((A * (1,n)) `2)),(((A * (1,(n + 1))) `2) - s)))) is Element of K6( the carrier of (Euclid 2))
G is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of (Euclid 2) : not min ((s - ((A * (1,n)) `2)),(((A * (1,(n + 1))) `2) - s)) <= dist (s1,b<sub>1</sub>) } is set
r9 is Element of the carrier of (Euclid 2)
dist (s1,r9) is V11() real ext-real Element of REAL
r is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
r `2 is V11() real ext-real Element of REAL
s - (r `2) is V11() real ext-real Element of REAL
K38((r `2)) is V11() real ext-real set
K36(s,K38((r `2))) is V11() real ext-real set
(s - (r `2)) ^2 is V11() real ext-real Element of REAL
K37((s - (r `2)),(s - (r `2))) is V11() real ext-real set
((s - (r `2)) ^2) + 0 is V11() real ext-real Element of REAL
r `1 is V11() real ext-real Element of REAL
p9 - (r `1) is V11() real ext-real Element of REAL
K38((r `1)) is V11() real ext-real set
K36(p9,K38((r `1))) is V11() real ext-real set
(p9 - (r `1)) ^2 is V11() real ext-real Element of REAL
K37((p9 - (r `1)),(p9 - (r `1))) is V11() real ext-real set
((p9 - (r `1)) ^2) + ((s - (r `2)) ^2) is V11() real ext-real Element of REAL
sqrt ((s - (r `2)) ^2) is V11() real ext-real Element of REAL
sqrt (((p9 - (r `1)) ^2) + ((s - (r `2)) ^2)) is V11() real ext-real Element of REAL
|[(r `1),(r `2)]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
abs (s - (r `2)) is V11() real ext-real Element of REAL
(r `2) - s is V11() real ext-real Element of REAL
K36((r `2),K38(s)) is V11() real ext-real set
- (s - (r `2)) is V11() real ext-real Element of REAL
abs (- (s - (r `2))) is V11() real ext-real Element of REAL
G is Element of K6( the carrier of (TOP-REAL 2))
n is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))
cell (n,0,0) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell (n,0,0)) is open Element of K6( the carrier of (TOP-REAL 2))
n * (1,1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(n * (1,1)) `1 is V11() real ext-real Element of REAL
(n * (1,1)) `2 is V11() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V11() real ext-real Element of REAL : ( not (n * (1,1)) `1 <= b<sub>1</sub> & not (n * (1,1)) `2 <= b₂ ) } is set
v_strip (n,0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (n,0) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (n,0)) /\ (h_strip (n,0)) is Element of K6( the carrier of (TOP-REAL 2))
Int (v_strip (n,0)) is open Element of K6( the carrier of (TOP-REAL 2))
Int (h_strip (n,0)) is open Element of K6( the carrier of (TOP-REAL 2))
(Int (v_strip (n,0))) /\ (Int (h_strip (n,0))) is open Element of K6( the carrier of (TOP-REAL 2))
{ |[b₁,b₂]| where b₁, b₂ is V11() real ext-real Element of REAL : not (n * (1,1)) `2 <= b<sub>2</sub> } is set
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() real ext-real Element of REAL : not (n * (1,1)) `1 <= b₁ } is set
A is set
p is V11() real ext-real Element of REAL
p9 is V11() real ext-real Element of REAL
|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
s is V11() real ext-real Element of REAL
s1 is V11() real ext-real Element of REAL
|[s,s1]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
A is set
p is V11() real ext-real Element of REAL
p9 is V11() real ext-real Element of REAL
|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
p9 is V11() real ext-real Element of REAL
|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
n is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))
width n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
cell (n,0,(width n)) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell (n,0,(width n))) is open Element of K6( the carrier of (TOP-REAL 2))
n * (1,1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(n * (1,1)) `1 is V11() real ext-real Element of REAL
n * (1,(width n)) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(n * (1,(width n))) `2 is V11() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V11() real ext-real Element of REAL : ( not (n * (1,1)) `1 <= b<sub>1</sub> & not b<sub>2</sub> <= (n * (1,(width n))) `2 ) } is set
v_strip (n,0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (n,(width n)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (n,0)) /\ (h_strip (n,(width n))) is Element of K6( the carrier of (TOP-REAL 2))
Int (v_strip (n,0)) is open Element of K6( the carrier of (TOP-REAL 2))
Int (h_strip (n,(width n))) is open Element of K6( the carrier of (TOP-REAL 2))
(Int (v_strip (n,0))) /\ (Int (h_strip (n,(width n)))) is open Element of K6( the carrier of (TOP-REAL 2))
{ |[b₁,b₂]| where b₁, b₂ is V11() real ext-real Element of REAL : not b₂ <= (n * (1,(width n))) `2 } is set
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() real ext-real Element of REAL : not (n * (1,1)) `1 <= b₁ } is set
A is set
p is V11() real ext-real Element of REAL
p9 is V11() real ext-real Element of REAL
|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
s is V11() real ext-real Element of REAL
s1 is V11() real ext-real Element of REAL
|[s,s1]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
A is set
p is V11() real ext-real Element of REAL
p9 is V11() real ext-real Element of REAL
|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
p9 is V11() real ext-real Element of REAL
|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
n + 1 is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
A is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))
width A is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
cell (A,0,n) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell (A,0,n)) is open Element of K6( the carrier of (TOP-REAL 2))
A * (1,1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(A * (1,1)) `1 is V11() real ext-real Element of REAL
A * (1,n) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(A * (1,n)) `2 is V11() real ext-real Element of REAL
A * (1,(n + 1)) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(A * (1,(n + 1))) `2 is V11() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() real ext-real Element of REAL : ( not (A * (1,1)) `1 <= b₁ & not b₂ <= (A * (1,n)) `2 & not (A * (1,(n + 1))) `2 <= b₂ ) } is set
v_strip (A,0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (A,n) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (A,0)) /\ (h_strip (A,n)) is Element of K6( the carrier of (TOP-REAL 2))
Int (v_strip (A,0)) is open Element of K6( the carrier of (TOP-REAL 2))
Int (h_strip (A,n)) is open Element of K6( the carrier of (TOP-REAL 2))
(Int (v_strip (A,0))) /\ (Int (h_strip (A,n))) is open Element of K6( the carrier of (TOP-REAL 2))
{ |[b₁,b₂]| where b₁, b₂ is V11() real ext-real Element of REAL : ( not b₂ <= (A * (1,n)) `2 & not (A * (1,(n + 1))) `2 <= b₂ ) } is set
{ |[b₁,b₂]| where b₁, b₂ is V11() real ext-real Element of REAL : not (A * (1,1)) `1 <= b<sub>1</sub> } is set
p is set
p9 is V11() real ext-real Element of REAL
s is V11() real ext-real Element of REAL
|[p9,s]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
s1 is V11() real ext-real Element of REAL
G is V11() real ext-real Element of REAL
|[s1,G]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
p is set
p9 is V11() real ext-real Element of REAL
s is V11() real ext-real Element of REAL
|[p9,s]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
p9 is V11() real ext-real Element of REAL
s is V11() real ext-real Element of REAL
|[p9,s]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
n is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))
len n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
cell (n,(len n),0) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell (n,(len n),0)) is open Element of K6( the carrier of (TOP-REAL 2))
n * ((len n),1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(n * ((len n),1)) `1 is V11() real ext-real Element of REAL
n * (1,1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(n * (1,1)) `2 is V11() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() real ext-real Element of REAL : ( not b<sub>1</sub> <= (n * ((len n),1)) `1 & not (n * (1,1)) `2 <= b<sub>2</sub> ) } is set
v_strip (n,(len n)) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (n,0) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (n,(len n))) /\ (h_strip (n,0)) is Element of K6( the carrier of (TOP-REAL 2))
Int (v_strip (n,(len n))) is open Element of K6( the carrier of (TOP-REAL 2))
Int (h_strip (n,0)) is open Element of K6( the carrier of (TOP-REAL 2))
(Int (v_strip (n,(len n)))) /\ (Int (h_strip (n,0))) is open Element of K6( the carrier of (TOP-REAL 2))
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() real ext-real Element of REAL : not (n * (1,1)) `2 <= b₂ } is set
{ |[b₁,b₂]| where b₁, b₂ is V11() real ext-real Element of REAL : not b₁ <= (n * ((len n),1)) `1 } is set
A is set
p is V11() real ext-real Element of REAL
p9 is V11() real ext-real Element of REAL
|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
s is V11() real ext-real Element of REAL
s1 is V11() real ext-real Element of REAL
|[s,s1]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
A is set
p is V11() real ext-real Element of REAL
p9 is V11() real ext-real Element of REAL
|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
p is V11() real ext-real Element of REAL
p9 is V11() real ext-real Element of REAL
|[p,p9]| is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
n is V16() V18() V19( NAT ) V20(K246( the carrier of (TOP-REAL 2))) V21() FinSequence-like V144() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))
len n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
width n is natural V11() real ext-real V33() V156() V157() V158() V159() V160() V161() V162() Element of NAT
cell (n,(len n),(width n)) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell (n,(len n),(width n))) is open Element of K6( the carrier of (TOP-REAL 2))
n * ((len n),1) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(n * ((len n),1)) `1 is V11() real ext-real Element of REAL
n * (1,(width n)) is V42(2) FinSequence-like V148() Element of the carrier of (TOP-REAL 2)
(n * (1,(width n))) `2 is V11() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() real ext-real Element of REAL : ( not b<sub>1</sub> <= (n * ((len n),1)) `1 & not b₂ <= (n * (1,(width n))) `2 ) } is set
v_strip (n,(len n)) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (n,(width n)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (n,(len n))) /\ (h_strip (n,(width n))) is Element of K6( the carrier of (