:: OPENLATT semantic presentation

registration

cluster Heyting -> implicative LattStr ;
coherence by LATTICE2:def 6;
cluster implicative -> upper-bounded LattStr ;
coherence by FILTER_0:37;

end;

theorem Th1: :: OPENLATT:1

for T being TopSpace
for A, B being Subset of T holds A /\ (Int ((A ` ) \/ B)) c= B

proof end;

theorem Th2: :: OPENLATT:2

for T being TopSpace
for A, B, C being Subset of T st C is open & A /\ C c= B holds
C c= Int ((A ` ) \/ B)

proof end;

definition

let T be TopStruct ;
func Topology_of T -> Subset-Family of T equals :: OPENLATT:def 1
the topology of T;
coherence ;

end;

:: deftheorem defines Topology_of OPENLATT:def 1 :

registration

let T be TopSpace;
cluster Topology_of T -> non empty ;
coherence by PRE_TOPC:5;

end;

theorem Th3: :: OPENLATT:3

for T being TopSpace
for A being Subset of T holds
( A is open iff A in Topology_of T ) by PRE_TOPC:def 5;

definition

let T be non empty TopSpace;
let P, Q be Element of Topology_of T;
:: original: \/
redefine func P \/ Q -> Element of Topology_of T;
coherence

proof end;

:: original: /\
redefine func P /\ Q -> Element of Topology_of T;
coherence

proof end;

end;

definition

let T be non empty TopSpace;
func Top_Union T -> BinOp of Topology_of T means :Def2: :: OPENLATT:def 2
for P, Q being Element of Topology_of T holds it . P,Q = P \/ Q;
existence

proof end;

uniqueness

proof end;

func Top_Meet T -> BinOp of Topology_of T means :Def3: :: OPENLATT:def 3
for P, Q being Element of Topology_of T holds it . P,Q = P /\ Q;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Top_Union OPENLATT:def 2 :

:: deftheorem Def3 defines Top_Meet OPENLATT:def 3 :

Lm1: for T being non empty TopSpace
for p, q being Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) holds p "\/" q = p \/ q
by Def2;

Lm2: for T being non empty TopSpace
for p, q being Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) holds p "/\" q = p /\ q
by Def3;

theorem Th4: :: OPENLATT:4

for T being non empty TopSpace holds LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is Lattice

proof end;

definition

let T be non empty TopSpace;
func Open_setLatt T -> Lattice equals :: OPENLATT:def 4
LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #);
coherence by Th4;

end;

:: deftheorem defines Open_setLatt OPENLATT:def 4 :

theorem :: OPENLATT:5

for T being non empty TopSpace holds the carrier of (Open_setLatt T) = Topology_of T ;

theorem Th6: :: OPENLATT:6

