:: Topology from Neighbourhoods
:: by Roland Coghetto
::
:: Received August 14, 2015
:: Copyright (c) 2015 Association of Mizar Users
definition
let
ETV
be non
empty
strict
FMT_Space_Str
;
attr
ETV
is
PP0
means
:
def01
:
:: FINTOPO7:def 1
for
x
being
Element
of
ETV
holds
U_FMT
x
is
Filter
of the
carrier
of
ETV
;
attr
ETV
is
PP1
means
:
def02
:
:: FINTOPO7:def 2
for
x
being
Element
of
ETV
for
V
being
Element
of
U_FMT
x
holds
x
in
V
;
attr
ETV
is
PP2
means
:
def03
:
:: FINTOPO7:def 3
for
x
being
Element
of
ETV
for
V
being
Element
of
U_FMT
x
ex
W
being
Element
of
U_FMT
x
st
for
y
being
Element
of
ETV
st
y
is
Element
of
W
holds
V
is
Element
of
U_FMT
y
;
end;
::
deftheorem
def01
defines
PP0
FINTOPO7:def 1 :
for
ETV
being non
empty
strict
FMT_Space_Str
holds
(
ETV
is
PP0
iff for
x
being
Element
of
ETV
holds
U_FMT
x
is
Filter
of the
carrier
of
ETV
);
::
deftheorem
def02
defines
PP1
FINTOPO7:def 2 :
for
ETV
being non
empty
strict
FMT_Space_Str
holds
(
ETV
is
PP1
iff for
x
being
Element
of
ETV
for
V
being
Element
of
U_FMT
x
holds
x
in
V
);
::
deftheorem
def03
defines
PP2
FINTOPO7:def 3 :
for
ETV
being non
empty
strict
FMT_Space_Str
holds
(
ETV
is
PP2
iff for
x
being
Element
of
ETV
for
V
being
Element
of
U_FMT
x
ex
W
being
Element
of
U_FMT
x
st
for
y
being
Element
of
ETV
st
y
is
Element
of
W
holds
V
is
Element
of
U_FMT
y
);
registration
cluster
non
empty
strict
PP0
PP1
PP2
for
FMT_Space_Str
;
existence
ex
b
1
being non
empty
strict
FMT_Space_Str
st
(
b
1
is
PP2
&
b
1
is
PP1
&
b
1
is
PP0
)
proof
end;
end;
definition
mode
FMT_TopSpace
is
non
empty
strict
PP0
PP1
PP2
FMT_Space_Str
;
end;
definition
let
ETV
be non
empty
strict
FMT_Space_Str
;
let
O
be
Subset
of
ETV
;
attr
O
is
open
means
:
def04
:
:: FINTOPO7:def 4
for
x
being
Element
of
ETV
st
x
in
O
holds
O
in
U_FMT
x
;
end;
::
deftheorem
def04
defines
open
FINTOPO7:def 4 :
for
ETV
being non
empty
strict
FMT_Space_Str
for
O
being
Subset
of
ETV
holds
(
O
is
open
iff for
x
being
Element
of
ETV
st
x
in
O
holds
O
in
U_FMT
x
);
registration
let
ETV
be
FMT_TopSpace
;
cluster
open
for
Element
of
K10
( the
carrier
of
ETV
);
existence
ex
b
1
being
Subset
of
ETV
st
b
1
is
open
proof
end;
end;
definition
let
ETV
be
FMT_TopSpace
;
func
OOpen
ETV
->
non
empty
Subset-Family
of the
carrier
of
ETV
equals
:: FINTOPO7:def 5
{
O
where
O
is
open
Subset
of
ETV
: verum
}
;
correctness
coherence
{
O
where
O
is
open
Subset
of
ETV
: verum
}
is non
empty
Subset-Family
of the
carrier
of
ETV
;
proof
end;
end;
::
deftheorem
defines
OOpen
FINTOPO7:def 5 :
for
ETV
being
FMT_TopSpace
holds
OOpen
ETV
=
{
O
where
O
is
open
Subset
of
ETV
: verum
}
;
theorem
Th01
:
:: FINTOPO7:1
for
ETV
being
FMT_TopSpace
holds
(
{}
in
OOpen
ETV
& the
carrier
of
ETV
in
OOpen
ETV
& ( for
a
being
Subset-Family
of
ETV
st
a
c=
OOpen
ETV
holds
union
a
in
OOpen
ETV
) & ( for
a
,
b
being
Subset
of
ETV
st
a
in
OOpen
ETV
&
b
in
OOpen
ETV
holds
a
/\
b
in
OOpen
ETV
) )
proof
end;
theorem
Th02
:
:: FINTOPO7:2
for
ETV
being non
empty
strict
PP0
FMT_Space_Str
for
x
being
Element
of
ETV
holds the
carrier
of
ETV
in
U_FMT
x
proof
end;
definition
let
ETV
be non
empty
strict
PP0
FMT_Space_Str
;
let
x
be
Element
of
ETV
;
mode
a_neighborhood
of
x
->
Subset
of
ETV
means
:
def06
:
:: FINTOPO7:def 6
it
in
U_FMT
x
;
existence
ex
b
1
being
Subset
of
ETV
st
b
1
in
U_FMT
x
proof
end;
end;
::
deftheorem
def06
defines
a_neighborhood
FINTOPO7:def 6 :
for
ETV
being non
empty
strict
PP0
FMT_Space_Str
for
x
being
Element
of
ETV
for
b
3
being
Subset
of
ETV
holds
(
b
3
is
a_neighborhood
of
x
iff
b
3
in
U_FMT
x
);
registration
let
ETV
be non
empty
strict
PP0
FMT_Space_Str
;
let
x
be
Element
of
ETV
;
cluster
open
for
a_neighborhood
of
x
;
existence
ex
b
1
being
a_neighborhood
of
x
st
b
1
is
open
proof
end;
end;
definition
let
ETV
be non
empty
strict
PP0
FMT_Space_Str
;
let
A
be
Subset
of
ETV
;
mode
a_neighborhood
of
A
->
Subset
of
ETV
means
:
def07
:
:: FINTOPO7:def 7
for
x
being
Element
of
ETV
st
x
in
A
holds
it
in
U_FMT
x
;
existence
ex
b
1
being
Subset
of
ETV
st
for
x
being
Element
of
ETV
st
x
in
A
holds
b
1
in
U_FMT
x
proof
end;
end;
::
deftheorem
def07
defines
a_neighborhood
FINTOPO7:def 7 :
for
ETV
being non
empty
strict
PP0
FMT_Space_Str
for
A
,
b
3
being
Subset
of
ETV
holds
(
b
3
is
a_neighborhood
of
A
iff for
x
being
Element
of
ETV
st
x
in
A
holds
b
3
in
U_FMT
x
);
registration
let
ETV
be non
empty
strict
PP0
FMT_Space_Str
;
let
A
be
Subset
of
ETV
;
cluster
open
for
a_neighborhood
of
A
;
existence
ex
b
1
being
a_neighborhood
of
A
st
b
1
is
open
proof
end;
end;
theorem
Th03
:
:: FINTOPO7:3
for
ETV
being non
empty
strict
PP0
FMT_Space_Str
for
A
being
Subset
of
ETV
for
NA
being
a_neighborhood
of
A
for
B
being
Subset
of
ETV
st
NA
c=
B
holds
B
is
a_neighborhood
of
A
proof
end;
definition
let
ETV
be non
empty
strict
PP0
FMT_Space_Str
;
let
A
be
Subset
of
ETV
;
func
Neighborhood
A
->
Subset-Family
of
ETV
equals
:: FINTOPO7:def 8
{
N
where
N
is
a_neighborhood
of
A
: verum
}
;
correctness
coherence
{
N
where
N
is
a_neighborhood
of
A
: verum
}
is
Subset-Family
of
ETV
;
proof
end;
end;
::
deftheorem
defines
Neighborhood
FINTOPO7:def 8 :
for
ETV
being non
empty
strict
PP0
FMT_Space_Str
for
A
being
Subset
of
ETV
holds
Neighborhood
A
=
{
N
where
N
is
a_neighborhood
of
A
: verum
}
;
theorem
:: FINTOPO7:4
for
ETV
being non
empty
strict
PP0
FMT_Space_Str
for
A
being non
empty
Subset
of
ETV
holds
{
F
where
F
is
a_neighborhood
of
A
: verum
}
is
Filter
of the
carrier
of
ETV
proof
end;
theorem
Th04
:
:: FINTOPO7:5
for
ETV
being non
empty
strict
FMT_Space_Str
st
ETV
is
PP0
holds
for
x
being
Element
of
ETV
holds not
U_FMT
x
is
empty
;
theorem
Th05
:
:: FINTOPO7:6
for
ETV
being
FMT_TopSpace
for
a
being
Element
of
ETV
for
V
being
a_neighborhood
of
a
ex
O
being
open
Subset
of
ETV
st
(
a
in
O
&
O
c=
V
)
proof
end;
theorem
Th06
:
:: FINTOPO7:7
for
ETV
being
FMT_TopSpace
for
A
being non
empty
Subset
of
ETV
for
V
being
Subset
of
ETV
holds
(
V
is
a_neighborhood
of
A
iff ex
O
being
open
Subset
of
ETV
st
(
A
c=
O
&
O
c=
V
) )
proof
end;
theorem
:: FINTOPO7:8
for
ETV
being
FMT_TopSpace
for
A
being non
empty
Subset
of
ETV
holds
Neighborhood
A
is
Filter
of the
carrier
of
ETV
proof
end;
definition
let
ETV
be
FMT_TopSpace
;
let
A
be non
empty
Subset
of
ETV
;
func
OpenNeighborhoods
A
->
Subset-Family
of the
carrier
of
ETV
equals
:: FINTOPO7:def 9
{
N
where
N
is
open
a_neighborhood
of
A
: verum
}
;
correctness
coherence
{
N
where
N
is
open
a_neighborhood
of
A
: verum
}
is
Subset-Family
of the
carrier
of
ETV
;
proof
end;
end;
::
deftheorem
defines
OpenNeighborhoods
FINTOPO7:def 9 :
for
ETV
being
FMT_TopSpace
for
A
being non
empty
Subset
of
ETV
holds
OpenNeighborhoods
A
=
{
N
where
N
is
open
a_neighborhood
of
A
: verum
}
;
theorem
:: FINTOPO7:9
for
ETV
being
FMT_TopSpace
for
F
being
Filter
of the
carrier
of
ETV
for
S
being non
empty
Subset
of
F
for
A
being non
empty
Subset
of
ETV
st
F
=
Neighborhood
A
&
S
=
OpenNeighborhoods
A
holds
S
is
filter_basis
proof
end;
definition
let
ETV
be non
empty
strict
FMT_Space_Str
;
attr
ETV
is
PP3
means
:: FINTOPO7:def 10
for
x
being
Element
of the
carrier
of
ETV
holds
U_FMT
x
is
filter_base
of the
carrier
of
ETV
;
end;
::
deftheorem
defines
PP3
FINTOPO7:def 10 :
for
ETV
being non
empty
strict
FMT_Space_Str
holds
(
ETV
is
PP3
iff for
x
being
Element
of the
carrier
of
ETV
holds
U_FMT
x
is
filter_base
of the
carrier
of
ETV
);
definition
let
ETV
be non
empty
FMT_Space_Str
;
func
<.
ETV
.]
->
Function
of the
carrier
of
ETV
,
(
bool
(
bool
the
carrier
of
ETV
)
)
means
:
def08
:
:: FINTOPO7:def 11
for
x
being
Element
of the
carrier
of
ETV
holds
it
.
x
=
<.
(
U_FMT
x
)
.]
;
existence
ex
b
1
being
Function
of the
carrier
of
ETV
,
(
bool
(
bool
the
carrier
of
ETV
)
)
st
for
x
being
Element
of the
carrier
of
ETV
holds
b
1
.
x
=
<.
(
U_FMT
x
)
.]
proof
end;
uniqueness
for
b
1
,
b
2
being
Function
of the
carrier
of
ETV
,
(
bool
(
bool
the
carrier
of
ETV
)
)
st ( for
x
being
Element
of the
carrier
of
ETV
holds
b
1
.
x
=
<.
(
U_FMT
x
)
.]
) & ( for
x
being
Element
of the
carrier
of
ETV
holds
b
2
.
x
=
<.
(
U_FMT
x
)
.]
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
def08
defines
<.
FINTOPO7:def 11 :
for
ETV
being non
empty
FMT_Space_Str
for
b
2
being
Function
of the
carrier
of
ETV
,
(
bool
(
bool
the
carrier
of
ETV
)
)
holds
(
b
2
=
<.
ETV
.]
iff for
x
being
Element
of the
carrier
of
ETV
holds
b
2
.
x
=
<.
(
U_FMT
x
)
.]
);
definition
let
ETV
be non
empty
strict
FMT_Space_Str
;
func
gen_top
ETV
->
non
empty
strict
FMT_Space_Str
equals
:: FINTOPO7:def 12
FMT_Space_Str
(# the
carrier
of
ETV
,
<.
ETV
.]
#);
correctness
coherence
FMT_Space_Str
(# the
carrier
of
ETV
,
<.
ETV
.]
#) is non
empty
strict
FMT_Space_Str
;
;
end;
::
deftheorem
defines
gen_top
FINTOPO7:def 12 :
for
ETV
being non
empty
strict
FMT_Space_Str
holds
gen_top
ETV
=
FMT_Space_Str
(# the
carrier
of
ETV
,
<.
ETV
.]
#);
theorem
Th07
:
:: FINTOPO7:10
for
ETV
being non
empty
strict
FMT_Space_Str
st
ETV
is
PP3
holds
gen_top
ETV
is
PP0
proof
end;
theorem
Th08
:
:: FINTOPO7:11
for
T
being non
empty
TopSpace
ex
ETV
being
FMT_TopSpace
st
( the
carrier
of
T
=
the
carrier
of
ETV
&
OOpen
ETV
=
the
topology
of
T
)
proof
end;
theorem
Th09
:
:: FINTOPO7:12
for
T
being non
empty
TopSpace
for
ETV
being
FMT_TopSpace
st the
carrier
of
T
=
the
carrier
of
ETV
&
OOpen
ETV
=
the
topology
of
T
holds
for
x
being
Element
of
ETV
holds
U_FMT
x
=
{
V
where
V
is
Subset
of
ETV
: ex
O
being
Subset
of
T
st
(
O
in
the
topology
of
T
&
x
in
O
&
O
c=
V
)
}
proof
end;
definition
let
X
be
FMT_TopSpace
;
let
F
be
Subset-Family
of
X
;
attr
F
is
quasi_basis
means
:
def10
:
:: FINTOPO7:def 13
OOpen
X
c=
UniCl
F
;
end;
::
deftheorem
def10
defines
quasi_basis
FINTOPO7:def 13 :
for
X
being
FMT_TopSpace
for
F
being
Subset-Family
of
X
holds
(
F
is
quasi_basis
iff
OOpen
X
c=
UniCl
F
);
registration
let
X
be
FMT_TopSpace
;
cluster
OOpen
X
->
non
empty
quasi_basis
;
coherence
OOpen
X
is
quasi_basis
proof
end;
end;
registration
let
X
be
FMT_TopSpace
;
cluster
quasi_basis
for
Element
of
K10
(
K10
( the
carrier
of
X
));
existence
ex
b
1
being
Subset-Family
of
X
st
b
1
is
quasi_basis
proof
end;
end;
definition
let
X
be
FMT_TopSpace
;
let
S
be
Subset-Family
of
X
;
attr
S
is
open
means
:: FINTOPO7:def 14
S
c=
OOpen
X
;
end;
::
deftheorem
defines
open
FINTOPO7:def 14 :
for
X
being
FMT_TopSpace
for
S
being
Subset-Family
of
X
holds
(
S
is
open
iff
S
c=
OOpen
X
);
registration
let
X
be
FMT_TopSpace
;
cluster
open
for
Element
of
K10
(
K10
( the
carrier
of
X
));
existence
ex
b
1
being
Subset-Family
of
X
st
b
1
is
open
proof
end;
end;
registration
let
X
be
FMT_TopSpace
;
cluster
quasi_basis
open
for
Element
of
K10
(
K10
( the
carrier
of
X
));
existence
ex
b
1
being
Subset-Family
of
X
st
(
b
1
is
open
&
b
1
is
quasi_basis
)
proof
end;
end;
definition
let
X
be
FMT_TopSpace
;
mode
Basis of
X
is
quasi_basis
open
Subset-Family
of
X
;
end;
theorem
:: FINTOPO7:13
for
X
being
FMT_TopSpace
for
B
being
Basis
of
X
holds
OOpen
X
=
UniCl
B
proof
end;
theorem
:: FINTOPO7:14
for
X
being non
empty
set
for
B
,
Y
being
Subset-Family
of
X
st
Y
c=
UniCl
B
holds
union
Y
in
UniCl
B
proof
end;
theorem
Th10
:
:: FINTOPO7:15
for
X
being non
empty
set
for
B
being
empty
Subset-Family
of
X
st ( for
B1
,
B2
being
Element
of
B
ex
BB
being
Subset
of
B
st
B1
/\
B2
=
union
BB
) &
X
=
union
B
holds
FinMeetCl
B
c=
UniCl
B
proof
end;
theorem
Th11
:
:: FINTOPO7:16
for
X
being non
empty
set
for
B
being non
empty
Subset-Family
of
X
st ( for
B1
,
B2
being
Element
of
B
ex
BB
being
Subset
of
B
st
B1
/\
B2
=
union
BB
) &
X
=
union
B
holds
FinMeetCl
B
c=
UniCl
B
proof
end;
theorem
Th12
:
:: FINTOPO7:17
for
X
being non
empty
set
for
B
being
Subset-Family
of
X
st ( for
B1
,
B2
being
Element
of
B
ex
BB
being
Subset
of
B
st
B1
/\
B2
=
union
BB
) &
X
=
union
B
holds
(
UniCl
B
=
UniCl
(
FinMeetCl
B
)
&
TopStruct
(#
X
,
(
UniCl
B
)
#) is
TopSpace-like
)
proof
end;
theorem
:: FINTOPO7:18
for
X
being non
empty
set
for
B
being non
empty
Subset-Family
of
X
st ( for
B1
,
B2
being
Element
of
B
ex
BB
being
Subset
of
B
st
B1
/\
B2
=
union
BB
) &
X
=
union
B
holds
ex
TV
being
FMT_TopSpace
st
( the
carrier
of
TV
=
X
&
B
is
Basis
of
TV
)
proof
end;
theorem
:: FINTOPO7:19
for
X
being
FMT_TopSpace
for
B
being
Basis
of
X
holds
( ( for
B1
,
B2
being
Element
of
B
ex
BB
being
Subset
of
B
st
B1
/\
B2
=
union
BB
) & the
carrier
of
X
=
union
B
)
proof
end;
definition
let
T
be non
empty
TopSpace
;
func
TopSpace2FMT
T
->
FMT_TopSpace
means
:
def11
:
:: FINTOPO7:def 15
( the
carrier
of
it
=
the
carrier
of
T
&
OOpen
it
=
the
topology
of
T
);
existence
ex
b
1
being
FMT_TopSpace
st
( the
carrier
of
b
1
=
the
carrier
of
T
&
OOpen
b
1
=
the
topology
of
T
)
by
Th08
;
uniqueness
for
b
1
,
b
2
being
FMT_TopSpace
st the
carrier
of
b
1
=
the
carrier
of
T
&
OOpen
b
1
=
the
topology
of
T
& the
carrier
of
b
2
=
the
carrier
of
T
&
OOpen
b
2
=
the
topology
of
T
holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
def11
defines
TopSpace2FMT
FINTOPO7:def 15 :
for
T
being non
empty
TopSpace
for
b
2
being
FMT_TopSpace
holds
(
b
2
=
TopSpace2FMT
T
iff ( the
carrier
of
b
2
=
the
carrier
of
T
&
OOpen
b
2
=
the
topology
of
T
) );
definition
let
ETV
be
FMT_TopSpace
;
func
FMT2TopSpace
ETV
->
strict
TopSpace
means
:
def12
:
:: FINTOPO7:def 16
( the
carrier
of
it
=
the
carrier
of
ETV
&
OOpen
ETV
=
the
topology
of
it
);
existence
ex
b
1
being
strict
TopSpace
st
( the
carrier
of
b
1
=
the
carrier
of
ETV
&
OOpen
ETV
=
the
topology
of
b
1
)
proof
end;
uniqueness
for
b
1
,
b
2
being
strict
TopSpace
st the
carrier
of
b
1
=
the
carrier
of
ETV
&
OOpen
ETV
=
the
topology
of
b
1
& the
carrier
of
b
2
=
the
carrier
of
ETV
&
OOpen
ETV
=
the
topology
of
b
2
holds
b
1
=
b
2
;
end;
::
deftheorem
def12
defines
FMT2TopSpace
FINTOPO7:def 16 :
for
ETV
being
FMT_TopSpace
for
b
2
being
strict
TopSpace
holds
(
b
2
=
FMT2TopSpace
ETV
iff ( the
carrier
of
b
2
=
the
carrier
of
ETV
&
OOpen
ETV
=
the
topology
of
b
2
) );
registration
let
ETV
be
FMT_TopSpace
;
cluster
FMT2TopSpace
ETV
->
non
empty
strict
;
coherence
not
FMT2TopSpace
ETV
is
empty
by
def12
;
end;
theorem
:: FINTOPO7:20
for
T
being non
empty
strict
TopSpace
holds
T
=
FMT2TopSpace
(
TopSpace2FMT
T
)
proof
end;
theorem
:: FINTOPO7:21
for
ETV
being
FMT_TopSpace
holds
ETV
=
TopSpace2FMT
(
FMT2TopSpace
ETV
)
proof
end;
theorem
:: FINTOPO7:22
for
T
being non
empty
TopStruct
holds
NeighSp
T
is non
empty
FMT_Space_Str
;
theorem
Th13
:
:: FINTOPO7:23
for
X
being non
empty
set
for
F
being non
empty
Subset
of
(
BooleLatt
X
)
holds
(
F
is
Filter
of
(
BooleLatt
X
)
iff ( ( for
p
,
q
being
Element
of
F
holds
p
/\
q
in
F
) & ( for
p
being
Element
of
F
for
q
being
Element
of
(
BooleLatt
X
)
st
p
c=
q
holds
q
in
F
) ) )
proof
end;
theorem
Th14
:
:: FINTOPO7:24
for
X
being non
empty
set
for
F
being non
empty
Subset
of
(
BooleLatt
X
)
holds
(
F
is
Filter
of
(
BooleLatt
X
)
iff for
Y1
,
Y2
being
Subset
of
X
holds
( (
Y1
in
F
&
Y2
in
F
implies
Y1
/\
Y2
in
F
) & (
Y1
in
F
&
Y1
c=
Y2
implies
Y2
in
F
) ) )
proof
end;
theorem
Th15
:
:: FINTOPO7:25
for
X
being non
empty
set
for
FF
being non
empty
Subset-Family
of
X
st
FF
is
Filter
of
(
BooleLatt
X
)
holds
FF
is
Filter
of
(
BoolePoset
X
)
proof
end;
theorem
Th16
:
:: FINTOPO7:26
for
X
being non
empty
set
for
F
being
Filter
of
(
BoolePoset
X
)
holds
F
is
Filter
of
(
BooleLatt
X
)
proof
end;
theorem
Th17
:
:: FINTOPO7:27
for
X
being non
empty
set
for
F
being non
empty
Subset
of
(
BooleLatt
X
)
holds
( (
F
is
with_non-empty_elements
&
F
is
Filter
of
(
BooleLatt
X
)
) iff
F
is
Filter
of
X
)
proof
end;
theorem
Th18
:
:: FINTOPO7:28
for
X
being non
empty
set
for
F
being
proper
Filter
of
(
BoolePoset
X
)
holds
F
is
Filter
of
X
proof
end;
theorem
:: FINTOPO7:29
for
T
being non
empty
TopSpace
for
x
being
Point
of
T
holds
NeighborhoodSystem
x
is
Filter
of the
carrier
of
T
by
Th18
;
definition
let
T
be non
empty
TopSpace
;
let
F
be
proper
Filter
of
(
BoolePoset
(
[#]
T
)
)
;
func
BOOL2F
F
->
Filter
of the
carrier
of
T
equals
:: FINTOPO7:def 17
F
;
coherence
F
is
Filter
of the
carrier
of
T
by
Th18
;
end;
::
deftheorem
defines
BOOL2F
FINTOPO7:def 17 :
for
T
being non
empty
TopSpace
for
F
being
proper
Filter
of
(
BoolePoset
(
[#]
T
)
)
holds
BOOL2F
F
=
F
;
definition
let
T
be non
empty
TopSpace
;
let
F1
be
Filter
of the
carrier
of
T
;
let
F2
be
proper
Filter
of
(
BoolePoset
(
[#]
T
)
)
;
pred
F1
is_filter-finer_than
F2
means
:: FINTOPO7:def 18
BOOL2F
F2
c=
F1
;
end;
::
deftheorem
defines
is_filter-finer_than
FINTOPO7:def 18 :
for
T
being non
empty
TopSpace
for
F1
being
Filter
of the
carrier
of
T
for
F2
being
proper
Filter
of
(
BoolePoset
(
[#]
T
)
)
holds
(
F1
is_filter-finer_than
F2
iff
BOOL2F
F2
c=
F1
);
definition
let
T
be non
empty
TopSpace
;
let
F
be
Filter
of the
carrier
of
T
;
func
lim_filtre
F
->
Subset
of
T
equals
:: FINTOPO7:def 19
{
x
where
x
is
Point
of
T
:
F
is_filter-finer_than
NeighborhoodSystem
x
}
;
correctness
coherence
{
x
where
x
is
Point
of
T
:
F
is_filter-finer_than
NeighborhoodSystem
x
}
is
Subset
of
T
;
proof
end;
end;
::
deftheorem
defines
lim_filtre
FINTOPO7:def 19 :
for
T
being non
empty
TopSpace
for
F
being
Filter
of the
carrier
of
T
holds
lim_filtre
F
=
{
x
where
x
is
Point
of
T
:
F
is_filter-finer_than
NeighborhoodSystem
x
}
;
definition
let
T
be non
empty
TopSpace
;
let
B
be
filter_base
of the
carrier
of
T
;
func
Lim
B
->
Subset
of
T
equals
:: FINTOPO7:def 20
lim_filtre
<.
B
.)
;
correctness
coherence
lim_filtre
<.
B
.)
is
Subset
of
T
;
;
end;
::
deftheorem
defines
Lim
FINTOPO7:def 20 :
for
T
being non
empty
TopSpace
for
B
being
filter_base
of the
carrier
of
T
holds
Lim
B
=
lim_filtre
<.
B
.)
;
theorem
Th19
:
:: FINTOPO7:30
for
T
being non
empty
TopSpace
for
F
being
Filter
of the
carrier
of
T
holds
F
is
proper
Filter
of
(
BoolePoset
the
carrier
of
T
)
proof
end;
definition
let
T
be non
empty
TopSpace
;
let
F
be
Filter
of the
carrier
of
T
;
func
F2BOOL
(
F
,
T
)
->
proper
Filter
of
(
BoolePoset
(
[#]
T
)
)
equals
:: FINTOPO7:def 21
F
;
coherence
F
is
proper
Filter
of
(
BoolePoset
(
[#]
T
)
)
proof
end;
end;
::
deftheorem
defines
F2BOOL
FINTOPO7:def 21 :
for
T
being non
empty
TopSpace
for
F
being
Filter
of the
carrier
of
T
holds
F2BOOL
(
F
,
T
)
=
F
;
theorem
:: FINTOPO7:31
for
T
being non
empty
TopSpace
for
x
being
Point
of
T
for
F
being
Filter
of the
carrier
of
T
holds
(
x
is_a_convergence_point_of
F
,
T
iff
x
is_a_convergence_point_of
F2BOOL
(
F
,
T
),
T
) ;
theorem
:: FINTOPO7:32
for
T
being non
empty
TopSpace
for
x
being
Point
of
T
for
F
being
Filter
of the
carrier
of
T
holds
(
x
is_a_convergence_point_of
F
,
T
iff
x
in
lim_filtre
F
)
proof
end;
definition
let
T
be non
empty
TopSpace
;
let
F
be
Filter
of
(
BoolePoset
(
[#]
T
)
)
;
func
lim_filtreb
F
->
Subset
of
T
equals
:: FINTOPO7:def 22
{
x
where
x
is
Point
of
T
:
NeighborhoodSystem
x
c=
F
}
;
correctness
coherence
{
x
where
x
is
Point
of
T
:
NeighborhoodSystem
x
c=
F
}
is
Subset
of
T
;
proof
end;
end;
::
deftheorem
defines
lim_filtreb
FINTOPO7:def 22 :
for
T
being non
empty
TopSpace
for
F
being
Filter
of
(
BoolePoset
(
[#]
T
)
)
holds
lim_filtreb
F
=
{
x
where
x
is
Point
of
T
:
NeighborhoodSystem
x
c=
F
}
;
theorem
:: FINTOPO7:33
for
T
being non
empty
TopSpace
for
F
being
Filter
of the
carrier
of
T
holds
lim_filtre
F
=
lim_filtreb
(
F2BOOL
(
F
,
T
)
)
proof
end;
theorem
:: FINTOPO7:34
for
T
being non
empty
TopSpace
for
F
being
Filter
of the
carrier
of
T
holds
Lim
(
a_net
(
F2BOOL
(
F
,
T
)
)
)
=
lim_filtre
F
proof
end;
theorem
Th20
:
:: FINTOPO7:35
for
T
being non
empty
Hausdorff
TopSpace
for
F
being
Filter
of the
carrier
of
T
for
p
,
q
being
Point
of
T
st
p
in
lim_filtre
F
&
q
in
lim_filtre
F
holds
p
=
q
proof
end;
registration
let
T
be non
empty
Hausdorff
TopSpace
;
let
F
be
Filter
of the
carrier
of
T
;
cluster
lim_filtre
F
->
trivial
;
coherence
lim_filtre
F
is
trivial
proof
end;
end;
definition
let
ETV
be
FMT_TopSpace
;
let
x
be
Element
of
ETV
;
let
A
be
Subset
of
ETV
;
pred
x
is_a_cluster_point_of
A
,
ETV
means
:: FINTOPO7:def 23
for
V
being
Element
of
U_FMT
x
holds
V
meets
A
;
end;
::
deftheorem
defines
is_a_cluster_point_of
FINTOPO7:def 23 :
for
ETV
being
FMT_TopSpace
for
x
being
Element
of
ETV
for
A
being
Subset
of
ETV
holds
(
x
is_a_cluster_point_of
A
,
ETV
iff for
V
being
Element
of
U_FMT
x
holds
V
meets
A
);
definition
let
ETV
be
FMT_TopSpace
;
let
x
be
Element
of
ETV
;
func
FU_FMT
x
->
Filter
of the
carrier
of
ETV
equals
:: FINTOPO7:def 24
U_FMT
x
;
coherence
U_FMT
x
is
Filter
of the
carrier
of
ETV
by
def01
;
end;
::
deftheorem
defines
FU_FMT
FINTOPO7:def 24 :
for
ETV
being
FMT_TopSpace
for
x
being
Element
of
ETV
holds
FU_FMT
x
=
U_FMT
x
;
definition
let
ETV
be
FMT_TopSpace
;
let
F
be
Filter
of the
carrier
of
ETV
;
let
x
be
Element
of
ETV
;
pred
x
is_a_convergence_point_of
F
means
:: FINTOPO7:def 25
FU_FMT
x
is_filter-coarser_than
F
;
end;
::
deftheorem
defines
is_a_convergence_point_of
FINTOPO7:def 25 :
for
ETV
being
FMT_TopSpace
for
F
being
Filter
of the
carrier
of
ETV
for
x
being
Element
of
ETV
holds
(
x
is_a_convergence_point_of
F
iff
FU_FMT
x
is_filter-coarser_than
F
);
definition
let
ETV
be
FMT_TopSpace
;
let
F
be
Filter
of the
carrier
of
ETV
;
func
lim_filtre
F
->
Subset
of
ETV
equals
:: FINTOPO7:def 26
{
x
where
x
is
Element
of
ETV
:
x
is_a_convergence_point_of
F
}
;
correctness
coherence
{
x
where
x
is
Element
of
ETV
:
x
is_a_convergence_point_of
F
}
is
Subset
of
ETV
;
proof
end;
end;
::
deftheorem
defines
lim_filtre
FINTOPO7:def 26 :
for
ETV
being
FMT_TopSpace
for
F
being
Filter
of the
carrier
of
ETV
holds
lim_filtre
F
=
{
x
where
x
is
Element
of
ETV
:
x
is_a_convergence_point_of
F
}
;
theorem
:: FINTOPO7:36
for
ETV
being
FMT_TopSpace
for
x
being
Element
of
ETV
holds
( not the
carrier
of
ETV
is
empty
&
U_FMT
x
is
Filter
of the
carrier
of
ETV
)
by
def01
;
definition
let
ETV
be
FMT_TopSpace
;
let
F
be
Filter
of the
carrier
of
ETV
;
let
B
be
basis
of
F
;
func
lim_filtre
B
->
Subset
of
ETV
equals
:: FINTOPO7:def 27
lim_filtre
F
;
correctness
coherence
lim_filtre
F
is
Subset
of
ETV
;
;
end;
::
deftheorem
defines
lim_filtre
FINTOPO7:def 27 :
for
ETV
being
FMT_TopSpace
for
F
being
Filter
of the
carrier
of
ETV
for
B
being
basis
of
F
holds
lim_filtre
B
=
lim_filtre
F
;
notation
let
ETV
be
FMT_TopSpace
;
let
x
be
Element
of
ETV
;
synonym
NeighborhoodSystem
x
for
U_FMT
x
;
end;
definition
let
ETV
be
FMT_TopSpace
;
let
B
be
filter_base
of the
carrier
of
ETV
;
func
lim_filtre
B
->
Subset
of
ETV
equals
:: FINTOPO7:def 28
lim_filtre
<.
B
.)
;
correctness
coherence
lim_filtre
<.
B
.)
is
Subset
of
ETV
;
;
end;
::
deftheorem
defines
lim_filtre
FINTOPO7:def 28 :
for
ETV
being
FMT_TopSpace
for
B
being
filter_base
of the
carrier
of
ETV
holds
lim_filtre
B
=
lim_filtre
<.
B
.)
;
theorem
:: FINTOPO7:37
for
ETV
being non
empty
strict
FMT_Space_Str
st
ETV
is
PP1
holds
ETV
is
Fo_filled
;
theorem
Th21
:
:: FINTOPO7:38
for
ETV
being non
empty
strict
FMT_Space_Str
st
ETV
is
Fo_filled
& ( for
x
being
Element
of
ETV
holds not
U_FMT
x
is
empty
) holds
ETV
is
PP1
proof
end;
theorem
:: FINTOPO7:39
for
ETV
being non
empty
strict
FMT_Space_Str
st
ETV
is
Fo_filled
&
ETV
is
PP0
holds
ETV
is
PP1
proof
end;
theorem
:: FINTOPO7:40
for
T
being non
empty
TopStruct
holds
NeighSp
T
is non
empty
FMT_Space_Str
;
registration
let
T
be non
empty
TopSpace
;
cluster
NeighSp
T
->
Fo_filled
;
coherence
NeighSp
T
is
Fo_filled
proof
end;
end;
theorem
:: FINTOPO7:41
for
FMT
being non
empty
FMT_Space_Str
ex
S
being
RelStr
st
for
x
being
Element
of
FMT
holds
U_FMT
x
is
Subset
of
S
proof
end;
definition
let
ETV
be non
empty
TopSpace
;
attr
ETV
is
PP4
means
:: FINTOPO7:def 29
ex
R
being non
empty
FMT_Space_Str
st
for
x
being
Element
of
R
for
y
being
Element
of
(
NeighSp
ETV
)
for
z
being
Subset-Family
of the
carrier
of
ETV
st
x
=
y
&
z
=
U_FMT
y
holds
the
BNbd
of
R
.
x
=
<.
z
.]
;
end;
::
deftheorem
defines
PP4
FINTOPO7:def 29 :
for
ETV
being non
empty
TopSpace
holds
(
ETV
is
PP4
iff ex
R
being non
empty
FMT_Space_Str
st
for
x
being
Element
of
R
for
y
being
Element
of
(
NeighSp
ETV
)
for
z
being
Subset-Family
of the
carrier
of
ETV
st
x
=
y
&
z
=
U_FMT
y
holds
the
BNbd
of
R
.
x
=
<.
z
.]
);
theorem
:: FINTOPO7:42
for
X
being non
empty
set
for
S
being
Element
of
bool
(
bool
X
)
holds
<.
S
.]
is
Element
of
bool
(
bool
X
)
;
theorem
:: FINTOPO7:43
for
ETV
being non
empty
FMT_Space_Str
holds
bool
(
bool
(
rng
the
BNbd
of
ETV
)
)
c=
bool
(
bool
(
bool
(
bool
the
carrier
of
ETV
)
)
)
proof
end;