:: ALI2 semantic presentation

REAL is non empty non finite V110() V111() V112() V116() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V110() V111() V112() V113() V114() V115() V116() Element of K10(REAL)
K10(REAL) is non empty set
omega is non empty epsilon-transitive epsilon-connected ordinal V110() V111() V112() V113() V114() V115() V116() set
K10(omega) is non empty set
1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
K11(1,1) is non empty set
K10(K11(1,1)) is non empty set
K11(K11(1,1),1) is non empty set
K10(K11(K11(1,1),1)) is non empty set
K11(K11(1,1),REAL) is non empty set
K10(K11(K11(1,1),REAL)) is non empty set
K11(REAL,REAL) is non empty set
K11(K11(REAL,REAL),REAL) is non empty set
K10(K11(K11(REAL,REAL),REAL)) is non empty set
2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
K11(2,2) is non empty set
K11(K11(2,2),REAL) is non empty set
K10(K11(K11(2,2),REAL)) is non empty set
COMPLEX is non empty non finite V110() V116() set
RAT is non empty non finite V110() V111() V112() V113() V116() set
INT is non empty non finite V110() V111() V112() V113() V114() V116() set
K11(COMPLEX,COMPLEX) is non empty set
K10(K11(COMPLEX,COMPLEX)) is non empty set
K11(K11(COMPLEX,COMPLEX),COMPLEX) is non empty set
K10(K11(K11(COMPLEX,COMPLEX),COMPLEX)) is non empty set
K10(K11(REAL,REAL)) is non empty set
K11(RAT,RAT) is non empty set
K10(K11(RAT,RAT)) is non empty set
K11(K11(RAT,RAT),RAT) is non empty set
K10(K11(K11(RAT,RAT),RAT)) is non empty set
K11(INT,INT) is non empty set
K10(K11(INT,INT)) is non empty set
K11(K11(INT,INT),INT) is non empty set
K10(K11(K11(INT,INT),INT)) is non empty set
K11(NAT,NAT) is non empty set
K11(K11(NAT,NAT),NAT) is non empty set
K10(K11(K11(NAT,NAT),NAT)) is non empty set
K10(NAT) is non empty set
{} is set
the empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V41() V42() V110() V111() V112() V113() V114() V115() V116() set is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V41() V42() V110() V111() V112() V113() V114() V115() V116() set
0 is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
K11(NAT,REAL) is non empty set
K10(K11(NAT,REAL)) is non empty set
M is non empty Reflexive discerning V100() triangle Discerning MetrStruct
the carrier of M is non empty set
K11( the carrier of M, the carrier of M) is non empty set
K10(K11( the carrier of M, the carrier of M)) is non empty set
M is non empty Reflexive discerning V100() triangle Discerning MetrStruct
the carrier of M is non empty set
K11( the carrier of M, the carrier of M) is non empty set
K10(K11( the carrier of M, the carrier of M)) is non empty set
the Element of the carrier of M is Element of the carrier of M
the carrier of M --> the Element of the carrier of M is non empty V7() V10( the carrier of M) V11( the carrier of M) V12() V14() V17( the carrier of M) V21( the carrier of M, the carrier of M) Element of K10(K11( the carrier of M, the carrier of M))
x0 is non empty V12() V17( the carrier of M) V21( the carrier of M, the carrier of M) Element of K10(K11( the carrier of M, the carrier of M))
1 / 2 is ext-real non negative V41() V42() Element of REAL
a is Element of the carrier of M
x0 . a is Element of the carrier of M
L is Element of the carrier of M
x0 . L is Element of the carrier of M
dist ((x0 . a),(x0 . L)) is ext-real V41() V42() Element of REAL
dist (a,L) is ext-real V41() V42() Element of REAL
(1 / 2) * (dist (a,L)) is ext-real V41() V42() Element of REAL
M is non empty Reflexive discerning V100() triangle Discerning MetrStruct
the carrier of M is non empty set
K11( the carrier of M, the carrier of M) is non empty set
K10(K11( the carrier of M, the carrier of M)) is non empty set
TopSpaceMetr M is non empty strict TopSpace-like TopStruct
f is non empty V12() V17( the carrier of M) V21( the carrier of M, the carrier of M) (M) Element of K10(K11( the carrier of M, the carrier of M))
the Element of the carrier of M is Element of the carrier of M
f . the Element of the carrier of M is Element of the carrier of M
dist ( the Element of the carrier of M,(f . the Element of the carrier of M)) is ext-real V41() V42() Element of REAL
L is ext-real V41() V42() Element of REAL
the carrier of (TopSpaceMetr M) is non empty set
K10( the carrier of (TopSpaceMetr M)) is non empty set
K10(K10( the carrier of (TopSpaceMetr M))) is non empty set
c is Element of K10(K10( the carrier of (TopSpaceMetr M)))
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
L to_power (0 + 1) is ext-real V41() V42() Element of REAL
(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power (0 + 1)) is ext-real V41() V42() Element of REAL
x is Element of K10( the carrier of (TopSpaceMetr M))
Family_open_set M is Element of K10(K10( the carrier of M))
K10( the carrier of M) is non empty set
K10(K10( the carrier of M)) is non empty set
TopStruct(# the carrier of M,(Family_open_set M) #) is strict TopStruct
x ` is Element of K10( the carrier of (TopSpaceMetr M))
the carrier of (TopSpaceMetr M) \ x is set
r is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
L to_power r is ext-real V41() V42() Element of REAL
(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power r) is ext-real V41() V42() Element of REAL
{ b₁ where b₁ is Element of the carrier of M : dist (b₁,(f . b₁)) <= (dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power r) } is set
c is Element of K10( the carrier of M)
s9 is Element of the carrier of M
f . s9 is Element of the carrier of M
dist (s9,(f . s9)) is ext-real V41() V42() Element of REAL
(dist (s9,(f . s9))) - ((dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power r)) is ext-real V41() V42() Element of REAL
((dist (s9,(f . s9))) - ((dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power r))) / 2 is ext-real V41() V42() Element of REAL
s is ext-real V41() V42() Element of REAL
Ball (s9,s) is Element of K10( the carrier of M)
n is set
B is Element of the carrier of M
dist (s9,B) is ext-real V41() V42() Element of REAL
2 * s is ext-real V41() V42() Element of REAL
2 * (dist (s9,B)) is ext-real V41() V42() Element of REAL
f . B is Element of the carrier of M
dist (B,(f . B)) is ext-real V41() V42() Element of REAL
(dist (B,(f . B))) + (2 * s) is ext-real V41() V42() Element of REAL
(dist (B,(f . B))) + (2 * (dist (s9,B))) is ext-real V41() V42() Element of REAL
dist (s9,(f . B)) is ext-real V41() V42() Element of REAL
(dist (s9,B)) + (dist (B,(f . B))) is ext-real V41() V42() Element of REAL
dist ((f . B),(f . s9)) is ext-real V41() V42() Element of REAL
(dist (s9,(f . B))) + (dist ((f . B),(f . s9))) is ext-real V41() V42() Element of REAL
((dist (s9,B)) + (dist (B,(f . B)))) + (dist ((f . B),(f . s9))) is ext-real V41() V42() Element of REAL
dist (B,s9) is ext-real V41() V42() Element of REAL
L * (dist (B,s9)) is ext-real V41() V42() Element of REAL
(dist ((f . B),(f . s9))) + (dist (B,s9)) is ext-real V41() V42() Element of REAL
(dist (B,s9)) + (dist (B,s9)) is ext-real V41() V42() Element of REAL
(dist (B,s9)) + (dist ((f . B),(f . s9))) is ext-real V41() V42() Element of REAL
(dist (B,(f . B))) + ((dist (B,s9)) + (dist ((f . B),(f . s9)))) is ext-real V41() V42() Element of REAL
2 * (dist (B,s9)) is ext-real V41() V42() Element of REAL
(dist (B,(f . B))) + (2 * (dist (B,s9))) is ext-real V41() V42() Element of REAL
(dist (B,(f . B))) + (dist (s9,B)) is ext-real V41() V42() Element of REAL
((dist (B,(f . B))) + (dist (s9,B))) + (dist ((f . B),(f . s9))) is ext-real V41() V42() Element of REAL
(dist (s9,(f . s9))) - (2 * s) is ext-real V41() V42() Element of REAL
c₁₄ is Element of the carrier of M
f . c₁₄ is Element of the carrier of M
dist (c₁₄,(f . c₁₄)) is ext-real V41() V42() Element of REAL
Family_open_set M is Element of K10(K10( the carrier of M))
K10( the carrier of M) is non empty set
K10(K10( the carrier of M)) is non empty set
TopStruct(# the carrier of M,(Family_open_set M) #) is strict TopStruct
{ b₁ where b₁ is Element of the carrier of M : S₂[b₁] } is set
{ b₁ where b₁ is Element of the carrier of M : dist (b₁,(f . b₁)) <= (dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power a₁) } is set
x is set
meet x is set
c is set
r is set
s9 is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
L to_power s9 is ext-real V41() V42() Element of REAL
(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power s9) is ext-real V41() V42() Element of REAL
{ b₁ where b₁ is Element of the carrier of M : dist (b₁,(f . b₁)) <= (dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power s9) } is set
s is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
L to_power s is ext-real V41() V42() Element of REAL
(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power s) is ext-real V41() V42() Element of REAL
{ b₁ where b₁ is Element of the carrier of M : dist (b₁,(f . b₁)) <= (dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power s) } is set
n is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
B is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
L to_power B is ext-real V41() V42() Element of REAL
L to_power n is ext-real V41() V42() Element of REAL
n is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
B is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
L to_power B is ext-real V41() V42() Element of REAL
(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power B) is ext-real V41() V42() Element of REAL
L to_power n is ext-real V41() V42() Element of REAL
(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power n) is ext-real V41() V42() Element of REAL
n is set
B is Element of the carrier of M
f . B is Element of the carrier of M
dist (B,(f . B)) is ext-real V41() V42() Element of REAL
n is set
B is Element of the carrier of M
f . B is Element of the carrier of M
dist (B,(f . B)) is ext-real V41() V42() Element of REAL
c is set
r is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
L to_power r is ext-real V41() V42() Element of REAL
(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power r) is ext-real V41() V42() Element of REAL
{ b₁ where b₁ is Element of the carrier of M : dist (b₁,(f . b₁)) <= (dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power r) } is set
r + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
L to_power (r + 1) is ext-real V41() V42() Element of REAL
(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power (r + 1)) is ext-real V41() V42() Element of REAL
{ b₁ where b₁ is Element of the carrier of M : dist (b₁,(f . b₁)) <= (dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power (r + 1)) } is set
the Element of { b₁ where b₁ is Element of the carrier of M : dist (b₁,(f . b₁)) <= (dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power r) } is Element of { b₁ where b₁ is Element of the carrier of M : dist (b₁,(f . b₁)) <= (dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power r) }
L * ((dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power r)) is ext-real V41() V42() Element of REAL
L * (L to_power r) is ext-real V41() V42() Element of REAL
(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L * (L to_power r)) is ext-real V41() V42() Element of REAL
L to_power 1 is ext-real V41() V42() Element of REAL
(L to_power r) * (L to_power 1) is ext-real V41() V42() Element of REAL
(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * ((L to_power r) * (L to_power 1)) is ext-real V41() V42() Element of REAL
s is Element of the carrier of M
f . s is Element of the carrier of M
dist (s,(f . s)) is ext-real V41() V42() Element of REAL
f . (f . s) is Element of the carrier of M
dist ((f . s),(f . (f . s))) is ext-real V41() V42() Element of REAL
L * (dist (s,(f . s))) is ext-real V41() V42() Element of REAL
(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * 1 is ext-real V41() V42() Element of REAL
L to_power 0 is ext-real V41() V42() Element of REAL
(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power 0) is ext-real V41() V42() Element of REAL
{ b₁ where b₁ is Element of the carrier of M : dist (b₁,(f . b₁)) <= (dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power 0) } is set
meet c is Element of K10( the carrier of (TopSpaceMetr M))
x is Element of the carrier of (TopSpaceMetr M)
c is Element of the carrier of M
f . c is Element of the carrier of M
dist (c,(f . c)) is ext-real V41() V42() Element of REAL
NAT --> (dist (c,(f . c))) is non empty V7() V10( NAT ) V11( REAL ) V12() V14() V17( NAT ) V21( NAT , REAL ) convergent Element of K10(K11(NAT,REAL))
s9 is non empty V12() V17( NAT ) V21( NAT , REAL ) Element of K10(K11(NAT,REAL))
(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) (#) s9 is non empty V12() V17( NAT ) V21( NAT , REAL ) Element of K10(K11(NAT,REAL))
lim s9 is ext-real V41() V42() Element of REAL
lim ((dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) (#) s9) is ext-real V41() V42() Element of REAL
(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * 0 is ext-real V41() V42() Element of REAL
n is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
n + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT
L to_power (n + 1) is ext-real V41() V42() Element of REAL
(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power (n + 1)) is ext-real V41() V42() Element of REAL
{ b₁ where b₁ is Element of the carrier of M : S₃[b₁] } is set
((dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) (#) s9) . n is ext-real V41() V42() Element of REAL
s9 . n is ext-real V41() V42() Element of REAL
(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (s9 . n) is ext-real V41() V42() Element of REAL
r is non empty V12() V17( NAT ) V21( NAT , REAL ) Element of K10(K11(NAT,REAL))
r . n is ext-real V41() V42() Element of REAL
c₁₄ is Element of the carrier of M
f . c₁₄ is Element of the carrier of M
dist (c₁₄,(f . c₁₄)) is ext-real V41() V42() Element of REAL
lim r is ext-real V41() V42() Element of REAL
r . 0 is ext-real V41() V42() Element of REAL
c is Element of the carrier of M
f . c is Element of the carrier of M
dist (c,(f . c)) is ext-real V41() V42() Element of REAL
c is Element of the carrier of M
f . c is Element of the carrier of M
dist (c,(f . c)) is ext-real V41() V42() Element of REAL
x is Element of the carrier of M
f . x is Element of the carrier of M
dist (x,c) is ext-real V41() V42() Element of REAL
L * (dist (x,c)) is ext-real V41() V42() Element of REAL