:: OPENLATT semantic presentation
begin
registration
cluster
non
empty
Lattice-like
lower-bounded
Heyting
->
non
empty
Lattice-like
lower-bounded
implicative
for ( ( ) ( )
LattStr
) ;
cluster
non
empty
Lattice-like
implicative
->
non
empty
Lattice-like
upper-bounded
for ( ( ) ( )
LattStr
) ;
end;
theorem
:: OPENLATT:1
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) holds
A
: ( ( ) ( )
Subset
of )
/\
(
Int
(
(
A
: ( ( ) ( )
Subset
of )
`
)
: ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
\/
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
open
)
Element
of
K19
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
B
: ( ( ) ( )
Subset
of ) ;
theorem
:: OPENLATT:2
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
,
B
,
C
being ( ( ) ( )
Subset
of ) st
C
: ( ( ) ( )
Subset
of ) is
open
&
A
: ( ( ) ( )
Subset
of )
/\
C
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
c=
B
: ( ( ) ( )
Subset
of ) holds
C
: ( ( ) ( )
Subset
of )
c=
Int
(
(
A
: ( ( ) ( )
Subset
of )
`
)
: ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
\/
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
open
)
Element
of
K19
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
definition
let
T
be ( ( ) ( )
TopStruct
) ;
func
Topology_of
T
->
( ( ) ( )
Subset-Family
of )
equals
:: OPENLATT:def 1
the
topology
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
Element
of
K19
(
K19
( the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
cluster
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
Subset-Family
of )
->
non
empty
;
end;
definition
let
T
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
P
,
Q
be ( ( ) ( )
Element
of
Topology_of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Subset-Family
of ) ) ;
:: original:
\/
redefine
func
P
\/
Q
->
( ( ) ( )
Element
of
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
Subset-Family
of ) ) ;
:: original:
/\
redefine
func
P
/\
Q
->
( ( ) ( )
Element
of
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
Subset-Family
of ) ) ;
end;
definition
let
T
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
func
Top_Union
T
->
( (
Function-like
quasi_total
) (
Relation-like
K20
(
(
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( non
empty
)
Subset-Family
of ) ,
(
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( non
empty
)
Subset-Family
of ) ) : ( ( ) ( non
empty
)
set
)
-defined
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
Subset-Family
of )
-valued
Function-like
quasi_total
)
BinOp
of
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
Subset-Family
of ) )
means
:: OPENLATT:def 2
for
P
,
Q
being ( ( ) ( )
Element
of
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
Subset-Family
of ) ) holds
it
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
.
(
P
: ( ( ) ( )
Element
of
Topology_of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Subset-Family
of ) ) ,
Q
: ( ( ) ( )
Element
of
Topology_of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Subset-Family
of ) ) ) : ( ( ) ( )
Element
of
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
Subset-Family
of ) )
=
P
: ( ( ) ( )
Element
of
Topology_of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Subset-Family
of ) )
\/
Q
: ( ( ) ( )
Element
of
Topology_of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Subset-Family
of ) ) : ( ( ) ( )
Element
of
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
Subset-Family
of ) ) ;
func
Top_Meet
T
->
( (
Function-like
quasi_total
) (
Relation-like
K20
(
(
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( non
empty
)
Subset-Family
of ) ,
(
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( non
empty
)
Subset-Family
of ) ) : ( ( ) ( non
empty
)
set
)
-defined
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
Subset-Family
of )
-valued
Function-like
quasi_total
)
BinOp
of
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
Subset-Family
of ) )
means
:: OPENLATT:def 3
for
P
,
Q
being ( ( ) ( )
Element
of
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
Subset-Family
of ) ) holds
it
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
.
(
P
: ( ( ) ( )
Element
of
Topology_of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Subset-Family
of ) ) ,
Q
: ( ( ) ( )
Element
of
Topology_of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Subset-Family
of ) ) ) : ( ( ) ( )
Element
of
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
Subset-Family
of ) )
=
P
: ( ( ) ( )
Element
of
Topology_of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Subset-Family
of ) )
/\
Q
: ( ( ) ( )
Element
of
Topology_of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Subset-Family
of ) ) : ( ( ) ( )
Element
of
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
Subset-Family
of ) ) ;
end;
theorem
:: OPENLATT:3
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) holds
LattStr
(#
(
Topology_of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
)
: ( ( ) ( non
empty
)
Subset-Family
of ) ,
(
Top_Union
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
K20
(
(
Topology_of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
)
: ( ( ) ( non
empty
)
Subset-Family
of ) ,
(
Topology_of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
)
: ( ( ) ( non
empty
)
Subset-Family
of ) ) : ( ( ) ( non
empty
)
set
)
-defined
Topology_of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Subset-Family
of )
-valued
Function-like
quasi_total
)
BinOp
of
Topology_of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Subset-Family
of ) ) ,
(
Top_Meet
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
K20
(
(
Topology_of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
)
: ( ( ) ( non
empty
)
Subset-Family
of ) ,
(
Topology_of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
)
: ( ( ) ( non
empty
)
Subset-Family
of ) ) : ( ( ) ( non
empty
)
set
)
-defined
Topology_of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Subset-Family
of )
-valued
Function-like
quasi_total
)
BinOp
of
Topology_of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Subset-Family
of ) ) #) : ( (
strict
) ( non
empty
strict
)
LattStr
) is ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
)
Lattice
) ;
definition
let
T
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
func
Open_setLatt
T
->
( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
)
Lattice
)
equals
:: OPENLATT:def 4
LattStr
(#
(
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( non
empty
)
Subset-Family
of ) ,
(
Top_Union
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
K20
(
(
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( non
empty
)
Subset-Family
of ) ,
(
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( non
empty
)
Subset-Family
of ) ) : ( ( ) ( non
empty
)
set
)
-defined
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
Subset-Family
of )
-valued
Function-like
quasi_total
)
BinOp
of
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
Subset-Family
of ) ) ,
(
Top_Meet
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
K20
(
(
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( non
empty
)
Subset-Family
of ) ,
(
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( non
empty
)
Subset-Family
of ) ) : ( ( ) ( non
empty
)
set
)
-defined
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
Subset-Family
of )
-valued
Function-like
quasi_total
)
BinOp
of
Topology_of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
Subset-Family
of ) ) #) : ( (
strict
) ( non
empty
strict
)
LattStr
) ;
end;
theorem
:: OPENLATT:4
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) holds the
carrier
of
(
Open_setLatt
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
)
Lattice
) : ( ( ) ( non
empty
)
set
)
=
Topology_of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Subset-Family
of ) ;
theorem
:: OPENLATT:5
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
p
,
q
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
p
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"\/"
q
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
(
Open_setLatt
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
)
Lattice
) : ( ( ) ( non
empty
)
set
) )
=
p
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\/
q
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) &
p
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
q
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
(
Open_setLatt
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
)
Lattice
) : ( ( ) ( non
empty
)
set
) )
=
p
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
/\
q
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: OPENLATT:6
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
p
,
q
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
p
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
[=
q
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) iff
p
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
c=
q
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: OPENLATT:7
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
p
,
q
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
for
p9
,
q9
being ( ( ) ( )
Element
of
Topology_of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Subset-Family
of ) ) st
p
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
p9
: ( ( ) ( )
Element
of
Topology_of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Subset-Family
of ) ) &
q
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
q9
: ( ( ) ( )
Element
of
Topology_of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Subset-Family
of ) ) holds
(
p
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
[=
q
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) iff
p9
: ( ( ) ( )
Element
of
Topology_of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Subset-Family
of ) )
c=
q9
: ( ( ) ( )
Element
of
Topology_of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Subset-Family
of ) ) ) ;
registration
let
T
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
cluster
Open_setLatt
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
)
Lattice
)
->
non
empty
Lattice-like
implicative
;
end;
theorem
:: OPENLATT:8
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) holds
(
Open_setLatt
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
upper-bounded
implicative
)
Lattice
) is
lower-bounded
&
Bottom
(
Open_setLatt
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
upper-bounded
implicative
)
Lattice
) : ( ( ) ( )
Element
of the
carrier
of
(
Open_setLatt
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
upper-bounded
implicative
)
Lattice
) : ( ( ) ( non
empty
)
set
) )
=
{}
: ( ( ) (
empty
)
set
) ) ;
registration
let
T
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
cluster
Open_setLatt
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
upper-bounded
implicative
)
Lattice
)
->
non
empty
Lattice-like
Heyting
;
end;
theorem
:: OPENLATT:9
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) holds
Top
(
Open_setLatt
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
Lattice
) : ( ( ) ( )
Element
of the
carrier
of
(
Open_setLatt
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
Lattice
) : ( ( ) ( non
empty
)
set
) )
=
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ;
definition
let
L
be ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ;
func
F_primeSet
L
->
( ( ) ( )
set
)
equals
:: OPENLATT:def 5
{
F
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ) where
F
is ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) ) : (
F
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) )
<>
the
carrier
of
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) &
F
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ) is
prime
)
}
;
end;
theorem
:: OPENLATT:10
for
L
being ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
for
F
being ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ) holds
(
F
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) )
in
F_primeSet
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( )
set
) iff (
F
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) )
<>
the
carrier
of
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
) &
F
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ) is
prime
) ) ;
definition
let
L
be ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ;
func
StoneH
L
->
( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
means
:: OPENLATT:def 6
for
a
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) holds
(
dom
it
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
)
=
the
carrier
of
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) &
it
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
.
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
)
=
{
F
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ) where
F
is ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) ) : (
F
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) )
in
F_primeSet
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) &
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
F
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ) )
}
);
end;
theorem
:: OPENLATT:11
for
L
being ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
for
F
being ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) )
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
F
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) )
in
(
StoneH
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
)
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) iff (
F
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) )
in
F_primeSet
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( )
set
) &
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
F
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ) ) ) ;
theorem
:: OPENLATT:12
for
L
being ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
for
x
being ( ( ) ( )
set
) holds
(
x
: ( ( ) ( )
set
)
in
(
StoneH
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
)
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) iff ex
F
being ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ) st
(
F
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) )
=
x
: ( ( ) ( )
set
) &
F
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) )
<>
the
carrier
of
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
) &
F
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ) is
prime
&
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
F
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ) ) ) ;
definition
let
L
be ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ;
func
StoneS
L
->
( ( ) ( )
set
)
equals
:: OPENLATT:def 7
rng
(
StoneH
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
) ;
end;
registration
let
L
be ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ;
cluster
StoneS
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
LattStr
) : ( ( ) ( )
set
)
->
non
empty
;
end;
theorem
:: OPENLATT:13
for
L
being ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
for
x
being ( ( ) ( )
set
) holds
(
x
: ( ( ) ( )
set
)
in
StoneS
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
) iff ex
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
set
)
=
(
StoneH
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
)
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: OPENLATT:14
for
L
being ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
StoneH
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
)
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"\/"
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
)
=
(
(
StoneH
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
)
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
set
)
\/
(
(
StoneH
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
)
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ;
theorem
:: OPENLATT:15
for
L
being ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
StoneH
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
)
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
)
=
(
(
StoneH
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
)
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
set
)
/\
(
(
StoneH
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
)
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ;
definition
let
L
be ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ;
let
a
be ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
func
SF_have
a
->
( ( ) ( )
Subset-Family
of )
equals
:: OPENLATT:def 8
{
F
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ) where
F
is ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) ) :
a
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
in
F
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) )
}
;
end;
registration
let
L
be ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ;
let
a
be ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
cluster
SF_have
a
: ( ( ) ( )
Element
of the
carrier
of
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
LattStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset-Family
of )
->
non
empty
;
end;
theorem
:: OPENLATT:16
for
L
being ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
for
x
being ( ( ) ( )
set
) holds
(
x
: ( ( ) ( )
set
)
in
SF_have
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset-Family
of ) iff (
x
: ( ( ) ( )
set
) is ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ) &
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
x
: ( ( ) ( )
set
) ) ) ;
theorem
:: OPENLATT:17
for
L
being ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
for
b
,
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
for
x
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
)
in
(
SF_have
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
Subset-Family
of )
\
(
SF_have
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
Subset-Family
of ) : ( ( ) ( )
Element
of
K19
(
K19
( the
carrier
of
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
set
) is ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ) &
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
x
: ( ( ) ( )
set
) & not
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
x
: ( ( ) ( )
set
) ) ;
theorem
:: OPENLATT:18
for
L
being ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
for
b
,
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
for
Z
being ( ( ) ( )
set
) st
Z
: ( ( ) ( )
set
)
<>
{}
: ( ( ) (
empty
)
set
) &
Z
: ( ( ) ( )
set
)
c=
(
SF_have
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
Subset-Family
of )
\
(
SF_have
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
Subset-Family
of ) : ( ( ) ( )
Element
of
K19
(
K19
( the
carrier
of
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) &
Z
: ( ( ) ( )
set
) is
c=-linear
holds
ex
Y
being ( ( ) ( )
set
) st
(
Y
: ( ( ) ( )
set
)
in
(
SF_have
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
Subset-Family
of )
\
(
SF_have
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
Subset-Family
of ) : ( ( ) ( )
Element
of
K19
(
K19
( the
carrier
of
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) & ( for
X1
being ( ( ) ( )
set
) st
X1
: ( ( ) ( )
set
)
in
Z
: ( ( ) ( )
set
) holds
X1
: ( ( ) ( )
set
)
c=
Y
: ( ( ) ( )
set
) ) ) ;
theorem
:: OPENLATT:19
for
L
being ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
for
b
,
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st not
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
[=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
<.
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
.)
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
in
(
SF_have
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
Subset-Family
of )
\
(
SF_have
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
Subset-Family
of ) : ( ( ) ( )
Element
of
K19
(
K19
( the
carrier
of
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: OPENLATT:20
for
L
being ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
for
b
,
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st not
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
[=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
ex
F
being ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ) st
(
F
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) )
in
F_primeSet
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( )
set
) & not
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
F
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ) &
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
F
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ) ) ;
theorem
:: OPENLATT:21
for
L
being ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
ex
F
being ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ) st
F
: ( ( non
empty
final
meet-closed
) ( non
empty
final
meet-closed
join-closed
)
Filter
of
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) )
in
F_primeSet
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( )
set
) ;
theorem
:: OPENLATT:22
for
L
being ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<>
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
StoneH
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
)
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
)
<>
(
StoneH
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
)
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ;
registration
let
L
be ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ;
cluster
StoneH
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
LattStr
) : ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
->
Relation-like
Function-like
one-to-one
;
end;
definition
let
L
be ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ;
let
A
,
B
be ( ( ) ( )
Element
of
StoneS
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
) ) ;
:: original:
\/
redefine
func
A
\/
B
->
( ( ) ( )
Element
of
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) ) ;
:: original:
/\
redefine
func
A
/\
B
->
( ( ) ( )
Element
of
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) ) ;
end;
definition
let
L
be ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ;
func
Set_Union
L
->
( (
Function-like
quasi_total
) (
Relation-like
K20
(
(
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
set
) ,
(
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
-defined
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
BinOp
of
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) )
means
:: OPENLATT:def 9
for
A
,
B
being ( ( ) ( )
Element
of
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) ) holds
it
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
.
(
A
: ( ( ) ( )
Element
of
StoneS
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
) ) ,
B
: ( ( ) ( )
Element
of
StoneS
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( )
Element
of
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) )
=
A
: ( ( ) ( )
Element
of
StoneS
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
) )
\/
B
: ( ( ) ( )
Element
of
StoneS
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) ) ;
func
Set_Meet
L
->
( (
Function-like
quasi_total
) (
Relation-like
K20
(
(
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
set
) ,
(
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
-defined
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
BinOp
of
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) )
means
:: OPENLATT:def 10
for
A
,
B
being ( ( ) ( )
Element
of
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) ) holds
it
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
.
(
A
: ( ( ) ( )
Element
of
StoneS
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
) ) ,
B
: ( ( ) ( )
Element
of
StoneS
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( )
Element
of
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) )
=
A
: ( ( ) ( )
Element
of
StoneS
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
) )
/\
B
: ( ( ) ( )
Element
of
StoneS
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) ) ;
end;
theorem
:: OPENLATT:23
for
L
being ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) holds
LattStr
(#
(
StoneS
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
)
: ( ( ) ( non
empty
)
set
) ,
(
Set_Union
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
K20
(
(
StoneS
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
)
: ( ( ) ( non
empty
)
set
) ,
(
StoneS
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
)
: ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
StoneS
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
quasi_total
)
BinOp
of
StoneS
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
) ) ,
(
Set_Meet
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
K20
(
(
StoneS
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
)
: ( ( ) ( non
empty
)
set
) ,
(
StoneS
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
)
: ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
StoneS
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
quasi_total
)
BinOp
of
StoneS
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
)
LattStr
) is ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
)
Lattice
) ;
definition
let
L
be ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ;
func
StoneLatt
L
->
( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
)
Lattice
)
equals
:: OPENLATT:def 11
LattStr
(#
(
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
set
) ,
(
Set_Union
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
K20
(
(
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
set
) ,
(
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
-defined
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
BinOp
of
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) ) ,
(
Set_Meet
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
K20
(
(
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
set
) ,
(
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
-defined
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
BinOp
of
StoneS
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
)
LattStr
) ;
end;
theorem
:: OPENLATT:24
for
L
being ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) holds the
carrier
of
(
StoneLatt
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
)
Lattice
) : ( ( ) ( non
empty
)
set
)
=
StoneS
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( ) ( non
empty
)
set
) ;
theorem
:: OPENLATT:25
for
L
being ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
for
p
,
q
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
p
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"\/"
q
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
(
StoneLatt
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
)
Lattice
) : ( ( ) ( non
empty
)
set
) )
=
p
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\/
q
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) &
p
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"/\"
q
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
(
StoneLatt
b
1
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
)
Lattice
) : ( ( ) ( non
empty
)
set
) )
=
p
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
/\
q
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: OPENLATT:26
for
L
being ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
)
for
p
,
q
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
p
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
[=
q
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) iff
p
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
c=
q
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
definition
let
L
be ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ;
:: original:
StoneH
redefine
func
StoneH
L
->
( ( ) (
Relation-like
the
carrier
of
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
(
StoneLatt
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
)
Lattice
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
quasi_total
)
Homomorphism
of
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) ,
StoneLatt
L
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
)
Lattice
) ) ;
end;
registration
let
L
be ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ;
cluster
StoneH
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
LattStr
) : ( (
Relation-like
Function-like
) (
Relation-like
Function-like
one-to-one
)
Function
)
->
Function-like
quasi_total
bijective
for ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
LattStr
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
(
StoneLatt
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
LattStr
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
)
Lattice
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) ;
cluster
StoneLatt
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
LattStr
) : ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
)
Lattice
)
->
non
empty
Lattice-like
distributive
;
end;
theorem
:: OPENLATT:27
for
L
being ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) holds
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) ,
StoneLatt
L
: ( ( non
empty
Lattice-like
distributive
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
D_Lattice
) : ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
Lattice
)
are_isomorphic
;
registration
cluster
non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
for ( ( ) ( )
LattStr
) ;
end;
theorem
:: OPENLATT:28
for
H
being ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) holds
(
StoneH
H
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) : ( ( ) ( non
empty
non
trivial
)
set
)
-defined
the
carrier
of
(
StoneLatt
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
Lattice
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
one-to-one
quasi_total
bijective
)
Homomorphism
of
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) ,
StoneLatt
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) : ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
Lattice
) )
.
(
Top
H
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) : ( ( ) ( non
empty
non
trivial
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
(
StoneLatt
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
Lattice
) : ( ( ) ( non
empty
)
set
) )
=
F_primeSet
H
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) : ( ( ) ( )
set
) ;
theorem
:: OPENLATT:29
for
H
being ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) holds
(
StoneH
H
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) : ( ( ) ( non
empty
non
trivial
)
set
)
-defined
the
carrier
of
(
StoneLatt
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
Lattice
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
one-to-one
quasi_total
bijective
)
Homomorphism
of
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) ,
StoneLatt
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) : ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
Lattice
) )
.
(
Bottom
H
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) : ( ( ) ( non
empty
non
trivial
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
(
StoneLatt
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
)
Lattice
) : ( ( ) ( non
empty
)
set
) )
=
{}
: ( ( ) (
empty
)
set
) ;
theorem
:: OPENLATT:30
for
H
being ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) holds
StoneS
H
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) : ( ( ) ( non
empty
)
set
)
c=
bool
(
F_primeSet
H
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
Element
of
K19
(
K19
(
(
F_primeSet
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
registration
let
H
be ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) ;
cluster
F_primeSet
H
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
LattStr
) : ( ( ) ( )
set
)
->
non
empty
;
end;
definition
let
H
be ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) ;
func
HTopSpace
H
->
( (
strict
) (
strict
)
TopStruct
)
means
:: OPENLATT:def 12
( the
carrier
of
it
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
=
F_primeSet
H
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) & the
topology
of
it
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
Element
of
K19
(
K19
( the
carrier
of
it
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) )
=
{
(
union
A
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
set
) where
A
is ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) : verum
}
);
end;
registration
let
H
be ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) ;
cluster
HTopSpace
H
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
LattStr
) : ( (
strict
) (
strict
)
TopStruct
)
->
non
empty
strict
TopSpace-like
;
end;
theorem
:: OPENLATT:31
for
H
being ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) holds the
carrier
of
(
Open_setLatt
(
HTopSpace
H
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
Lattice
) : ( ( ) ( non
empty
)
set
)
=
{
(
union
A
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
set
) where
A
is ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) : verum
}
;
theorem
:: OPENLATT:32
for
H
being ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) holds
StoneS
H
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) : ( ( ) ( non
empty
)
set
)
c=
the
carrier
of
(
Open_setLatt
(
HTopSpace
H
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
Lattice
) : ( ( ) ( non
empty
)
set
) ;
definition
let
H
be ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) ;
:: original:
StoneH
redefine
func
StoneH
H
->
( ( ) (
Relation-like
the
carrier
of
H
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
(
Open_setLatt
(
HTopSpace
H
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( (
strict
) (
strict
)
TopStruct
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
)
Lattice
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
quasi_total
)
Homomorphism
of
H
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) ,
Open_setLatt
(
HTopSpace
H
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
)
)
: ( (
strict
) (
strict
)
TopStruct
) : ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
)
Lattice
) ) ;
end;
theorem
:: OPENLATT:33
for
H
being ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
for
p9
,
q9
being ( ( ) ( )
Element
of ( ( ) ( non
empty
non
trivial
)
set
) ) holds
(
StoneH
H
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) : ( ( ) ( non
empty
non
trivial
)
set
)
-defined
the
carrier
of
(
Open_setLatt
(
HTopSpace
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
Lattice
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
one-to-one
quasi_total
)
Homomorphism
of
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) ,
Open_setLatt
(
HTopSpace
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
) : ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
Lattice
) )
.
(
p9
: ( ( ) ( )
Element
of ( ( ) ( non
empty
non
trivial
)
set
) )
=>
q9
: ( ( ) ( )
Element
of ( ( ) ( non
empty
non
trivial
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) : ( ( ) ( non
empty
non
trivial
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
(
Open_setLatt
(
HTopSpace
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
Lattice
) : ( ( ) ( non
empty
)
set
) )
=
(
(
StoneH
H
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) : ( ( ) ( non
empty
non
trivial
)
set
)
-defined
the
carrier
of
(
Open_setLatt
(
HTopSpace
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
Lattice
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
one-to-one
quasi_total
)
Homomorphism
of
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) ,
Open_setLatt
(
HTopSpace
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
) : ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
Lattice
) )
.
p9
: ( ( ) ( )
Element
of ( ( ) ( non
empty
non
trivial
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
(
Open_setLatt
(
HTopSpace
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
Lattice
) : ( ( ) ( non
empty
)
set
) )
=>
(
(
StoneH
H
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) : ( ( ) ( non
empty
non
trivial
)
set
)
-defined
the
carrier
of
(
Open_setLatt
(
HTopSpace
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
Lattice
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
one-to-one
quasi_total
)
Homomorphism
of
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) ,
Open_setLatt
(
HTopSpace
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
) : ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
Lattice
) )
.
q9
: ( ( ) ( )
Element
of ( ( ) ( non
empty
non
trivial
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
(
Open_setLatt
(
HTopSpace
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
Lattice
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
(
Open_setLatt
(
HTopSpace
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
Lattice
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: OPENLATT:34
for
H
being ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) holds
StoneH
H
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) : ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) : ( ( ) ( non
empty
non
trivial
)
set
)
-defined
the
carrier
of
(
Open_setLatt
(
HTopSpace
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
Lattice
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
one-to-one
quasi_total
)
Homomorphism
of
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) ,
Open_setLatt
(
HTopSpace
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
) : ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
Lattice
) )
preserves_implication
;
theorem
:: OPENLATT:35
for
H
being ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) holds
StoneH
H
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) : ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) : ( ( ) ( non
empty
non
trivial
)
set
)
-defined
the
carrier
of
(
Open_setLatt
(
HTopSpace
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
Lattice
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
one-to-one
quasi_total
)
Homomorphism
of
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) ,
Open_setLatt
(
HTopSpace
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
) : ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
Lattice
) )
preserves_top
;
theorem
:: OPENLATT:36
for
H
being ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) holds
StoneH
H
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) : ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) : ( ( ) ( non
empty
non
trivial
)
set
)
-defined
the
carrier
of
(
Open_setLatt
(
HTopSpace
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
)
)
: ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
Lattice
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
one-to-one
quasi_total
)
Homomorphism
of
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
) ,
Open_setLatt
(
HTopSpace
b
1
: ( ( non
empty
non
trivial
Lattice-like
Heyting
) ( non
empty
non
trivial
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
H_Lattice
)
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
) : ( ( non
empty
Lattice-like
) ( non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V90
()
Heyting
implicative
)
Lattice
) )
preserves_bottom
;