:: ALI2 semantic presentation
begin
definition
let
M
be ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) ;
let
f
be ( (
V12
()
V21
( the
carrier
of
M
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
M
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
)
set
) ) ) ( non
empty
V12
()
V17
( the
carrier
of
M
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
)
set
) )
V21
( the
carrier
of
M
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
M
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
)
set
) ) )
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) ;
attr
f
is
contraction
means
:: ALI2:def 1
ex
L
being ( ( ) (
ext-real
V41
()
V42
() )
Real
) st
(
0
: ( ( ) (
ext-real
epsilon-transitive
epsilon-connected
ordinal
natural
V41
()
V42
()
V108
()
V109
()
V110
()
V111
()
V112
()
V113
()
V114
()
V115
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V110
()
V111
()
V112
()
V113
()
V114
()
V115
()
V116
() )
Element
of
K10
(
REAL
: ( ( ) ( non
empty
non
finite
V110
()
V111
()
V112
()
V116
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
<
L
: ( ( ) (
ext-real
V41
()
V42
() )
Real
) &
L
: ( ( ) (
ext-real
V41
()
V42
() )
Real
)
<
1 : ( ( ) ( 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
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V110
()
V111
()
V112
()
V113
()
V114
()
V115
()
V116
() )
Element
of
K10
(
REAL
: ( ( ) ( non
empty
non
finite
V110
()
V111
()
V112
()
V116
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) & ( for
x
,
y
being ( ( ) ( )
Point
of ( ( ) ( )
set
) ) holds
dist
(
(
f
: ( ( ) ( )
Element
of
K10
(
K10
(
M
: ( ( ) ( )
TopStruct
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
.
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
M
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) ,
(
f
: ( ( ) ( )
Element
of
K10
(
K10
(
M
: ( ( ) ( )
TopStruct
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
.
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
M
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) ) : ( ( ) (
ext-real
V41
()
V42
() )
Element
of
REAL
: ( ( ) ( non
empty
non
finite
V110
()
V111
()
V112
()
V116
() )
set
) )
<=
L
: ( ( ) (
ext-real
V41
()
V42
() )
Real
)
*
(
dist
(
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ,
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
)
: ( ( ) (
ext-real
V41
()
V42
() )
Element
of
REAL
: ( ( ) ( non
empty
non
finite
V110
()
V111
()
V112
()
V116
() )
set
) ) : ( ( ) (
ext-real
V41
()
V42
() )
Element
of
REAL
: ( ( ) ( non
empty
non
finite
V110
()
V111
()
V112
()
V116
() )
set
) ) ) );
end;
registration
let
M
be ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) ;
cluster
non
empty
V12
()
V17
( the
carrier
of
M
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrStruct
) : ( ( ) ( non
empty
)
set
) )
V21
( the
carrier
of
M
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrStruct
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
M
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrStruct
) : ( ( ) ( non
empty
)
set
) )
contraction
for ( ( ) ( )
Element
of
K10
(
K11
( the
carrier
of
M
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrStruct
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
M
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
definition
let
M
be ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) ;
mode
Contraction of
M
is
( (
V12
()
V21
( the
carrier
of
M
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrStruct
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
M
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrStruct
) : ( ( ) ( non
empty
)
set
) )
contraction
) ( non
empty
V12
()
V17
( the
carrier
of
M
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrStruct
) : ( ( ) ( non
empty
)
set
) )
V21
( the
carrier
of
M
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrStruct
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
M
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrStruct
) : ( ( ) ( non
empty
)
set
) )
contraction
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: ALI2:1
for
M
being ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
)
for
f
being ( (
V12
()
V21
( the
carrier
of
b
1
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
b
1
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
)
set
) )
contraction
) ( non
empty
V12
()
V17
( the
carrier
of
b
1
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
)
set
) )
V21
( the
carrier
of
b
1
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
b
1
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
)
set
) )
contraction
)
Contraction
of
M
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) ) st
TopSpaceMetr
M
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
strict
TopSpace-like
)
TopStruct
) is
compact
holds
ex
c
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
(
f
: ( (
V12
()
V21
( the
carrier
of
b
1
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
b
1
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
)
set
) )
contraction
) ( non
empty
V12
()
V17
( the
carrier
of
b
1
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
)
set
) )
V21
( the
carrier
of
b
1
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
b
1
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
)
set
) )
contraction
)
Contraction
of
b
1
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) )
.
c
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
)
set
) )
=
c
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) & ( for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
f
: ( (
V12
()
V21
( the
carrier
of
b
1
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
b
1
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
)
set
) )
contraction
) ( non
empty
V12
()
V17
( the
carrier
of
b
1
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
)
set
) )
V21
( the
carrier
of
b
1
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
b
1
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
)
set
) )
contraction
)
Contraction
of
b
1
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) )
.
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
Reflexive
discerning
V100
()
triangle
) ( non
empty
Reflexive
discerning
V100
()
triangle
Discerning
)
MetrSpace
) : ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
=
c
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) ) ;