:: TOPDIM_1 semantic presentation
begin
theorem
:: TOPDIM_1:1
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
B
,
A
being ( ( ) ( )
Subset
of )
for
F
being ( ( ) ( )
Subset
of ) st
F
: ( ( ) ( )
Subset
of )
=
B
: ( ( ) ( )
Subset
of )
/\
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) holds
Fr
F
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
(
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
|
b
3
: ( ( ) ( )
Subset
of )
)
: ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
c=
(
Fr
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
/\
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPDIM_1:2
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) holds
(
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) is
normal
iff for
A
,
B
being ( (
closed
) (
closed
)
Subset
of ) st
A
: ( (
closed
) (
closed
)
Subset
of )
misses
B
: ( (
closed
) (
closed
)
Subset
of ) holds
ex
U
,
W
being ( (
open
) (
open
)
Subset
of ) st
(
A
: ( (
closed
) (
closed
)
Subset
of )
c=
U
: ( (
open
) (
open
)
Subset
of ) &
B
: ( (
closed
) (
closed
)
Subset
of )
c=
W
: ( (
open
) (
open
)
Subset
of ) &
Cl
U
: ( (
open
) (
open
)
Subset
of ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
misses
Cl
W
: ( (
open
) (
open
)
Subset
of ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) ) ;
definition
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
func
Seq_of_ind
T
->
( (
Function-like
quasi_total
) ( non
empty
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
-defined
bool
(
bool
the
carrier
of
T
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
(
bool
the
carrier
of
T
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V14
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
)
SetSequence
of ( ( ) ( non
empty
)
Element
of
bool
(
bool
(
bool
the
carrier
of
T
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) )
means
:: TOPDIM_1:def 1
for
A
being ( ( ) ( )
Subset
of )
for
n
being ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
) holds
(
it
: ( ( ) ( )
set
)
.
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
T
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
{
(
{}
T
: ( ( ) ( )
2-sorted
)
)
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
finite
finite-yielding
V32
()
cardinal
{}
: ( ( ) ( )
set
)
-element
V89
()
V90
()
ext-real
non
positive
non
negative
integer
)
Element
of
bool
the
carrier
of
T
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
finite
V32
() 1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
(
bool
the
carrier
of
T
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) & ( not
A
: ( ( ) ( )
Subset
of )
in
it
: ( ( ) ( )
set
)
.
(
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
)
+
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
T
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) or
A
: ( ( ) ( )
Subset
of )
in
it
: ( ( ) ( )
set
)
.
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
T
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) or for
p
being ( ( ) ( )
Point
of ( ( ) ( )
set
) )
for
U
being ( (
open
) (
open
)
Subset
of ) st
p
: ( ( ) ( )
Point
of ( ( ) ( )
set
) )
in
U
: ( (
open
) (
open
)
Subset
of ) holds
ex
W
being ( (
open
) (
open
)
Subset
of ) st
(
p
: ( ( ) ( )
Point
of ( ( ) ( )
set
) )
in
W
: ( (
open
) (
open
)
Subset
of ) &
W
: ( (
open
) (
open
)
Subset
of )
c=
U
: ( (
open
) (
open
)
Subset
of ) &
Fr
W
: ( (
open
) (
open
)
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
(
T
: ( ( ) ( )
2-sorted
)
|
b
1
: ( ( ) ( )
Subset
of )
)
: ( (
strict
) (
strict
)
SubSpace
of
T
: ( ( ) ( )
2-sorted
) ) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
in
it
: ( ( ) ( )
set
)
.
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
T
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ) & ( (
A
: ( ( ) ( )
Subset
of )
in
it
: ( ( ) ( )
set
)
.
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
T
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) or for
p
being ( ( ) ( )
Point
of ( ( ) ( )
set
) )
for
U
being ( (
open
) (
open
)
Subset
of ) st
p
: ( ( ) ( )
Point
of ( ( ) ( )
set
) )
in
U
: ( (
open
) (
open
)
Subset
of ) holds
ex
W
being ( (
open
) (
open
)
Subset
of ) st
(
p
: ( ( ) ( )
Point
of ( ( ) ( )
set
) )
in
W
: ( (
open
) (
open
)
Subset
of ) &
W
: ( (
open
) (
open
)
Subset
of )
c=
U
: ( (
open
) (
open
)
Subset
of ) &
Fr
W
: ( (
open
) (
open
)
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
(
T
: ( ( ) ( )
2-sorted
)
|
b
1
: ( ( ) ( )
Subset
of )
)
: ( (
strict
) (
strict
)
SubSpace
of
T
: ( ( ) ( )
2-sorted
) ) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
in
it
: ( ( ) ( )
set
)
.
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
T
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ) implies
A
: ( ( ) ( )
Subset
of )
in
it
: ( ( ) ( )
set
)
.
(
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
)
+
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
T
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ) );
end;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
cluster
Seq_of_ind
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( (
Function-like
quasi_total
) ( non
empty
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
-defined
bool
(
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
(
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V14
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
)
SetSequence
of ( ( ) ( non
empty
)
Element
of
bool
(
bool
(
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) )
->
Function-like
quasi_total
non-descending
;
end;
theorem
:: TOPDIM_1:3
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of )
for
n
being ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
)
for
F
being ( ( ) ( )
Subset
of ) st
F
: ( ( ) ( )
Subset
of )
=
B
: ( ( ) ( )
Subset
of ) holds
(
F
: ( ( ) ( )
Subset
of )
in
(
Seq_of_ind
(
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
|
A
: ( ( ) ( )
Subset
of )
)
: ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) )
)
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
-defined
bool
(
bool
the
carrier
of
(
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
|
b
2
: ( ( ) ( )
Subset
of )
)
: ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
(
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
|
b
2
: ( ( ) ( )
Subset
of )
)
: ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
(
bool
the
carrier
of
(
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
|
b
2
: ( ( ) ( )
Subset
of )
)
: ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
(
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
|
b
2
: ( ( ) ( )
Subset
of )
)
: ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V14
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
non-descending
)
SetSequence
of ( ( ) ( non
empty
)
Element
of
bool
(
bool
(
bool
the
carrier
of
(
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
|
b
2
: ( ( ) ( )
Subset
of )
)
: ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
(
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
|
b
2
: ( ( ) ( )
Subset
of )
)
: ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
(
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
|
b
2
: ( ( ) ( )
Subset
of )
)
: ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) iff
B
: ( ( ) ( )
Subset
of )
in
(
Seq_of_ind
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
)
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
-defined
bool
(
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
(
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V14
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
non-descending
)
SetSequence
of ( ( ) ( non
empty
)
Element
of
bool
(
bool
(
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ;
definition
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
attr
A
is
with_finite_small_inductive_dimension
means
:: TOPDIM_1:def 2
ex
n
being ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
) st
A
: ( ( ) ( )
set
)
in
(
Seq_of_ind
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
)
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
-defined
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V14
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
non-descending
)
SetSequence
of ( ( ) ( non
empty
)
Element
of
bool
(
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
end;
notation
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
synonym
finite-ind
A
for
with_finite_small_inductive_dimension
;
end;
definition
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
G
be ( ( ) ( )
Subset-Family
of ) ;
attr
G
is
with_finite_small_inductive_dimension
means
:: TOPDIM_1:def 3
ex
n
being ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
) st
G
: ( ( ) ( )
set
)
c=
(
Seq_of_ind
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
)
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
-defined
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V14
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
non-descending
)
SetSequence
of ( ( ) ( non
empty
)
Element
of
bool
(
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
end;
notation
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
G
be ( ( ) ( )
Subset-Family
of ) ;
synonym
finite-ind
G
for
with_finite_small_inductive_dimension
;
end;
theorem
:: TOPDIM_1:4
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of )
for
G
being ( ( ) ( )
Subset-Family
of ) st
A
: ( ( ) ( )
Subset
of )
in
G
: ( ( ) ( )
Subset-Family
of ) &
G
: ( ( ) ( )
Subset-Family
of ) is
finite-ind
holds
A
: ( ( ) ( )
Subset
of ) is
finite-ind
;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
cluster
finite
->
finite-ind
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
cluster
empty
->
finite-ind
for ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
cluster
non
empty
finite-ind
for ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
end;
registration
let
T
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
cluster
non
empty
finite-ind
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
end;
definition
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
attr
T
is
with_finite_small_inductive_dimension
means
:: TOPDIM_1:def 4
[#]
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
non
proper
open
closed
dense
non
boundary
)
Element
of
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
with_finite_small_inductive_dimension
;
end;
notation
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
synonym
finite-ind
T
for
with_finite_small_inductive_dimension
;
end;
registration
cluster
empty
TopSpace-like
->
TopSpace-like
finite-ind
for ( ( ) ( )
TopStruct
) ;
end;
registration
let
X
be ( ( ) ( )
set
) ;
cluster
1TopSp
X
: ( ( ) ( )
set
) : ( ( ) (
strict
TopSpace-like
)
TopStruct
)
->
finite-ind
;
end;
registration
cluster
non
empty
TopSpace-like
finite-ind
for ( ( ) ( )
TopStruct
) ;
end;
begin
definition
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
assume
A
: ( ( ) ( )
Subset
of ) is
finite-ind
;
func
ind
A
->
( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
means
:: TOPDIM_1:def 5
(
A
: ( ( ) ( )
set
)
in
(
Seq_of_ind
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
)
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
-defined
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V14
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
non-descending
)
SetSequence
of ( ( ) ( non
empty
)
Element
of
bool
(
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.
(
it
: ( ( ) ( )
Element
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) )
+
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( ( ) (
V89
()
V90
()
ext-real
)
Element
of
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) & not
A
: ( ( ) ( )
set
)
in
(
Seq_of_ind
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
)
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
-defined
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V14
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
non-descending
)
SetSequence
of ( ( ) ( non
empty
)
Element
of
bool
(
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.
it
: ( ( ) ( )
Element
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) );
end;
theorem
:: TOPDIM_1:5
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
Af
being ( (
finite-ind
) (
finite-ind
)
Subset
of ) holds
-
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( non
empty
V89
()
V90
()
ext-real
non
positive
negative
integer
)
Element
of
REAL
: ( ( ) ( )
set
) )
<=
ind
Af
: ( (
finite-ind
) (
finite-ind
)
Subset
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) ;
theorem
:: TOPDIM_1:6
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
Af
being ( (
finite-ind
) (
finite-ind
)
Subset
of ) holds
(
ind
Af
: ( (
finite-ind
) (
finite-ind
)
Subset
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
=
-
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( non
empty
V89
()
V90
()
ext-real
non
positive
negative
integer
)
Element
of
REAL
: ( ( ) ( )
set
) ) iff
Af
: ( (
finite-ind
) (
finite-ind
)
Subset
of ) is
empty
) ;
registration
let
T
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( non
empty
finite-ind
) ( non
empty
finite-ind
)
Subset
of ) ;
cluster
ind
A
: ( ( non
empty
finite-ind
) ( non
empty
finite-ind
)
Element
of
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
->
natural
integer
;
end;
theorem
:: TOPDIM_1:7
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
n
being ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
)
for
Af
being ( (
finite-ind
) (
finite-ind
)
Subset
of ) holds
(
ind
Af
: ( (
finite-ind
) (
finite-ind
)
Subset
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
)
-
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) (
V89
()
V90
()
ext-real
integer
)
Element
of
REAL
: ( ( ) ( )
set
) ) iff
Af
: ( (
finite-ind
) (
finite-ind
)
Subset
of )
in
(
Seq_of_ind
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
)
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
-defined
bool
(
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
(
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V14
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
non-descending
)
SetSequence
of ( ( ) ( non
empty
)
Element
of
bool
(
bool
(
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: TOPDIM_1:8
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( (
finite
) (
finite
compact
finite-ind
)
Subset
of ) holds
ind
A
: ( (
finite
) (
finite
compact
finite-ind
)
Subset
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<
card
A
: ( (
finite
) (
finite
compact
finite-ind
)
Subset
of ) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Element
of
omega
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
set
) ) ;
theorem
:: TOPDIM_1:9
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
n
being ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
)
for
Af
being ( (
finite-ind
) (
finite-ind
)
Subset
of ) holds
(
ind
Af
: ( (
finite-ind
) (
finite-ind
)
Subset
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
) iff for
p
being ( ( ) ( )
Point
of ( ( ) ( )
set
) )
for
U
being ( (
open
) (
open
)
Subset
of ) st
p
: ( ( ) ( )
Point
of ( ( ) ( )
set
) )
in
U
: ( (
open
) (
open
)
Subset
of ) holds
ex
W
being ( (
open
) (
open
)
Subset
of ) st
(
p
: ( ( ) ( )
Point
of ( ( ) ( )
set
) )
in
W
: ( (
open
) (
open
)
Subset
of ) &
W
: ( (
open
) (
open
)
Subset
of )
c=
U
: ( (
open
) (
open
)
Subset
of ) &
Fr
W
: ( (
open
) (
open
)
Subset
of ) : ( ( ) (
closed
boundary
nowhere_dense
)
Element
of
bool
the
carrier
of
(
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
|
b
3
: ( (
finite-ind
) (
finite-ind
)
Subset
of )
)
: ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) is
finite-ind
&
ind
(
Fr
W
: ( (
open
) (
open
)
Subset
of )
)
: ( ( ) (
closed
boundary
nowhere_dense
)
Element
of
bool
the
carrier
of
(
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
|
b
3
: ( (
finite-ind
) (
finite-ind
)
Subset
of )
)
: ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
)
-
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) (
V89
()
V90
()
ext-real
integer
)
Element
of
REAL
: ( ( ) ( )
set
) ) ) ) ;
definition
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
G
be ( ( ) ( )
Subset-Family
of ) ;
assume
G
: ( ( ) ( )
Subset-Family
of ) is
finite-ind
;
func
ind
G
->
( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
means
:: TOPDIM_1:def 6
(
G
: ( ( ) ( )
set
)
c=
(
Seq_of_ind
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
)
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
-defined
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V14
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
non-descending
)
SetSequence
of ( ( ) ( non
empty
)
Element
of
bool
(
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.
(
it
: ( ( ) ( )
Element
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) )
+
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( ( ) (
V89
()
V90
()
ext-real
)
Element
of
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) &
-
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( non
empty
V89
()
V90
()
ext-real
non
positive
negative
integer
)
Element
of
REAL
: ( ( ) ( )
set
) )
<=
it
: ( ( ) ( )
Element
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) & ( for
i
being ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) st
-
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( non
empty
V89
()
V90
()
ext-real
non
positive
negative
integer
)
Element
of
REAL
: ( ( ) ( )
set
) )
<=
i
: ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) &
G
: ( ( ) ( )
set
)
c=
(
Seq_of_ind
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
)
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
-defined
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V14
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
non-descending
)
SetSequence
of ( ( ) ( non
empty
)
Element
of
bool
(
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.
(
i
: ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
+
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( ( ) (
V89
()
V90
()
ext-real
integer
)
Element
of
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) holds
it
: ( ( ) ( )
Element
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) )
<=
i
: ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) ) );
end;
theorem
:: TOPDIM_1:10
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
G
being ( ( ) ( )
Subset-Family
of ) holds
( (
ind
G
: ( ( ) ( )
Subset-Family
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
=
-
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( non
empty
V89
()
V90
()
ext-real
non
positive
negative
integer
)
Element
of
REAL
: ( ( ) ( )
set
) ) &
G
: ( ( ) ( )
Subset-Family
of ) is
finite-ind
) iff
G
: ( ( ) ( )
Subset-Family
of )
c=
{
(
{}
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
)
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
finite
finite-yielding
V32
()
cardinal
{}
: ( ( ) ( )
set
)
-element
open
closed
boundary
nowhere_dense
V89
()
V90
()
compact
ext-real
non
positive
non
negative
integer
finite-ind
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
finite
V32
() 1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
(
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: TOPDIM_1:11
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
G
being ( ( ) ( )
Subset-Family
of )
for
I
being ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) holds
(
G
: ( ( ) ( )
Subset-Family
of ) is
finite-ind
&
ind
G
: ( ( ) ( )
Subset-Family
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
I
: ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) iff (
-
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( non
empty
V89
()
V90
()
ext-real
non
positive
negative
integer
)
Element
of
REAL
: ( ( ) ( )
set
) )
<=
I
: ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) & ( for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
in
G
: ( ( ) ( )
Subset-Family
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
finite-ind
&
ind
A
: ( ( ) ( )
Subset
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
I
: ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) ) ) ) ) ;
theorem
:: TOPDIM_1:12
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
G1
,
G2
being ( ( ) ( )
Subset-Family
of ) st
G1
: ( ( ) ( )
Subset-Family
of ) is
finite-ind
&
G2
: ( ( ) ( )
Subset-Family
of )
c=
G1
: ( ( ) ( )
Subset-Family
of ) holds
(
G2
: ( ( ) ( )
Subset-Family
of ) is
finite-ind
&
ind
G2
: ( ( ) ( )
Subset-Family
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
ind
G1
: ( ( ) ( )
Subset-Family
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) ) ;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
G1
,
G2
be ( (
finite-ind
) (
finite-ind
)
Subset-Family
of ) ;
cluster
G1
: ( (
finite-ind
) (
finite-ind
)
Element
of
bool
(
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
\/
G2
: ( (
finite-ind
) (
finite-ind
)
Element
of
bool
(
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
)
->
finite-ind
for ( ( ) ( )
Subset-Family
of ) ;
end;
theorem
:: TOPDIM_1:13
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
G
,
G1
being ( ( ) ( )
Subset-Family
of )
for
I
being ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) st
G
: ( ( ) ( )
Subset-Family
of ) is
finite-ind
&
G1
: ( ( ) ( )
Subset-Family
of ) is
finite-ind
&
ind
G
: ( ( ) ( )
Subset-Family
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
I
: ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) &
ind
G1
: ( ( ) ( )
Subset-Family
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
I
: ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) holds
ind
(
G
: ( ( ) ( )
Subset-Family
of )
\/
G1
: ( ( ) ( )
Subset-Family
of )
)
: ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
I
: ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) ;
definition
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
func
ind
T
->
( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
equals
:: TOPDIM_1:def 7
ind
(
[#]
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( non
empty
non
proper
open
closed
dense
non
boundary
)
Element
of
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) ;
end;
registration
let
T
be ( ( non
empty
TopSpace-like
finite-ind
) ( non
empty
TopSpace-like
finite-ind
)
TopSpace
) ;
cluster
ind
T
: ( ( non
empty
TopSpace-like
finite-ind
) ( non
empty
TopSpace-like
finite-ind
)
TopStruct
) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
->
natural
integer
;
end;
theorem
:: TOPDIM_1:14
for
X
being ( ( non
empty
) ( non
empty
)
set
) holds
ind
(
1TopSp
X
: ( ( non
empty
) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
strict
TopSpace-like
finite-ind
)
TopStruct
) : ( (
integer
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Integer
)
=
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: TOPDIM_1:15
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) st ex
n
being ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
) st
for
p
being ( ( ) ( )
Point
of ( ( ) ( )
set
) )
for
U
being ( (
open
) (
open
)
Subset
of ) st
p
: ( ( ) ( )
Point
of ( ( ) ( )
set
) )
in
U
: ( (
open
) (
open
)
Subset
of ) holds
ex
W
being ( (
open
) (
open
)
Subset
of ) st
(
p
: ( ( ) ( )
Point
of ( ( ) ( )
set
) )
in
W
: ( (
open
) (
open
)
Subset
of ) &
W
: ( (
open
) (
open
)
Subset
of )
c=
U
: ( (
open
) (
open
)
Subset
of ) &
Fr
W
: ( (
open
) (
open
)
Subset
of ) : ( ( ) (
closed
boundary
nowhere_dense
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) is
finite-ind
&
ind
(
Fr
W
: ( (
open
) (
open
)
Subset
of )
)
: ( ( ) (
closed
boundary
nowhere_dense
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
)
-
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) (
V89
()
V90
()
ext-real
integer
)
Element
of
REAL
: ( ( ) ( )
set
) ) ) holds
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) is
finite-ind
;
theorem
:: TOPDIM_1:16
for
n
being ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
)
for
Tf
being ( (
TopSpace-like
finite-ind
) (
TopSpace-like
finite-ind
)
TopSpace
) holds
(
ind
Tf
: ( (
TopSpace-like
finite-ind
) (
TopSpace-like
finite-ind
)
TopSpace
) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
) iff for
p
being ( ( ) ( )
Point
of ( ( ) ( )
set
) )
for
U
being ( (
open
) (
open
)
Subset
of ) st
p
: ( ( ) ( )
Point
of ( ( ) ( )
set
) )
in
U
: ( (
open
) (
open
)
Subset
of ) holds
ex
W
being ( (
open
) (
open
)
Subset
of ) st
(
p
: ( ( ) ( )
Point
of ( ( ) ( )
set
) )
in
W
: ( (
open
) (
open
)
Subset
of ) &
W
: ( (
open
) (
open
)
Subset
of )
c=
U
: ( (
open
) (
open
)
Subset
of ) &
Fr
W
: ( (
open
) (
open
)
Subset
of ) : ( ( ) (
closed
boundary
nowhere_dense
)
Element
of
bool
the
carrier
of
b
2
: ( (
TopSpace-like
finite-ind
) (
TopSpace-like
finite-ind
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) is
finite-ind
&
ind
(
Fr
W
: ( (
open
) (
open
)
Subset
of )
)
: ( ( ) (
closed
boundary
nowhere_dense
)
Element
of
bool
the
carrier
of
b
2
: ( (
TopSpace-like
finite-ind
) (
TopSpace-like
finite-ind
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
)
-
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) (
V89
()
V90
()
ext-real
integer
)
Element
of
REAL
: ( ( ) ( )
set
) ) ) ) ;
begin
registration
let
Tf
be ( (
TopSpace-like
finite-ind
) (
TopSpace-like
finite-ind
)
TopSpace
) ;
cluster
->
finite-ind
for ( ( ) ( )
Element
of
bool
the
carrier
of
Tf
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
end;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
Af
be ( (
finite-ind
) (
finite-ind
)
Subset
of ) ;
cluster
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
|
Af
: ( (
finite-ind
) (
finite-ind
)
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) )
->
strict
finite-ind
;
end;
theorem
:: TOPDIM_1:17
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
Af
being ( (
finite-ind
) (
finite-ind
)
Subset
of ) holds
ind
(
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
|
Af
: ( (
finite-ind
) (
finite-ind
)
Subset
of )
)
: ( (
strict
) (
strict
TopSpace-like
finite-ind
)
SubSpace
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
=
ind
Af
: ( (
finite-ind
) (
finite-ind
)
Subset
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) ;
theorem
:: TOPDIM_1:18
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
|
A
: ( ( ) ( )
Subset
of ) : ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ) is
finite-ind
holds
A
: ( ( ) ( )
Subset
of ) is
finite-ind
;
theorem
:: TOPDIM_1:19
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of )
for
Af
being ( (
finite-ind
) (
finite-ind
)
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
c=
Af
: ( (
finite-ind
) (
finite-ind
)
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
finite-ind
&
ind
A
: ( ( ) ( )
Subset
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
ind
Af
: ( (
finite-ind
) (
finite-ind
)
Subset
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) ) ;
theorem
:: TOPDIM_1:20
for
Tf
being ( (
TopSpace-like
finite-ind
) (
TopSpace-like
finite-ind
)
TopSpace
)
for
A
being ( ( ) (
finite-ind
)
Subset
of ) holds
ind
A
: ( ( ) (
finite-ind
)
Subset
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
ind
Tf
: ( (
TopSpace-like
finite-ind
) (
TopSpace-like
finite-ind
)
TopSpace
) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) ;
theorem
:: TOPDIM_1:21
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of )
for
F
being ( ( ) ( )
Subset
of ) st
F
: ( ( ) (
finite-ind
)
Subset
of )
=
B
: ( ( ) ( )
Subset
of ) &
B
: ( ( ) ( )
Subset
of ) is
finite-ind
holds
(
F
: ( ( ) (
finite-ind
)
Subset
of ) is
finite-ind
&
ind
F
: ( ( ) (
finite-ind
)
Subset
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
=
ind
B
: ( ( ) ( )
Subset
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) ) ;
theorem
:: TOPDIM_1:22
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of )
for
F
being ( ( ) ( )
Subset
of ) st
F
: ( ( ) (
finite-ind
)
Subset
of )
=
B
: ( ( ) ( )
Subset
of ) &
F
: ( ( ) (
finite-ind
)
Subset
of ) is
finite-ind
holds
(
B
: ( ( ) ( )
Subset
of ) is
finite-ind
&
ind
F
: ( ( ) (
finite-ind
)
Subset
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
=
ind
B
: ( ( ) ( )
Subset
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) ) ;
theorem
:: TOPDIM_1:23
for
n
being ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
)
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) st
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
regular
holds
( (
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
finite-ind
&
ind
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
) ) iff for
A
being ( (
closed
) (
closed
)
Subset
of )
for
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st not
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
A
: ( (
closed
) (
closed
)
Subset
of ) holds
ex
L
being ( ( ) ( )
Subset
of ) st
(
L
: ( ( ) ( )
Subset
of )
separates
{
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
finite
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
compact
finite-ind
)
Element
of
bool
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ,
A
: ( (
closed
) (
closed
)
Subset
of ) &
L
: ( ( ) ( )
Subset
of ) is
finite-ind
&
ind
L
: ( ( ) ( )
Subset
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
)
-
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) (
V89
()
V90
()
ext-real
integer
)
Element
of
REAL
: ( ( ) ( )
set
) ) ) ) ;
theorem
:: TOPDIM_1:24
for
T1
,
T2
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) st
T1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ,
T2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
are_homeomorphic
holds
(
T1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) is
finite-ind
iff
T2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) is
finite-ind
) ;
theorem
:: TOPDIM_1:25
for
T1
,
T2
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) st
T1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ,
T2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
are_homeomorphic
&
T1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) is
finite-ind
holds
ind
T1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
=
ind
T2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) ;
theorem
:: TOPDIM_1:26
for
T1
,
T2
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A1
being ( ( ) ( )
Subset
of )
for
A2
being ( ( ) ( )
Subset
of ) st
A1
: ( ( ) ( )
Subset
of ) ,
A2
: ( ( ) ( )
Subset
of )
are_homeomorphic
holds
(
A1
: ( ( ) ( )
Subset
of ) is
finite-ind
iff
A2
: ( ( ) ( )
Subset
of ) is
finite-ind
) ;
theorem
:: TOPDIM_1:27
for
T1
,
T2
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A1
being ( ( ) ( )
Subset
of )
for
A2
being ( ( ) ( )
Subset
of ) st
A1
: ( ( ) ( )
Subset
of ) ,
A2
: ( ( ) ( )
Subset
of )
are_homeomorphic
&
A1
: ( ( ) ( )
Subset
of ) is
finite-ind
holds
ind
A1
: ( ( ) ( )
Subset
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
=
ind
A2
: ( ( ) ( )
Subset
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) ;
theorem
:: TOPDIM_1:28
for
T1
,
T2
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) st
[:
T1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ,
T2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
:]
: ( (
strict
TopSpace-like
) (
strict
TopSpace-like
)
TopStruct
) is
finite-ind
holds
(
[:
T2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ,
T1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
:]
: ( (
strict
TopSpace-like
) (
strict
TopSpace-like
)
TopStruct
) is
finite-ind
&
ind
[:
T1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ,
T2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
:]
: ( (
strict
TopSpace-like
) (
strict
TopSpace-like
)
TopStruct
) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
=
ind
[:
T2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ,
T1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
:]
: ( (
strict
TopSpace-like
) (
strict
TopSpace-like
)
TopStruct
) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) ) ;
theorem
:: TOPDIM_1:29
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of )
for
G
being ( ( ) ( )
Subset-Family
of )
for
Ga
being ( ( ) ( )
Subset-Family
of ) st
Ga
: ( ( ) ( )
Subset-Family
of ) is
finite-ind
&
Ga
: ( ( ) ( )
Subset-Family
of )
=
G
: ( ( ) ( )
Subset-Family
of ) holds
(
G
: ( ( ) ( )
Subset-Family
of ) is
finite-ind
&
ind
G
: ( ( ) ( )
Subset-Family
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
=
ind
Ga
: ( ( ) ( )
Subset-Family
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) ) ;
theorem
:: TOPDIM_1:30
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of )
for
G
being ( ( ) ( )
Subset-Family
of )
for
Ga
being ( ( ) ( )
Subset-Family
of ) st
G
: ( ( ) ( )
Subset-Family
of ) is
finite-ind
&
Ga
: ( ( ) ( )
Subset-Family
of )
=
G
: ( ( ) ( )
Subset-Family
of ) holds
(
Ga
: ( ( ) ( )
Subset-Family
of ) is
finite-ind
&
ind
G
: ( ( ) ( )
Subset-Family
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
=
ind
Ga
: ( ( ) ( )
Subset-Family
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
) ) ;
begin
theorem
:: TOPDIM_1:31
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
n
being ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
) holds
( (
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) is
finite-ind
&
ind
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
) ) iff ex
Bas
being ( (
open
V91
(
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ) ) (
open
V91
(
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ) )
Basis
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ) st
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
in
Bas
: ( (
open
V91
(
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ) ) (
open
V91
(
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ) )
Basis
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ) holds
(
Fr
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) is
finite-ind
&
ind
(
Fr
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
)
-
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) (
V89
()
V90
()
ext-real
integer
)
Element
of
REAL
: ( ( ) ( )
set
) ) ) ) ;
theorem
:: TOPDIM_1:32
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) st
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) is
T_1
& ( for
A
,
B
being ( (
closed
) (
closed
)
Subset
of ) st
A
: ( (
closed
) (
closed
)
Subset
of )
misses
B
: ( (
closed
) (
closed
)
Subset
of ) holds
ex
A9
,
B9
being ( (
closed
) (
closed
)
Subset
of ) st
(
A9
: ( (
closed
) (
closed
)
Subset
of )
misses
B9
: ( (
closed
) (
closed
)
Subset
of ) &
A9
: ( (
closed
) (
closed
)
Subset
of )
\/
B9
: ( (
closed
) (
closed
)
Subset
of ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
=
[#]
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
proper
open
closed
dense
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) &
A
: ( (
closed
) (
closed
)
Subset
of )
c=
A9
: ( (
closed
) (
closed
)
Subset
of ) &
B
: ( (
closed
) (
closed
)
Subset
of )
c=
B9
: ( (
closed
) (
closed
)
Subset
of ) ) ) holds
(
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) is
finite-ind
&
ind
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) ) ;
theorem
:: TOPDIM_1:33
for
X
being ( ( ) ( )
set
)
for
f
being ( (
Function-like
quasi_total
) ( non
empty
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
-defined
bool
b
1
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V14
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
)
SetSequence
of ( ( ) ( non
empty
)
Element
of
bool
(
bool
X
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ex
g
being ( (
Function-like
quasi_total
) ( non
empty
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
-defined
bool
b
1
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V14
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
)
SetSequence
of ( ( ) ( non
empty
)
Element
of
bool
(
bool
X
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ) st
(
union
(
rng
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
-defined
bool
b
1
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V14
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
)
SetSequence
of ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
b
1
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
=
union
(
rng
g
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
-defined
bool
b
1
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V14
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
)
SetSequence
of ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
b
1
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) & ( for
i
,
j
being ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
) st
i
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
)
<>
j
: ( (
finite
) (
finite
)
Subset-Family
of ) holds
g
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
-defined
bool
b
1
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V14
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
)
SetSequence
of ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.
i
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
) : ( ( ) ( )
Element
of
bool
b
1
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) )
misses
g
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
-defined
bool
b
1
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V14
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
)
SetSequence
of ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.
j
: ( (
finite
) (
finite
)
Subset-Family
of ) : ( ( ) ( )
Element
of
bool
b
1
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ) & ( for
n
being ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
) ex
fn
being ( (
finite
) (
finite
)
Subset-Family
of ) st
(
fn
: ( (
finite
) (
finite
)
Subset-Family
of )
=
{
(
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
-defined
bool
b
1
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V14
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
)
SetSequence
of ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.
i
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( ( ) ( )
Element
of
bool
b
1
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ) where
i
is ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) :
i
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
<
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
)
}
&
g
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
-defined
bool
b
1
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V14
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
)
SetSequence
of ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
) : ( ( ) ( )
Element
of
bool
b
1
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) )
=
(
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
-defined
bool
b
1
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V14
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
)
SetSequence
of ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.
n
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Nat
)
)
: ( ( ) ( )
Element
of
bool
b
1
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
Element
of
bool
(
bool
b
1
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) )
\
(
union
fn
: ( (
finite
) (
finite
)
Subset-Family
of )
)
: ( ( ) ( )
Element
of
bool
b
1
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
b
1
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) ) ) ;
theorem
:: TOPDIM_1:34
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) st
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) is
finite-ind
&
ind
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) &
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) is
Lindelof
holds
for
A
,
B
being ( (
closed
) (
closed
)
Subset
of ) st
A
: ( (
closed
) (
closed
)
Subset
of )
misses
B
: ( (
closed
) (
closed
)
Subset
of ) holds
ex
A9
,
B9
being ( (
closed
) (
closed
)
Subset
of ) st
(
A9
: ( (
closed
) (
closed
)
Subset
of )
misses
B9
: ( (
closed
) (
closed
)
Subset
of ) &
A9
: ( (
closed
) (
closed
)
Subset
of )
\/
B9
: ( (
closed
) (
closed
)
Subset
of ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
=
[#]
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
proper
open
closed
dense
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) &
A
: ( (
closed
) (
closed
)
Subset
of )
c=
A9
: ( (
closed
) (
closed
)
Subset
of ) &
B
: ( (
closed
) (
closed
)
Subset
of )
c=
B9
: ( (
closed
) (
closed
)
Subset
of ) ) ;
theorem
:: TOPDIM_1:35
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) st
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) is
T_1
&
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) is
Lindelof
holds
( (
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) is
finite-ind
&
ind
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) ) iff for
A
,
B
being ( (
closed
) (
closed
)
Subset
of ) st
A
: ( (
closed
) (
closed
)
Subset
of )
misses
B
: ( (
closed
) (
closed
)
Subset
of ) holds
{}
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) (
empty
Relation-like
non-empty
empty-yielding
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
finite
finite-yielding
V32
()
cardinal
{}
: ( ( ) ( )
set
)
-element
open
closed
boundary
nowhere_dense
V89
()
V90
()
compact
ext-real
non
positive
non
negative
integer
finite-ind
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
separates
A
: ( (
closed
) (
closed
)
Subset
of ) ,
B
: ( (
closed
) (
closed
)
Subset
of ) ) ;
theorem
:: TOPDIM_1:36
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) st
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) is
T_4
&
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) is
Lindelof
& ex
F
being ( ( ) ( )
Subset-Family
of ) st
(
F
: ( ( ) ( )
Subset-Family
of ) is
closed
&
F
: ( ( ) ( )
Subset-Family
of ) is ( ( ) ( )
Cover
of ( ( ) ( )
set
) ) &
F
: ( ( ) ( )
Subset-Family
of ) is
countable
&
F
: ( ( ) ( )
Subset-Family
of ) is
finite-ind
&
ind
F
: ( ( ) ( )
Subset-Family
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) ) holds
(
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) is
finite-ind
&
ind
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) ) ;
theorem
:: TOPDIM_1:37
for
TM
being ( (
TopSpace-like
metrizable
) (
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
TopSpace
)
for
A
,
B
being ( (
closed
) (
closed
)
Subset
of ) st
A
: ( (
closed
) (
closed
)
Subset
of )
misses
B
: ( (
closed
) (
closed
)
Subset
of ) holds
for
Null
being ( (
finite-ind
) (
finite-ind
)
Subset
of ) st
ind
Null
: ( (
finite-ind
) (
finite-ind
)
Subset
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) &
TM
: ( (
TopSpace-like
metrizable
) (
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
TopSpace
)
|
Null
: ( (
finite-ind
) (
finite-ind
)
Subset
of ) : ( (
strict
) (
strict
TopSpace-like
T_0
T_1
normal
T_4
metrizable
finite-ind
)
SubSpace
of
b
1
: ( (
TopSpace-like
metrizable
) (
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
TopSpace
) ) is
second-countable
holds
ex
L
being ( ( ) ( )
Subset
of ) st
(
L
: ( ( ) ( )
Subset
of )
separates
A
: ( (
closed
) (
closed
)
Subset
of ) ,
B
: ( (
closed
) (
closed
)
Subset
of ) &
L
: ( ( ) ( )
Subset
of )
misses
Null
: ( (
finite-ind
) (
finite-ind
)
Subset
of ) ) ;
theorem
:: TOPDIM_1:38
for
TM
being ( (
TopSpace-like
metrizable
) (
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
TopSpace
)
for
Null
being ( ( ) ( )
Subset
of ) st
TM
: ( (
TopSpace-like
metrizable
) (
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
TopSpace
)
|
Null
: ( ( ) ( )
Subset
of ) : ( (
strict
) (
strict
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
SubSpace
of
b
1
: ( (
TopSpace-like
metrizable
) (
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
TopSpace
) ) is
second-countable
holds
( (
Null
: ( ( ) ( )
Subset
of ) is
finite-ind
&
ind
Null
: ( ( ) ( )
Subset
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) ) iff for
p
being ( ( ) ( )
Point
of ( ( ) ( )
set
) )
for
U
being ( (
open
) (
open
)
Subset
of ) st
p
: ( ( ) ( )
Point
of ( ( ) ( )
set
) )
in
U
: ( (
open
) (
open
)
Subset
of ) holds
ex
W
being ( (
open
) (
open
)
Subset
of ) st
(
p
: ( ( ) ( )
Point
of ( ( ) ( )
set
) )
in
W
: ( (
open
) (
open
)
Subset
of ) &
W
: ( (
open
) (
open
)
Subset
of )
c=
U
: ( (
open
) (
open
)
Subset
of ) &
Null
: ( ( ) ( )
Subset
of )
misses
Fr
W
: ( (
open
) (
open
)
Subset
of ) : ( ( ) (
closed
boundary
nowhere_dense
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
metrizable
) (
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) ) ;
theorem
:: TOPDIM_1:39
for
TM
being ( (
TopSpace-like
metrizable
) (
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
TopSpace
)
for
Null
being ( ( ) ( )
Subset
of ) st
TM
: ( (
TopSpace-like
metrizable
) (
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
TopSpace
)
|
Null
: ( ( ) ( )
Subset
of ) : ( (
strict
) (
strict
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
SubSpace
of
b
1
: ( (
TopSpace-like
metrizable
) (
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
TopSpace
) ) is
second-countable
holds
( (
Null
: ( ( ) ( )
Subset
of ) is
finite-ind
&
ind
Null
: ( ( ) ( )
Subset
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) ) iff ex
B
being ( (
open
V91
(
b
1
: ( (
TopSpace-like
metrizable
) (
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
TopSpace
) ) ) (
open
V91
(
b
1
: ( (
TopSpace-like
metrizable
) (
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
TopSpace
) ) )
Basis
of
TM
: ( (
TopSpace-like
metrizable
) (
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
TopSpace
) ) st
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
in
B
: ( (
open
V91
(
b
1
: ( (
TopSpace-like
metrizable
) (
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
TopSpace
) ) ) (
open
V91
(
b
1
: ( (
TopSpace-like
metrizable
) (
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
TopSpace
) ) )
Basis
of
b
1
: ( (
TopSpace-like
metrizable
) (
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
TopSpace
) ) holds
Null
: ( ( ) ( )
Subset
of )
misses
Fr
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
metrizable
) (
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: TOPDIM_1:40
for
TM
being ( (
TopSpace-like
metrizable
) (
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
TopSpace
)
for
Null
,
A
being ( ( ) ( )
Subset
of ) st
TM
: ( (
TopSpace-like
metrizable
) (
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
TopSpace
)
|
Null
: ( ( ) ( )
Subset
of ) : ( (
strict
) (
strict
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
SubSpace
of
b
1
: ( (
TopSpace-like
metrizable
) (
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
TopSpace
) ) is
second-countable
&
Null
: ( ( ) ( )
Subset
of ) is
finite-ind
&
A
: ( ( ) ( )
Subset
of ) is
finite-ind
&
ind
Null
: ( ( ) ( )
Subset
of ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) holds
(
A
: ( ( ) ( )
Subset
of )
\/
Null
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
metrizable
) (
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) is
finite-ind
&
ind
(
A
: ( ( ) ( )
Subset
of )
\/
Null
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
metrizable
) (
TopSpace-like
T_0
T_1
normal
T_4
metrizable
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
<=
(
ind
A
: ( ( ) ( )
Subset
of )
)
: ( (
integer
) (
V89
()
V90
()
ext-real
integer
)
Integer
)
+
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
finite
cardinal
V89
()
V90
()
ext-real
positive
non
negative
integer
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) (
V89
()
V90
()
ext-real
integer
)
Element
of
REAL
: ( ( ) ( )
set
) ) ) ;