:: On the Order-consistent Topology of Complete and Uncomplete Lattices
:: by Ewa Gr\c{a}dzka
::
:: Received May 23, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users
begin
definition
let
T
be non
empty
TopRelStr
;
attr
T
is
upper
means
:
Def1
:
:: WAYBEL32:def 1
{
(
(
downarrow
x
)
`
)
where
x
is
Element
of
T
: verum
}
is
prebasis
of
T
;
end;
::
deftheorem
Def1
defines
upper
WAYBEL32:def 1 :
for
T
being non
empty
TopRelStr
holds
(
T
is
upper
iff
{
(
(
downarrow
x
)
`
)
where
x
is
Element
of
T
: verum
}
is
prebasis
of
T
);
registration
cluster
non
empty
TopSpace-like
reflexive
transitive
antisymmetric
with_suprema
with_infima
up-complete
strict
Scott
for
TopRelStr
;
existence
ex
b
1
being
TopLattice
st
(
b
1
is
Scott
&
b
1
is
up-complete
&
b
1
is
strict
)
proof
end;
end;
definition
let
T
be non
empty
TopSpace-like
reflexive
TopRelStr
;
attr
T
is
order_consistent
means
:
Def2
:
:: WAYBEL32:def 2
for
x
being
Element
of
T
holds
(
downarrow
x
=
Cl
{
x
}
& ( for
N
being
eventually-directed
net
of
T
st
x
=
sup
N
holds
for
V
being
a_neighborhood
of
x
holds
N
is_eventually_in
V
) );
end;
::
deftheorem
Def2
defines
order_consistent
WAYBEL32:def 2 :
for
T
being non
empty
TopSpace-like
reflexive
TopRelStr
holds
(
T
is
order_consistent
iff for
x
being
Element
of
T
holds
(
downarrow
x
=
Cl
{
x
}
& ( for
N
being
eventually-directed
net
of
T
st
x
=
sup
N
holds
for
V
being
a_neighborhood
of
x
holds
N
is_eventually_in
V
) ) );
registration
cluster
1
-element
TopSpace-like
reflexive
->
1
-element
TopSpace-like
reflexive
upper
for
TopRelStr
;
coherence
for
b
1
being 1
-element
TopSpace-like
reflexive
TopRelStr
holds
b
1
is
upper
proof
end;
end;
registration
cluster
non
empty
trivial
TopSpace-like
reflexive
transitive
antisymmetric
with_suprema
with_infima
up-complete
strict
upper
for
TopRelStr
;
existence
ex
b
1
being
TopLattice
st
(
b
1
is
upper
&
b
1
is
trivial
&
b
1
is
up-complete
&
b
1
is
strict
)
proof
end;
end;
theorem
Th1
:
:: WAYBEL32:1
for
T
being non
empty
up-complete
upper
TopPoset
for
A
being
Subset
of
T
st
A
is
open
holds
A
is
upper
proof
end;
theorem
:: WAYBEL32:2
for
T
being non
empty
up-complete
TopPoset
st
T
is
upper
holds
T
is
order_consistent
proof
end;
theorem
Th3
:
:: WAYBEL32:3
for
R
being non
empty
reflexive
transitive
antisymmetric
up-complete
RelStr
ex
T
being
TopAugmentation
of
R
st
T
is
Scott
proof
end;
theorem
:: WAYBEL32:4
for
R
being non
empty
up-complete
Poset
for
T
being
TopAugmentation
of
R
st
T
is
Scott
holds
T
is
correct
;
registration
let
R
be non
empty
reflexive
transitive
antisymmetric
up-complete
RelStr
;
cluster
Scott
->
correct
for
TopAugmentation
of
R
;
coherence
for
b
1
being
TopAugmentation
of
R
st
b
1
is
Scott
holds
b
1
is
correct
;
end;
registration
let
R
be non
empty
reflexive
transitive
antisymmetric
up-complete
RelStr
;
cluster
non
empty
correct
reflexive
transitive
antisymmetric
up-complete
Scott
for
TopAugmentation
of
R
;
existence
ex
b
1
being
TopAugmentation
of
R
st
(
b
1
is
Scott
&
b
1
is
correct
)
proof
end;
end;
theorem
Th5
:
:: WAYBEL32:5
for
T
being non
empty
reflexive
transitive
antisymmetric
up-complete
Scott
TopRelStr
for
x
being
Element
of
T
holds
Cl
{
x
}
=
downarrow
x
proof
end;
theorem
Th6
:
:: WAYBEL32:6
for
T
being non
empty
up-complete
Scott
TopPoset
holds
T
is
order_consistent
proof
end;
theorem
Th7
:
:: WAYBEL32:7
for
R
being
/\-complete
Semilattice
for
Z
being
net
of
R
for
D
being
Subset
of
R
st
D
=
{
(
"/\"
(
{
(
Z
.
k
)
where
k
is
Element
of
Z
:
k
>=
j
}
,
R
)
)
where
j
is
Element
of
Z
: verum
}
holds
( not
D
is
empty
&
D
is
directed
)
proof
end;
theorem
Th8
:
:: WAYBEL32:8
for
R
being
/\-complete
Semilattice
for
S
being
Subset
of
R
for
a
being
Element
of
R
st
a
in
S
holds
"/\"
(
S
,
R
)
<=
a
proof
end;
theorem
Th9
:
:: WAYBEL32:9
for
R
being
/\-complete
Semilattice
for
N
being
reflexive
monotone
net
of
R
holds
lim_inf
N
=
sup
N
proof
end;
theorem
Th10
:
:: WAYBEL32:10
for
R
being
/\-complete
Semilattice
for
S
being
Subset
of
R
holds
(
S
in
the
topology
of
(
ConvergenceSpace
(
Scott-Convergence
R
)
)
iff (
S
is
inaccessible
&
S
is
upper
) )
proof
end;
theorem
Th11
:
:: WAYBEL32:11
for
R
being
up-complete
/\-complete
Semilattice
for
T
being
TopAugmentation
of
R
st the
topology
of
T
=
sigma
R
holds
T
is
Scott
proof
end;
registration
let
R
be
up-complete
/\-complete
Semilattice
;
cluster
non
empty
correct
reflexive
transitive
antisymmetric
up-complete
strict
Scott
for
TopAugmentation
of
R
;
existence
ex
b
1
being
TopAugmentation
of
R
st
(
b
1
is
strict
&
b
1
is
Scott
&
b
1
is
correct
)
proof
end;
end;
theorem
:: WAYBEL32:12
for
S
being
up-complete
/\-complete
Semilattice
for
T
being
Scott
TopAugmentation
of
S
holds
sigma
S
=
the
topology
of
T
proof
end;
theorem
:: WAYBEL32:13
for
T
being non
empty
reflexive
transitive
antisymmetric
up-complete
Scott
TopRelStr
holds
T
is
T_0-TopSpace
proof
end;
registration
let
R
be non
empty
reflexive
transitive
antisymmetric
up-complete
RelStr
;
cluster
->
up-complete
for
TopAugmentation
of
R
;
coherence
for
b
1
being
TopAugmentation
of
R
holds
b
1
is
up-complete
;
end;
theorem
Th14
:
:: WAYBEL32:14
for
R
being non
empty
reflexive
transitive
antisymmetric
up-complete
RelStr
for
T
being
Scott
TopAugmentation
of
R
for
x
being
Element
of
T
for
A
being
upper
Subset
of
T
st not
x
in
A
holds
(
downarrow
x
)
`
is
a_neighborhood
of
A
proof
end;
theorem
:: WAYBEL32:15
for
R
being non
empty
reflexive
transitive
antisymmetric
up-complete
TopRelStr
for
T
being
Scott
TopAugmentation
of
R
for
S
being
upper
Subset
of
T
ex
F
being
Subset-Family
of
T
st
(
S
=
meet
F
& ( for
X
being
Subset
of
T
st
X
in
F
holds
X
is
a_neighborhood
of
S
) )
proof
end;
theorem
:: WAYBEL32:16
for
T
being non
empty
reflexive
transitive
antisymmetric
up-complete
Scott
TopRelStr
for
S
being
Subset
of
T
holds
(
S
is
open
iff (
S
is
upper
&
S
is
property(S)
) )
proof
end;
theorem
Th17
:
:: WAYBEL32:17
for
R
being non
empty
reflexive
transitive
antisymmetric
up-complete
TopRelStr
for
S
being non
empty
directed
Subset
of
R
for
a
being
Element
of
R
st
a
in
S
holds
a
<=
"\/"
(
S
,
R
)
proof
end;
::Remark 1.4 (vi)
registration
let
T
be non
empty
reflexive
transitive
antisymmetric
up-complete
TopRelStr
;
cluster
lower
->
property(S)
for
Element
of
bool
the
carrier
of
T
;
coherence
for
b
1
being
Subset
of
T
st
b
1
is
lower
holds
b
1
is
property(S)
proof
end;
end;
theorem
:: WAYBEL32:18
for
T
being non
empty
finite
up-complete
Poset
for
S
being
Subset
of
T
holds
S
is
inaccessible
proof
end;
theorem
Th19
:
:: WAYBEL32:19
for
R
being
complete
connected
LATTICE
for
T
being
Scott
TopAugmentation
of
R
for
x
being
Element
of
T
holds
(
downarrow
x
)
`
is
open
proof
end;
theorem
:: WAYBEL32:20
for
R
being
complete
connected
LATTICE
for
T
being
Scott
TopAugmentation
of
R
for
S
being
Subset
of
T
holds
(
S
is
open
iff (
S
=
the
carrier
of
T
or
S
in
{
(
(
downarrow
x
)
`
)
where
x
is
Element
of
T
: verum
}
) )
proof
end;
registration
let
R
be non
empty
up-complete
Poset
;
cluster
non
empty
correct
reflexive
transitive
antisymmetric
up-complete
order_consistent
for
TopAugmentation
of
R
;
correctness
existence
ex
b
1
being
correct
TopAugmentation
of
R
st
b
1
is
order_consistent
;
proof
end;
end;
registration
cluster
non
empty
TopSpace-like
reflexive
transitive
antisymmetric
with_suprema
with_infima
complete
order_consistent
for
TopRelStr
;
correctness
existence
ex
b
1
being
TopLattice
st
(
b
1
is
order_consistent
&
b
1
is
complete
)
;
proof
end;
end;
theorem
Th21
:
:: WAYBEL32:21
for
R
being non
empty
TopRelStr
for
A
being
Subset
of
R
st ( for
x
being
Element
of
R
holds
downarrow
x
=
Cl
{
x
}
) &
A
is
open
holds
A
is
upper
proof
end;
theorem
:: WAYBEL32:22
for
R
being non
empty
TopRelStr
for
A
being
Subset
of
R
st ( for
x
being
Element
of
R
holds
downarrow
x
=
Cl
{
x
}
) holds
for
A
being
Subset
of
R
st
A
is
closed
holds
A
is
lower
proof
end;
definition
let
S
be non
empty
1-sorted
;
let
R
be non
empty
RelStr
;
let
f
be
Function
of the
carrier
of
R
, the
carrier
of
S
;
func
R
*'
f
->
non
empty
strict
NetStr
over
S
means
:
Def3
:
:: WAYBEL32:def 3
(
RelStr
(# the
carrier
of
it
, the
InternalRel
of
it
#)
=
RelStr
(# the
carrier
of
R
, the
InternalRel
of
R
#) & the
mapping
of
it
=
f
);
existence
ex
b
1
being non
empty
strict
NetStr
over
S
st
(
RelStr
(# the
carrier
of
b
1
, the
InternalRel
of
b
1
#)
=
RelStr
(# the
carrier
of
R
, the
InternalRel
of
R
#) & the
mapping
of
b
1
=
f
)
proof
end;
uniqueness
for
b
1
,
b
2
being non
empty
strict
NetStr
over
S
st
RelStr
(# the
carrier
of
b
1
, the
InternalRel
of
b
1
#)
=
RelStr
(# the
carrier
of
R
, the
InternalRel
of
R
#) & the
mapping
of
b
1
=
f
&
RelStr
(# the
carrier
of
b
2
, the
InternalRel
of
b
2
#)
=
RelStr
(# the
carrier
of
R
, the
InternalRel
of
R
#) & the
mapping
of
b
2
=
f
holds
b
1
=
b
2
;
end;
::
deftheorem
Def3
defines
*'
WAYBEL32:def 3 :
for
S
being non
empty
1-sorted
for
R
being non
empty
RelStr
for
f
being
Function
of the
carrier
of
R
, the
carrier
of
S
for
b
4
being non
empty
strict
NetStr
over
S
holds
(
b
4
=
R
*'
f
iff (
RelStr
(# the
carrier
of
b
4
, the
InternalRel
of
b
4
#)
=
RelStr
(# the
carrier
of
R
, the
InternalRel
of
R
#) & the
mapping
of
b
4
=
f
) );
registration
let
S
be non
empty
1-sorted
;
let
R
be non
empty
transitive
RelStr
;
let
f
be
Function
of the
carrier
of
R
, the
carrier
of
S
;
cluster
R
*'
f
->
non
empty
transitive
strict
;
coherence
R
*'
f
is
transitive
proof
end;
end;
registration
let
S
be non
empty
1-sorted
;
let
R
be non
empty
directed
RelStr
;
let
f
be
Function
of the
carrier
of
R
, the
carrier
of
S
;
cluster
R
*'
f
->
non
empty
strict
directed
;
coherence
R
*'
f
is
directed
proof
end;
end;
definition
let
R
be non
empty
RelStr
;
let
N
be
prenet
of
R
;
func
inf_net
N
->
strict
prenet
of
R
means
:
Def4
:
:: WAYBEL32:def 4
ex
f
being
Function
of
N
,
R
st
(
it
=
N
*'
f
& ( for
i
being
Element
of
N
holds
f
.
i
=
"/\"
(
{
(
N
.
k
)
where
k
is
Element
of
N
:
k
>=
i
}
,
R
) ) );
existence
ex
b
1
being
strict
prenet
of
R
ex
f
being
Function
of
N
,
R
st
(
b
1
=
N
*'
f
& ( for
i
being
Element
of
N
holds
f
.
i
=
"/\"
(
{
(
N
.
k
)
where
k
is
Element
of
N
:
k
>=
i
}
,
R
) ) )
proof
end;
uniqueness
for
b
1
,
b
2
being
strict
prenet
of
R
st ex
f
being
Function
of
N
,
R
st
(
b
1
=
N
*'
f
& ( for
i
being
Element
of
N
holds
f
.
i
=
"/\"
(
{
(
N
.
k
)
where
k
is
Element
of
N
:
k
>=
i
}
,
R
) ) ) & ex
f
being
Function
of
N
,
R
st
(
b
2
=
N
*'
f
& ( for
i
being
Element
of
N
holds
f
.
i
=
"/\"
(
{
(
N
.
k
)
where
k
is
Element
of
N
:
k
>=
i
}
,
R
) ) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def4
defines
inf_net
WAYBEL32:def 4 :
for
R
being non
empty
RelStr
for
N
being
prenet
of
R
for
b
3
being
strict
prenet
of
R
holds
(
b
3
=
inf_net
N
iff ex
f
being
Function
of
N
,
R
st
(
b
3
=
N
*'
f
& ( for
i
being
Element
of
N
holds
f
.
i
=
"/\"
(
{
(
N
.
k
)
where
k
is
Element
of
N
:
k
>=
i
}
,
R
) ) ) );
registration
let
R
be non
empty
RelStr
;
let
N
be
net
of
R
;
cluster
inf_net
N
->
transitive
strict
;
coherence
inf_net
N
is
transitive
proof
end;
end;
registration
let
R
be non
empty
RelStr
;
let
N
be
net
of
R
;
cluster
inf_net
N
->
strict
;
coherence
inf_net
N
is
directed
;
end;
registration
let
R
be non
empty
reflexive
antisymmetric
/\-complete
RelStr
;
let
N
be
net
of
R
;
cluster
inf_net
N
->
strict
monotone
;
coherence
inf_net
N
is
monotone
proof
end;
end;
registration
let
R
be non
empty
reflexive
antisymmetric
/\-complete
RelStr
;
let
N
be
net
of
R
;
cluster
inf_net
N
->
strict
eventually-directed
;
coherence
inf_net
N
is
eventually-directed
;
end;
theorem
Th23
:
:: WAYBEL32:23
for
R
being non
empty
RelStr
for
N
being
net
of
R
holds
rng
the
mapping
of
(
inf_net
N
)
=
{
(
"/\"
(
{
(
N
.
i
)
where
i
is
Element
of
N
:
i
>=
j
}
,
R
)
)
where
j
is
Element
of
N
: verum
}
proof
end;
theorem
Th24
:
:: WAYBEL32:24
for
R
being
up-complete
/\-complete
LATTICE
for
N
being
net
of
R
holds
sup
(
inf_net
N
)
=
lim_inf
N
proof
end;
theorem
:: WAYBEL32:25
for
R
being
up-complete
/\-complete
LATTICE
for
N
being
net
of
R
for
i
being
Element
of
N
holds
sup
(
inf_net
N
)
=
lim_inf
(
N
|
i
)
proof
end;
theorem
Th26
:
:: WAYBEL32:26
for
R
being
/\-complete
Semilattice
for
N
being
net
of
R
for
V
being
upper
Subset
of
R
st
inf_net
N
is_eventually_in
V
holds
N
is_eventually_in
V
proof
end;
theorem
:: WAYBEL32:27
for
R
being
/\-complete
Semilattice
for
N
being
net
of
R
for
V
being
lower
Subset
of
R
st
N
is_eventually_in
V
holds
inf_net
N
is_eventually_in
V
proof
end;
theorem
Th28
:
:: WAYBEL32:28
for
R
being non
empty
up-complete
/\-complete
order_consistent
TopLattice
for
N
being
net
of
R
for
x
being
Element
of
R
st
x
<=
lim_inf
N
holds
x
is_a_cluster_point_of
N
proof
end;
theorem
:: WAYBEL32:29
for
R
being non
empty
up-complete
/\-complete
order_consistent
TopLattice
for
N
being
eventually-directed
net
of
R
for
x
being
Element
of
R
holds
(
x
<=
lim_inf
N
iff
x
is_a_cluster_point_of
N
)
proof
end;