:: Algebraic Lattices
:: by Robert Milewski
::
:: Received December 1, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users
begin
definition
let
L
be non
empty
reflexive
RelStr
;
func
CompactSublatt
L
->
strict
full
SubRelStr
of
L
means
:
Def1
:
:: WAYBEL_8:def 1
for
x
being
Element
of
L
holds
(
x
in
the
carrier
of
it
iff
x
is
compact
);
existence
ex
b
1
being
strict
full
SubRelStr
of
L
st
for
x
being
Element
of
L
holds
(
x
in
the
carrier
of
b
1
iff
x
is
compact
)
proof
end;
uniqueness
for
b
1
,
b
2
being
strict
full
SubRelStr
of
L
st ( for
x
being
Element
of
L
holds
(
x
in
the
carrier
of
b
1
iff
x
is
compact
) ) & ( for
x
being
Element
of
L
holds
(
x
in
the
carrier
of
b
2
iff
x
is
compact
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def1
defines
CompactSublatt
WAYBEL_8:def 1 :
for
L
being non
empty
reflexive
RelStr
for
b
2
being
strict
full
SubRelStr
of
L
holds
(
b
2
=
CompactSublatt
L
iff for
x
being
Element
of
L
holds
(
x
in
the
carrier
of
b
2
iff
x
is
compact
) );
registration
let
L
be non
empty
reflexive
antisymmetric
lower-bounded
RelStr
;
cluster
CompactSublatt
L
->
non
empty
strict
full
;
coherence
not
CompactSublatt
L
is
empty
proof
end;
end;
theorem
:: WAYBEL_8:1
for
L
being
complete
LATTICE
for
x
,
y
,
k
being
Element
of
L
st
x
<=
k
&
k
<=
y
&
k
in
the
carrier
of
(
CompactSublatt
L
)
holds
x
<<
y
proof
end;
theorem
:: WAYBEL_8:2
for
L
being
complete
LATTICE
for
x
being
Element
of
L
holds
(
uparrow
x
is
Open
Filter
of
L
iff
x
is
compact
)
proof
end;
theorem
:: WAYBEL_8:3
for
L
being non
empty
with_suprema
lower-bounded
Poset
holds
(
CompactSublatt
L
is
join-inheriting
&
Bottom
L
in
the
carrier
of
(
CompactSublatt
L
)
)
proof
end;
definition
let
L
be non
empty
reflexive
RelStr
;
let
x
be
Element
of
L
;
func
compactbelow
x
->
Subset
of
L
equals
:: WAYBEL_8:def 2
{
y
where
y
is
Element
of
L
: (
x
>=
y
&
y
is
compact
)
}
;
coherence
{
y
where
y
is
Element
of
L
: (
x
>=
y
&
y
is
compact
)
}
is
Subset
of
L
proof
end;
end;
::
deftheorem
defines
compactbelow
WAYBEL_8:def 2 :
for
L
being non
empty
reflexive
RelStr
for
x
being
Element
of
L
holds
compactbelow
x
=
{
y
where
y
is
Element
of
L
: (
x
>=
y
&
y
is
compact
)
}
;
theorem
Th4
:
:: WAYBEL_8:4
for
L
being non
empty
reflexive
RelStr
for
x
,
y
being
Element
of
L
holds
(
y
in
compactbelow
x
iff (
x
>=
y
&
y
is
compact
) )
proof
end;
theorem
Th5
:
:: WAYBEL_8:5
for
L
being non
empty
reflexive
RelStr
for
x
being
Element
of
L
holds
compactbelow
x
=
(
downarrow
x
)
/\
the
carrier
of
(
CompactSublatt
L
)
proof
end;
theorem
Th6
:
:: WAYBEL_8:6
for
L
being non
empty
reflexive
transitive
RelStr
for
x
being
Element
of
L
holds
compactbelow
x
c=
waybelow
x
proof
end;
registration
let
L
be non
empty
reflexive
antisymmetric
lower-bounded
RelStr
;
let
x
be
Element
of
L
;
cluster
compactbelow
x
->
non
empty
;
coherence
not
compactbelow
x
is
empty
proof
end;
end;
begin
definition
let
L
be non
empty
reflexive
RelStr
;
attr
L
is
satisfying_axiom_K
means
:
Def3
:
:: WAYBEL_8:def 3
for
x
being
Element
of
L
holds
x
=
sup
(
compactbelow
x
)
;
end;
::
deftheorem
Def3
defines
satisfying_axiom_K
WAYBEL_8:def 3 :
for
L
being non
empty
reflexive
RelStr
holds
(
L
is
satisfying_axiom_K
iff for
x
being
Element
of
L
holds
x
=
sup
(
compactbelow
x
)
);
definition
let
L
be non
empty
reflexive
RelStr
;
attr
L
is
algebraic
means
:
Def4
:
:: WAYBEL_8:def 4
( ( for
x
being
Element
of
L
holds
( not
compactbelow
x
is
empty
&
compactbelow
x
is
directed
) ) &
L
is
up-complete
&
L
is
satisfying_axiom_K
);
end;
::
deftheorem
Def4
defines
algebraic
WAYBEL_8:def 4 :
for
L
being non
empty
reflexive
RelStr
holds
(
L
is
algebraic
iff ( ( for
x
being
Element
of
L
holds
( not
compactbelow
x
is
empty
&
compactbelow
x
is
directed
) ) &
L
is
up-complete
&
L
is
satisfying_axiom_K
) );
theorem
Th7
:
:: WAYBEL_8:7
for
L
being
LATTICE
holds
(
L
is
algebraic
iff (
L
is
continuous
& ( for
x
,
y
being
Element
of
L
st
x
<<
y
holds
ex
k
being
Element
of
L
st
(
k
in
the
carrier
of
(
CompactSublatt
L
)
&
x
<=
k
&
k
<=
y
) ) ) )
proof
end;
registration
cluster
reflexive
transitive
antisymmetric
with_suprema
with_infima
algebraic
->
continuous
for
RelStr
;
coherence
for
b
1
being
LATTICE
st
b
1
is
algebraic
holds
b
1
is
continuous
by
Th7
;
end;
registration
cluster
non
empty
reflexive
algebraic
->
non
empty
reflexive
up-complete
satisfying_axiom_K
for
RelStr
;
coherence
for
b
1
being non
empty
reflexive
RelStr
st
b
1
is
algebraic
holds
(
b
1
is
up-complete
&
b
1
is
satisfying_axiom_K
)
by
Def4
;
end;
registration
let
L
be non
empty
with_suprema
Poset
;
cluster
CompactSublatt
L
->
strict
full
join-inheriting
;
coherence
CompactSublatt
L
is
join-inheriting
proof
end;
end;
definition
let
L
be non
empty
reflexive
RelStr
;
attr
L
is
arithmetic
means
:
Def5
:
:: WAYBEL_8:def 5
(
L
is
algebraic
&
CompactSublatt
L
is
meet-inheriting
);
end;
::
deftheorem
Def5
defines
arithmetic
WAYBEL_8:def 5 :
for
L
being non
empty
reflexive
RelStr
holds
(
L
is
arithmetic
iff (
L
is
algebraic
&
CompactSublatt
L
is
meet-inheriting
) );
begin
registration
cluster
reflexive
transitive
antisymmetric
with_suprema
with_infima
arithmetic
->
algebraic
for
RelStr
;
coherence
for
b
1
being
LATTICE
st
b
1
is
arithmetic
holds
b
1
is
algebraic
by
Def5
;
end;
registration
cluster
trivial
reflexive
transitive
antisymmetric
with_suprema
with_infima
->
arithmetic
for
RelStr
;
coherence
for
b
1
being
LATTICE
st
b
1
is
trivial
holds
b
1
is
arithmetic
proof
end;
end;
registration
cluster
non
empty
1
-element
strict
reflexive
transitive
antisymmetric
with_suprema
with_infima
for
RelStr
;
existence
ex
b
1
being
LATTICE
st
(
b
1
is 1
-element
&
b
1
is
strict
)
proof
end;
end;
theorem
Th8
:
:: WAYBEL_8:8
for
L1
,
L2
being non
empty
reflexive
antisymmetric
RelStr
st
RelStr
(# the
carrier
of
L1
, the
InternalRel
of
L1
#)
=
RelStr
(# the
carrier
of
L2
, the
InternalRel
of
L2
#) &
L1
is
up-complete
holds
for
x1
,
y1
being
Element
of
L1
for
x2
,
y2
being
Element
of
L2
st
x1
=
x2
&
y1
=
y2
&
x1
<<
y1
holds
x2
<<
y2
proof
end;
theorem
Th9
:
:: WAYBEL_8:9
for
L1
,
L2
being non
empty
reflexive
antisymmetric
RelStr
st
RelStr
(# the
carrier
of
L1
, the
InternalRel
of
L1
#)
=
RelStr
(# the
carrier
of
L2
, the
InternalRel
of
L2
#) &
L1
is
up-complete
holds
for
x
being
Element
of
L1
for
y
being
Element
of
L2
st
x
=
y
&
x
is
compact
holds
y
is
compact
proof
end;
theorem
Th10
:
:: WAYBEL_8:10
for
L1
,
L2
being non
empty
reflexive
antisymmetric
up-complete
RelStr
st
RelStr
(# the
carrier
of
L1
, the
InternalRel
of
L1
#)
=
RelStr
(# the
carrier
of
L2
, the
InternalRel
of
L2
#) holds
for
x
being
Element
of
L1
for
y
being
Element
of
L2
st
x
=
y
holds
compactbelow
x
=
compactbelow
y
proof
end;
theorem
:: WAYBEL_8:11
for
L1
,
L2
being
RelStr
st
RelStr
(# the
carrier
of
L1
, the
InternalRel
of
L1
#)
=
RelStr
(# the
carrier
of
L2
, the
InternalRel
of
L2
#) & not
L1
is
empty
holds
not
L2
is
empty
;
theorem
Th12
:
:: WAYBEL_8:12
for
L1
,
L2
being
RelStr
st
RelStr
(# the
carrier
of
L1
, the
InternalRel
of
L1
#)
=
RelStr
(# the
carrier
of
L2
, the
InternalRel
of
L2
#) &
L1
is
reflexive
holds
L2
is
reflexive
proof
end;
theorem
Th13
:
:: WAYBEL_8:13
for
L1
,
L2
being
RelStr
st
RelStr
(# the
carrier
of
L1
, the
InternalRel
of
L1
#)
=
RelStr
(# the
carrier
of
L2
, the
InternalRel
of
L2
#) &
L1
is
transitive
holds
L2
is
transitive
proof
end;
theorem
Th14
:
:: WAYBEL_8:14
for
L1
,
L2
being
RelStr
st
RelStr
(# the
carrier
of
L1
, the
InternalRel
of
L1
#)
=
RelStr
(# the
carrier
of
L2
, the
InternalRel
of
L2
#) &
L1
is
antisymmetric
holds
L2
is
antisymmetric
proof
end;
theorem
Th15
:
:: WAYBEL_8:15
for
L1
,
L2
being non
empty
reflexive
RelStr
st
RelStr
(# the
carrier
of
L1
, the
InternalRel
of
L1
#)
=
RelStr
(# the
carrier
of
L2
, the
InternalRel
of
L2
#) &
L1
is
up-complete
holds
L2
is
up-complete
proof
end;
theorem
Th16
:
:: WAYBEL_8:16
for
L1
,
L2
being non
empty
reflexive
antisymmetric
up-complete
RelStr
st
RelStr
(# the
carrier
of
L1
, the
InternalRel
of
L1
#)
=
RelStr
(# the
carrier
of
L2
, the
InternalRel
of
L2
#) &
L1
is
satisfying_axiom_K
& ( for
x
being
Element
of
L1
holds
( not
compactbelow
x
is
empty
&
compactbelow
x
is
directed
) ) holds
L2
is
satisfying_axiom_K
proof
end;
theorem
Th17
:
:: WAYBEL_8:17
for
L1
,
L2
being non
empty
reflexive
antisymmetric
RelStr
st
RelStr
(# the
carrier
of
L1
, the
InternalRel
of
L1
#)
=
RelStr
(# the
carrier
of
L2
, the
InternalRel
of
L2
#) &
L1
is
algebraic
holds
L2
is
algebraic
proof
end;
theorem
Th18
:
:: WAYBEL_8:18
for
L1
,
L2
being
LATTICE
st
RelStr
(# the
carrier
of
L1
, the
InternalRel
of
L1
#)
=
RelStr
(# the
carrier
of
L2
, the
InternalRel
of
L2
#) &
L1
is
arithmetic
holds
L2
is
arithmetic
proof
end;
registration
let
L
be non
empty
RelStr
;
cluster
RelStr
(# the
carrier
of
L
, the
InternalRel
of
L
#)
->
non
empty
;
coherence
not
RelStr
(# the
carrier
of
L
, the
InternalRel
of
L
#) is
empty
;
end;
registration
let
L
be non
empty
reflexive
RelStr
;
cluster
RelStr
(# the
carrier
of
L
, the
InternalRel
of
L
#)
->
reflexive
;
coherence
RelStr
(# the
carrier
of
L
, the
InternalRel
of
L
#) is
reflexive
by
Th12
;
end;
registration
let
L
be
transitive
RelStr
;
cluster
RelStr
(# the
carrier
of
L
, the
InternalRel
of
L
#)
->
transitive
;
coherence
RelStr
(# the
carrier
of
L
, the
InternalRel
of
L
#) is
transitive
by
Th13
;
end;
registration
let
L
be
antisymmetric
RelStr
;
cluster
RelStr
(# the
carrier
of
L
, the
InternalRel
of
L
#)
->
antisymmetric
;
coherence
RelStr
(# the
carrier
of
L
, the
InternalRel
of
L
#) is
antisymmetric
by
Th14
;
end;
registration
let
L
be
with_infima
RelStr
;
cluster
RelStr
(# the
carrier
of
L
, the
InternalRel
of
L
#)
->
with_infima
;
coherence
RelStr
(# the
carrier
of
L
, the
InternalRel
of
L
#) is
with_infima
by
YELLOW_7:14
;
end;
registration
let
L
be
with_suprema
RelStr
;
cluster
RelStr
(# the
carrier
of
L
, the
InternalRel
of
L
#)
->
with_suprema
;
coherence
RelStr
(# the
carrier
of
L
, the
InternalRel
of
L
#) is
with_suprema
by
YELLOW_7:15
;
end;
registration
let
L
be non
empty
reflexive
up-complete
RelStr
;
cluster
RelStr
(# the
carrier
of
L
, the
InternalRel
of
L
#)
->
up-complete
;
coherence
RelStr
(# the
carrier
of
L
, the
InternalRel
of
L
#) is
up-complete
by
Th15
;
end;
registration
let
L
be non
empty
reflexive
antisymmetric
algebraic
RelStr
;
cluster
RelStr
(# the
carrier
of
L
, the
InternalRel
of
L
#)
->
algebraic
;
coherence
RelStr
(# the
carrier
of
L
, the
InternalRel
of
L
#) is
algebraic
by
Th17
;
end;
registration
let
L
be
arithmetic
LATTICE
;
cluster
RelStr
(# the
carrier
of
L
, the
InternalRel
of
L
#)
->
arithmetic
;
coherence
RelStr
(# the
carrier
of
L
, the
InternalRel
of
L
#) is
arithmetic
by
Th18
;
end;
theorem
:: WAYBEL_8:19
for
L
being
algebraic
LATTICE
holds
(
L
is
arithmetic
iff
CompactSublatt
L
is
LATTICE
)
proof
end;
theorem
Th20
:
:: WAYBEL_8:20
for
L
being
lower-bounded
algebraic
LATTICE
holds
(
L
is
arithmetic
iff
L
-waybelow
is
multiplicative
)
proof
end;
theorem
:: WAYBEL_8:21
for
L
being
lower-bounded
arithmetic
LATTICE
for
p
being
Element
of
L
st
p
is
pseudoprime
holds
p
is
prime
proof
end;
theorem
:: WAYBEL_8:22
for
L
being
lower-bounded
distributive
algebraic
LATTICE
st ( for
p
being
Element
of
L
st
p
is
pseudoprime
holds
p
is
prime
) holds
L
is
arithmetic
proof
end;
registration
let
L
be
algebraic
LATTICE
;
let
c
be
closure
Function
of
L
,
L
;
cluster
non
empty
directed
for
Element
of
bool
the
carrier
of
(
Image
c
)
;
existence
ex
b
1
being
Subset
of
(
Image
c
)
st
( not
b
1
is
empty
&
b
1
is
directed
)
proof
end;
end;
theorem
Th23
:
:: WAYBEL_8:23
for
L
being
algebraic
LATTICE
for
c
being
closure
Function
of
L
,
L
st
c
is
directed-sups-preserving
holds
c
.:
(
[#]
(
CompactSublatt
L
)
)
c=
[#]
(
CompactSublatt
(
Image
c
)
)
proof
end;
theorem
:: WAYBEL_8:24
for
L
being
lower-bounded
algebraic
LATTICE
for
c
being
closure
Function
of
L
,
L
st
c
is
directed-sups-preserving
holds
Image
c
is
algebraic
LATTICE
proof
end;
theorem
:: WAYBEL_8:25
for
L
being
lower-bounded
algebraic
LATTICE
for
c
being
closure
Function
of
L
,
L
st
c
is
directed-sups-preserving
holds
c
.:
(
[#]
(
CompactSublatt
L
)
)
=
[#]
(
CompactSublatt
(
Image
c
)
)
proof
end;
begin
theorem
Th26
:
:: WAYBEL_8:26
for
X
,
x
being
set
holds
(
x
is
Element
of
(
BoolePoset
X
)
iff
x
c=
X
)
proof
end;
theorem
Th27
:
:: WAYBEL_8:27
for
X
being
set
for
x
,
y
being
Element
of
(
BoolePoset
X
)
holds
(
x
<<
y
iff for
Y
being
Subset-Family
of
X
st
y
c=
union
Y
holds
ex
Z
being
finite
Subset
of
Y
st
x
c=
union
Z
)
proof
end;
theorem
Th28
:
:: WAYBEL_8:28
for
X
being
set
for
x
being
Element
of
(
BoolePoset
X
)
holds
(
x
is
finite
iff
x
is
compact
)
proof
end;
theorem
Th29
:
:: WAYBEL_8:29
for
X
being
set
for
x
being
Element
of
(
BoolePoset
X
)
holds
compactbelow
x
=
{
y
where
y
is
finite
Subset
of
x
: verum
}
proof
end;
theorem
:: WAYBEL_8:30
for
X
being
set
for
F
being
Subset
of
X
holds
(
F
in
the
carrier
of
(
CompactSublatt
(
BoolePoset
X
)
)
iff
F
is
finite
)
proof
end;
registration
let
X
be
set
;
let
x
be
Element
of
(
BoolePoset
X
)
;
cluster
compactbelow
x
->
directed
lower
;
coherence
(
compactbelow
x
is
lower
&
compactbelow
x
is
directed
)
proof
end;
end;
theorem
Th31
:
:: WAYBEL_8:31
for
X
being
set
holds
BoolePoset
X
is
algebraic
proof
end;
registration
let
X
be
set
;
cluster
BoolePoset
X
->
algebraic
;
coherence
BoolePoset
X
is
algebraic
by
Th31
;
end;