for T being non empty TopSpace
for p, q being Element of (Open_setLatt T) holds
( p "\/" q = p \/ q & p "/\" q = p /\ q ) by Def2, Def3;

theorem Th7: :: OPENLATT:7

for T being non empty TopSpace
for p, q being Element of (Open_setLatt T) holds
( p [= q iff p c= q )

proof end;

theorem Th8: :: OPENLATT:8

for T being non empty TopSpace
for p, q being Element of (Open_setLatt T)
for p', q' being Element of Topology_of T st p = p' & q = q' holds
( p [= q iff p' c= q' )

proof end;

theorem Th9: :: OPENLATT:9

for T being non empty TopSpace holds Open_setLatt T is implicative

proof end;

theorem Th10: :: OPENLATT:10

for T being non empty TopSpace holds
( Open_setLatt T is lower-bounded & Bottom (Open_setLatt T) = {} )

proof end;

registration

let T be non empty TopSpace;
cluster Open_setLatt T -> upper-bounded Heyting ;
coherence

proof end;

end;

theorem Th11: :: OPENLATT:11

for T being non empty TopSpace holds Top (Open_setLatt T) = the carrier of T

proof end;

definition

let L be D_Lattice;
func F_primeSet L -> set equals :: OPENLATT:def 5
{ F where F is Filter of L : ( F <> the carrier of L & F is prime ) } ;
coherence ;

end;

:: deftheorem defines F_primeSet OPENLATT:def 5 :

theorem Th12: :: OPENLATT:12

for L being D_Lattice
for F being Filter of L holds
( F in F_primeSet L iff ( F <> the carrier of L & F is prime ) )

proof end;

definition

let L be D_Lattice;
func StoneH L -> Function means :Def6: :: OPENLATT:def 6
for a being Element of L holds
( dom it = the carrier of L & it . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines StoneH OPENLATT:def 6 :

theorem Th13: :: OPENLATT:13

for L being D_Lattice
for F being Filter of L
for a being Element of L holds
( F in (StoneH L) . a iff ( F in F_primeSet L & a in F ) )

proof end;

theorem Th14: :: OPENLATT:14

for L being D_Lattice
for a being Element of L
for x being set holds
( x in (StoneH L) . a iff ex F being Filter of L st
( F = x & F <> the carrier of L & F is prime & a in F ) )

proof end;

definition

let L be D_Lattice;
func StoneS L -> set equals :: OPENLATT:def 7
rng (StoneH L);
coherence ;

end;

:: deftheorem defines StoneS OPENLATT:def 7 :

registration

let L be D_Lattice;
cluster StoneS L -> non empty ;
coherence

proof end;

end;

theorem Th15: :: OPENLATT:15

for L being D_Lattice
for x being set holds
( x in StoneS L iff ex a being Element of L st x = (StoneH L) . a )

proof end;

theorem Th16: :: OPENLATT:16

for L being D_Lattice
for a, b being Element of L holds (StoneH L) . (a "\/" b) = ((StoneH L) . a) \/ ((StoneH L) . b)

proof end;

theorem Th17: :: OPENLATT:17

for L being D_Lattice
for a, b being Element of L holds (StoneH L) . (a "/\" b) = ((StoneH L) . a) /\ ((StoneH L) . b)

proof end;

definition

let L be D_Lattice;
let a be Element of L;
func SF_have a -> Subset-Family of L equals :: OPENLATT:def 8
{ F where F is Filter of L : a in F } ;
coherence

proof end;

end;

:: deftheorem defines SF_have OPENLATT:def 8 :

registration

let L be D_Lattice;
let a be Element of L;
cluster SF_have a -> non empty ;
coherence

proof end;

end;

theorem Th18: :: OPENLATT:18

for L being D_Lattice
for a being Element of L
for x being set holds
( x in SF_have a iff ( x is Filter of L & a in x ) )

proof end;

Lm3: for L being D_Lattice
for F being Filter of L
for b, a being Element of L holds
( F in (SF_have b) \ (SF_have a) iff ( b in F & not a in F ) )

proof end;

theorem Th19: :: OPENLATT:19

for L being D_Lattice
for b, a being Element of L
for x being set st x in (SF_have b) \ (SF_have a) holds
( x is Filter of L & b in x & not a in x )

proof end;

theorem Th20: :: OPENLATT:20

for L being D_Lattice
for b, a being Element of L
for Z being set st Z <> {} & Z c= (SF_have b) \ (SF_have a) & Z is c=-linear holds
ex Y being set st
( Y in (SF_have b) \ (SF_have a) & ( for X1 being set st X1 in Z holds
X1 c= Y ) )

proof end;

theorem Th21: :: OPENLATT:21

for L being D_Lattice
for b, a being Element of L st not b [= a holds
<.b.) in (SF_have b) \ (SF_have a)

proof end;

theorem Th22: :: OPENLATT:22

for L being D_Lattice
for b, a being Element of L st not b [= a holds
ex F being Filter of L st
( F in F_primeSet L & not a in F & b in F )

proof end;

theorem Th23: :: OPENLATT:23

for L being D_Lattice
for a, b being Element of L st a <> b holds
ex F being Filter of L st F in F_primeSet L

proof end;

theorem Th24: :: OPENLATT:24

for L being D_Lattice
for a, b being Element of L st a <> b holds
(StoneH L) . a <> (StoneH L) . b

proof end;

theorem Th25: :: OPENLATT:25

for L being D_Lattice holds StoneH L is one-to-one

proof end;

definition

let L be D_Lattice;
let A, B be Element of StoneS L;
:: original: \/
redefine func A \/ B -> Element of StoneS L;
coherence

proof end;

:: original: /\
redefine func A /\ B -> Element of StoneS L;
coherence

proof end;

end;

definition

let L be D_Lattice;
func Set_Union L -> BinOp of StoneS L means :Def9: :: OPENLATT:def 9
for A, B being Element of StoneS L holds it . A,B = A \/ B;
existence

proof end;

uniqueness

proof end;

func Set_Meet L -> BinOp of StoneS L means :Def10: :: OPENLATT:def 10
for A, B being Element of StoneS L holds it . A,B = A /\ B;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines Set_Union OPENLATT:def 9 :

:: deftheorem Def10 defines Set_Meet OPENLATT:def 10 :

Lm4: for L being D_Lattice
for x, y being Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) holds x "\/" y = x \/ y
by Def9;

Lm5: for L being D_Lattice
for x, y being Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) holds x "/\" y = x /\ y
by Def10;

theorem Th26: :: OPENLATT:26

for L being D_Lattice holds LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is Lattice

proof end;

definition

let L be D_Lattice;
func StoneLatt L -> Lattice equals :: OPENLATT:def 11
LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #);
coherence by Th26;

end;

:: deftheorem defines StoneLatt OPENLATT:def 11 :

theorem :: OPENLATT:27

for L being D_Lattice holds the carrier of (StoneLatt L) = StoneS L ;

theorem Th28: :: OPENLATT:28

for L being D_Lattice
for p, q being Element of (StoneLatt L) holds
( p "\/" q = p \/ q & p "/\" q = p /\ q ) by Lm4, Lm5;

theorem :: OPENLATT:29

for L being D_Lattice
for p, q being Element of (StoneLatt L) holds
( p [= q iff p c= q )

proof end;

definition

let L be D_Lattice;
:: original: StoneH
redefine func StoneH L -> Homomorphism of L, StoneLatt L;
coherence

proof end;

end;

theorem Th30: :: OPENLATT:30

for L being D_Lattice holds StoneH L is isomorphism

proof end;

theorem :: OPENLATT:31

for L being D_Lattice holds StoneLatt L is distributive

proof end;

theorem :: OPENLATT:32

for L being D_Lattice holds L, StoneLatt L are_isomorphic

proof end;

registration

cluster upper-bounded non trivial LattStr ;
existence

proof end;

end;

theorem Th33: :: OPENLATT:33

for H being non trivial H_Lattice holds (StoneH H) . (Top H) = F_primeSet H

proof end;

theorem Th34: :: OPENLATT:34

for H being non trivial H_Lattice holds (StoneH H) . (Bottom H) = {}

proof end;

theorem Th35: :: OPENLATT:35

for H being non trivial H_Lattice holds StoneS H c= bool (F_primeSet H)

proof end;

registration

let H be non trivial H_Lattice;
cluster F_primeSet H -> non empty ;
coherence

proof end;

end;

definition

let H be non trivial H_Lattice;
func HTopSpace H -> strict TopStruct means :Def12: :: OPENLATT:def 12
( the carrier of it = F_primeSet H & the topology of it = { (union A) where A is Subset of (StoneS H) : verum } );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def12 defines HTopSpace OPENLATT:def 12 :

registration

let H be non trivial H_Lattice;
cluster HTopSpace H -> non empty strict TopSpace-like ;
coherence

proof end;

end;

theorem Th36: :: OPENLATT:36

for H being non trivial H_Lattice holds the carrier of (Open_setLatt (HTopSpace H)) = { (union A) where A is Subset of (StoneS H) : verum } by Def12;

theorem Th37: :: OPENLATT:37