:: COMPLSP1 semantic presentation
begin
definition
let
n
be ( ( ) (
V38
()
V39
()
V40
()
V41
()
V44
()
V45
()
V56
()
V57
()
V58
()
V59
()
V60
()
V61
() )
Element
of
NAT
: ( ( ) (
V56
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
K10
(
REAL
: ( ( ) ( non
empty
V56
()
V57
()
V58
()
V62
()
V63
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ;
func
the_Complex_Space
n
->
( (
strict
TopSpace-like
) (
strict
TopSpace-like
)
TopSpace
)
equals
:: COMPLSP1:def 1
TopStruct
(#
(
COMPLEX
n
: ( ( ) ( )
TopStruct
)
)
: ( ( ) (
V15
()
V83
() )
M13
(
COMPLEX
: ( ( ) ( non
empty
V56
()
V62
()
V63
() )
set
) )) ,
(
ComplexOpenSets
n
: ( ( ) ( )
TopStruct
)
)
: ( ( ) ( )
Element
of
K10
(
K10
(
(
COMPLEX
n
: ( ( ) ( )
TopStruct
)
)
: ( ( ) (
V15
()
V83
() )
M13
(
COMPLEX
: ( ( ) ( non
empty
V56
()
V62
()
V63
() )
set
) )) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) #) : ( (
strict
) (
strict
)
TopStruct
) ;
end;
registration
let
n
be ( ( ) (
V38
()
V39
()
V40
()
V41
()
V44
()
V45
()
V56
()
V57
()
V58
()
V59
()
V60
()
V61
() )
Element
of
NAT
: ( ( ) (
V56
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
K10
(
REAL
: ( ( ) ( non
empty
V56
()
V57
()
V58
()
V62
()
V63
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ;
cluster
the_Complex_Space
n
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V44
()
V45
()
V56
()
V57
()
V58
()
V59
()
V60
()
V61
() )
Element
of
NAT
: ( ( ) (
V56
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
K10
(
REAL
: ( ( ) ( non
empty
V56
()
V57
()
V58
()
V62
()
V63
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
TopSpace-like
) (
strict
TopSpace-like
)
TopSpace
)
->
non
empty
strict
TopSpace-like
;
end;
theorem
:: COMPLSP1:1
for
n
being ( ( ) (
V38
()
V39
()
V40
()
V41
()
V44
()
V45
()
V56
()
V57
()
V58
()
V59
()
V60
()
V61
() )
Element
of
NAT
: ( ( ) (
V56
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
K10
(
REAL
: ( ( ) ( non
empty
V56
()
V57
()
V58
()
V62
()
V63
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) holds the
topology
of
(
the_Complex_Space
n
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V44
()
V45
()
V56
()
V57
()
V58
()
V59
()
V60
()
V61
() )
Element
of
NAT
: ( ( ) (
V56
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
K10
(
REAL
: ( ( ) ( non
empty
V56
()
V57
()
V58
()
V62
()
V63
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
TopSpace-like
) ( non
empty
strict
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
(
the_Complex_Space
b
1
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V44
()
V45
()
V56
()
V57
()
V58
()
V59
()
V60
()
V61
() )
Element
of
NAT
: ( ( ) (
V56
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
K10
(
REAL
: ( ( ) ( non
empty
V56
()
V57
()
V58
()
V62
()
V63
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
TopSpace-like
) ( non
empty
strict
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
ComplexOpenSets
n
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V44
()
V45
()
V56
()
V57
()
V58
()
V59
()
V60
()
V61
() )
Element
of
NAT
: ( ( ) (
V56
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
K10
(
REAL
: ( ( ) ( non
empty
V56
()
V57
()
V58
()
V62
()
V63
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( )
Element
of
K10
(
K10
(
(
COMPLEX
b
1
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V44
()
V45
()
V56
()
V57
()
V58
()
V59
()
V60
()
V61
() )
Element
of
NAT
: ( ( ) (
V56
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
K10
(
REAL
: ( ( ) ( non
empty
V56
()
V57
()
V58
()
V62
()
V63
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
)
: ( ( ) ( non
empty
V15
()
V83
() )
M13
(
COMPLEX
: ( ( ) ( non
empty
V56
()
V62
()
V63
() )
set
) )) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: COMPLSP1:2
for
n
being ( ( ) (
V38
()
V39
()
V40
()
V41
()
V44
()
V45
()
V56
()
V57
()
V58
()
V59
()
V60
()
V61
() )
Element
of
NAT
: ( ( ) (
V56
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
K10
(
REAL
: ( ( ) ( non
empty
V56
()
V57
()
V58
()
V62
()
V63
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) holds the
carrier
of
(
the_Complex_Space
n
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V44
()
V45
()
V56
()
V57
()
V58
()
V59
()
V60
()
V61
() )
Element
of
NAT
: ( ( ) (
V56
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
K10
(
REAL
: ( ( ) ( non
empty
V56
()
V57
()
V58
()
V62
()
V63
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
TopSpace-like
) ( non
empty
strict
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
=
COMPLEX
n
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V44
()
V45
()
V56
()
V57
()
V58
()
V59
()
V60
()
V61
() )
Element
of
NAT
: ( ( ) (
V56
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
K10
(
REAL
: ( ( ) ( non
empty
V56
()
V57
()
V58
()
V62
()
V63
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( non
empty
V15
()
V83
() )
M13
(
COMPLEX
: ( ( ) ( non
empty
V56
()
V62
()
V63
() )
set
) )) ;
theorem
:: COMPLSP1:3
for
n
being ( ( ) (
V38
()
V39
()
V40
()
V41
()
V44
()
V45
()
V56
()
V57
()
V58
()
V59
()
V60
()
V61
() )
Element
of
NAT
: ( ( ) (
V56
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
K10
(
REAL
: ( ( ) ( non
empty
V56
()
V57
()
V58
()
V62
()
V63
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
for
p
being ( ( ) ( )
Point
of ( ( ) ( )
set
) ) holds
p
: ( ( ) ( )
Point
of ( ( ) ( )
set
) ) is ( ( ) (
V7
()
V10
(
NAT
: ( ( ) (
V56
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
K10
(
REAL
: ( ( ) ( non
empty
V56
()
V57
()
V58
()
V62
()
V63
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
V11
(
COMPLEX
: ( ( ) ( non
empty
V56
()
V62
()
V63
() )
set
) )
V12
()
V46
()
V81
() )
Element
of
COMPLEX
n
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V44
()
V45
()
V56
()
V57
()
V58
()
V59
()
V60
()
V61
() )
Element
of
NAT
: ( ( ) (
V56
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
K10
(
REAL
: ( ( ) ( non
empty
V56
()
V57
()
V58
()
V62
()
V63
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( non
empty
V15
()
V83
() )
M13
(
COMPLEX
: ( ( ) ( non
empty
V56
()
V62
()
V63
() )
set
) )) ) ;
theorem
:: COMPLSP1:4
for
n
being ( ( ) (
V38
()
V39
()
V40
()
V41
()
V44
()
V45
()
V56
()
V57
()
V58
()
V59
()
V60
()
V61
() )
Element
of
NAT
: ( ( ) (
V56
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
K10
(
REAL
: ( ( ) ( non
empty
V56
()
V57
()
V58
()
V62
()
V63
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
for
V
being ( ( ) ( )
Subset
of )
for
A
being ( ( ) (
V15
() )
Subset
of ( ( ) ( non
empty
)
set
) ) st
A
: ( ( ) (
V15
() )
Subset
of ( ( ) ( non
empty
)
set
) )
=
V
: ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) (
V15
() )
Subset
of ( ( ) ( non
empty
)
set
) ) is
open
iff
V
: ( ( ) ( )
Subset
of ) is
open
) ;
theorem
:: COMPLSP1:5
for
n
being ( ( ) (
V38
()
V39
()
V40
()
V41
()
V44
()
V45
()
V56
()
V57
()
V58
()
V59
()
V60
()
V61
() )
Element
of
NAT
: ( ( ) (
V56
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
K10
(
REAL
: ( ( ) ( non
empty
V56
()
V57
()
V58
()
V62
()
V63
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
for
V
being ( ( ) ( )
Subset
of )
for
A
being ( ( ) (
V15
() )
Subset
of ( ( ) ( non
empty
)
set
) ) st
A
: ( ( ) (
V15
() )
Subset
of ( ( ) ( non
empty
)
set
) )
=
V
: ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) (
V15
() )
Subset
of ( ( ) ( non
empty
)
set
) ) is
closed
iff
V
: ( ( ) ( )
Subset
of ) is
closed
) ;
theorem
:: COMPLSP1:6
for
n
being ( ( ) (
V38
()
V39
()
V40
()
V41
()
V44
()
V45
()
V56
()
V57
()
V58
()
V59
()
V60
()
V61
() )
Element
of
NAT
: ( ( ) (
V56
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
K10
(
REAL
: ( ( ) ( non
empty
V56
()
V57
()
V58
()
V62
()
V63
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) holds
the_Complex_Space
n
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V44
()
V45
()
V56
()
V57
()
V58
()
V59
()
V60
()
V61
() )
Element
of
NAT
: ( ( ) (
V56
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
K10
(
REAL
: ( ( ) ( non
empty
V56
()
V57
()
V58
()
V62
()
V63
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
TopSpace-like
) ( non
empty
strict
TopSpace-like
)
TopSpace
) is
T_2
;
theorem
:: COMPLSP1:7
for
n
being ( ( ) (
V38
()
V39
()
V40
()
V41
()
V44
()
V45
()
V56
()
V57
()
V58
()
V59
()
V60
()
V61
() )
Element
of
NAT
: ( ( ) (
V56
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
K10
(
REAL
: ( ( ) ( non
empty
V56
()
V57
()
V58
()
V62
()
V63
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) holds
the_Complex_Space
n
: ( ( ) (
V38
()
V39
()
V40
()
V41
()
V44
()
V45
()
V56
()
V57
()
V58
()
V59
()
V60
()
V61
() )
Element
of
NAT
: ( ( ) (
V56
()
V57
()
V58
()
V59
()
V60
()
V61
()
V62
() )
Element
of
K10
(
REAL
: ( ( ) ( non
empty
V56
()
V57
()
V58
()
V62
()
V63
() )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
TopSpace-like
) ( non
empty
strict
TopSpace-like
)
TopSpace
) is
regular
;