:: 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 b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds b₂ /\ (Int ((b₂ ` ) \/ b₃)) c= b₃

proof end;

theorem Th2: :: OPENLATT:2

for b₁ being TopSpace
for b₂, b₃, b₄ being Subset of b₁ st b₄ is open & b₂ /\ b₄ c= b₃ holds
b₄ c= Int ((b₂ ` ) \/ b₃)

proof end;

definition

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

end;

:: deftheorem Def1 defines Topology_of OPENLATT:def 1 :

registration

let c₁ be TopSpace;
cluster Topology_of a₁ -> non empty ;
coherence by PRE_TOPC:5;

end;

theorem Th3: :: OPENLATT:3

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is open iff b₂ in Topology_of b₁ ) by PRE_TOPC:def 5;

definition

let c₁ be non empty TopSpace;
let c₂, c₃ be Element of Topology_of c₁;
redefine func \/ as c₂ \/ c₃ -> Element of Topology_of a₁;
coherence

proof end;

redefine func /\ as c₂ /\ c₃ -> Element of Topology_of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty TopSpace;
func Top_Union c₁ -> BinOp of Topology_of a₁ means :Def2: :: OPENLATT:def 2
for b₁, b₂ being Element of Topology_of a₁ holds a₂ . b₁,b₂ = b₁ \/ b₂;
existence

proof end;

uniqueness

proof end;

func Top_Meet c₁ -> BinOp of Topology_of a₁ means :Def3: :: OPENLATT:def 3
for b₁, b₂ being Element of Topology_of a₁ holds a₂ . b₁,b₂ = b₁ /\ b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Top_Union OPENLATT:def 2 :

:: deftheorem Def3 defines Top_Meet OPENLATT:def 3 :

Lemma6: for b₁ being non empty TopSpace
for b₂, b₃ being Element of LattStr(# (Topology_of b₁),(Top_Union b₁),(Top_Meet b₁) #) holds b₂ "\/" b₃ = b₂ \/ b₃
by Def2;

Lemma7: for b₁ being non empty TopSpace
for b₂, b₃ being Element of LattStr(# (Topology_of b₁),(Top_Union b₁),(Top_Meet b₁) #) holds b₂ "/\" b₃ = b₂ /\ b₃
by Def3;

theorem Th4: :: OPENLATT:4

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

proof end;

definition

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

end;

:: deftheorem Def4 defines Open_setLatt OPENLATT:def 4 :

theorem Th5: :: OPENLATT:5

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

theorem Th6: :: OPENLATT:6

for b₁ being non empty TopSpace
for b₂, b₃ being Element of (Open_setLatt b₁) holds
( b₂ "\/" b₃ = b₂ \/ b₃ & b₂ "/\" b₃ = b₂ /\ b₃ ) by Def2, Def3;

theorem Th7: :: OPENLATT:7

for b₁ being non empty TopSpace
for b₂, b₃ being Element of (Open_setLatt b₁) holds
( b₂ [= b₃ iff b₂ c= b₃ )

proof end;

theorem Th8: :: OPENLATT:8

for b₁ being non empty TopSpace
for b₂, b₃ being Element of (Open_setLatt b₁)
for b₄, b₅ being Element of Topology_of b₁ st b₂ = b₄ & b₃ = b₅ holds
( b₂ [= b₃ iff b₄ c= b₅ )

proof end;

theorem Th9: :: OPENLATT:9

for b₁ being non empty TopSpace holds Open_setLatt b₁ is implicative

proof end;

theorem Th10: :: OPENLATT:10

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

proof end;

registration

let c₁ be non empty TopSpace;
cluster Open_setLatt a₁ -> upper-bounded Heyting ;
coherence

proof end;

end;

theorem Th11: :: OPENLATT:11

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

proof end;

definition

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

end;

:: deftheorem Def5 defines F_primeSet OPENLATT:def 5 :

theorem Th12: :: OPENLATT:12

for b₁ being D_Lattice
for b₂ being Filter of b₁ holds
( b₂ in F_primeSet b₁ iff ( b₂ <> the carrier of b₁ & b₂ is prime ) )

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines StoneH OPENLATT:def 6 :

theorem Th13: :: OPENLATT:13

for b₁ being D_Lattice
for b₂ being Filter of b₁
for b₃ being Element of b₁ holds
( b₂ in (StoneH b₁) . b₃ iff ( b₂ in F_primeSet b₁ & b₃ in b₂ ) )

proof end;

theorem Th14: :: OPENLATT:14

for b₁ being D_Lattice
for b₂ being Element of b₁
for b₃ being set holds
( b₃ in (StoneH b₁) . b₂ iff ex b₄ being Filter of b₁ st
( b₄ = b₃ & b₄ <> the carrier of b₁ & b₄ is prime & b₂ in b₄ ) )

proof end;

definition

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

end;

:: deftheorem Def7 defines StoneS OPENLATT:def 7 :

registration

let c₁ be D_Lattice;
cluster StoneS a₁ -> non empty ;
coherence

proof end;

end;

theorem Th15: :: OPENLATT:15

for b₁ being D_Lattice
for b₂ being set holds
( b₂ in StoneS b₁ iff ex b₃ being Element of b₁ st b₂ = (StoneH b₁) . b₃ )

proof end;

theorem Th16: :: OPENLATT:16

for b₁ being D_Lattice
for b₂, b₃ being Element of b₁ holds (StoneH b₁) . (b₂ "\/" b₃) = ((StoneH b₁) . b₂) \/ ((StoneH b₁) . b₃)

proof end;

theorem Th17: :: OPENLATT:17

for b₁ being D_Lattice
for b₂, b₃ being Element of b₁ holds (StoneH b₁) . (b₂ "/\" b₃) = ((StoneH b₁) . b₂) /\ ((StoneH b₁) . b₃)

proof end;

definition

let c₁ be D_Lattice;
let c₂ be Element of c₁;
func SF_have c₂ -> Subset-Family of a₁ equals :: OPENLATT:def 8
{ b₁ where B is Filter of a₁ : a₂ in b₁ } ;
coherence

proof end;

end;

:: deftheorem Def8 defines SF_have OPENLATT:def 8 :

registration

let c₁ be D_Lattice;
let c₂ be Element of c₁;
cluster SF_have a₂ -> non empty ;
coherence

proof end;

end;

theorem Th18: :: OPENLATT:18

for b₁ being D_Lattice
for b₂ being Element of b₁
for b₃ being set holds
( b₃ in SF_have b₂ iff ( b₃ is Filter of b₁ & b₂ in b₃ ) )

proof end;

Lemma23: for b₁ being D_Lattice
for b₂ being Filter of b₁
for b₃, b₄ being Element of b₁ holds
( b₂ in (SF_have b₃) \ (SF_have b₄) iff ( b₃ in b₂ & not b₄ in b₂ ) )

proof end;

theorem Th19: :: OPENLATT:19

for b₁ being D_Lattice
for b₂, b₃ being Element of b₁
for b₄ being set st b₄ in (SF_have b₂) \ (SF_have b₃) holds
( b₄ is Filter of b₁ & b₂ in b₄ & not b₃ in b₄ )

proof end;

theorem Th20: :: OPENLATT:20

for b₁ being D_Lattice
for b₂, b₃ being Element of b₁
for b₄ being set st b₄ <> {} & b₄ c= (SF_have b₂) \ (SF_have b₃) & b₄ is c=-linear holds
ex b₅ being set st
( b₅ in (SF_have b₂) \ (SF_have b₃) & ( for b₆ being set st b₆ in b₄ holds
b₆ c= b₅ ) )

proof end;

theorem Th21: :: OPENLATT:21

for b₁ being D_Lattice
for b₂, b₃ being Element of b₁ st not b₂ [= b₃ holds
<.b₂.) in (SF_have b₂) \ (SF_have b₃)

proof end;

theorem Th22: :: OPENLATT:22

for b₁ being D_Lattice
for b₂, b₃ being Element of b₁ st not b₂ [= b₃ holds
ex b₄ being Filter of b₁ st
( b₄ in F_primeSet b₁ & not b₃ in b₄ & b₂ in b₄ )

proof end;

theorem Th23: :: OPENLATT:23

for b₁ being D_Lattice
for b₂, b₃ being Element of b₁ st b₂ <> b₃ holds
ex b₄ being Filter of b₁ st b₄ in F_primeSet b₁

proof end;

theorem Th24: :: OPENLATT:24

for b₁ being D_Lattice
for b₂, b₃ being Element of b₁ st b₂ <> b₃ holds
(StoneH b₁) . b₂ <> (StoneH b₁) . b₃

proof end;

theorem Th25: :: OPENLATT:25

for b₁ being D_Lattice holds StoneH b₁ is one-to-one

proof end;

definition

let c₁ be D_Lattice;
let c₂, c₃ be Element of StoneS c₁;
redefine func \/ as c₂ \/ c₃ -> Element of StoneS a₁;
coherence

proof end;

redefine func /\ as c₂ /\ c₃ -> Element of StoneS a₁;
coherence

proof end;

end;

definition

let c₁ be D_Lattice;
func Set_Union c₁ -> BinOp of StoneS a₁ means :Def9: :: OPENLATT:def 9
for b₁, b₂ being Element of StoneS a₁ holds a₂ . b₁,b₂ = b₁ \/ b₂;
existence

proof end;

uniqueness

proof end;

func Set_Meet c₁ -> BinOp of StoneS a₁ means :Def10: :: OPENLATT:def 10
for b₁, b₂ being Element of StoneS a₁ holds a₂ . b₁,b₂ = b₁ /\ b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines Set_Union OPENLATT:def 9 :

:: deftheorem Def10 defines Set_Meet OPENLATT:def 10 :

Lemma33: for b₁ being D_Lattice
for b₂, b₃ being Element of LattStr(# (StoneS b₁),(Set_Union b₁),(Set_Meet b₁) #) holds b₂ "\/" b₃ = b₂ \/ b₃
by Def9;

Lemma34: for b₁ being D_Lattice
for b₂, b₃ being Element of LattStr(# (StoneS b₁),(Set_Union b₁),(Set_Meet b₁) #) holds b₂ "/\" b₃ = b₂ /\ b₃
by Def10;

theorem Th26: :: OPENLATT:26

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

proof end;

definition

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

end;

:: deftheorem Def11 defines StoneLatt OPENLATT:def 11 :

theorem Th27: :: OPENLATT:27

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

theorem Th28: :: OPENLATT:28

for b₁ being D_Lattice
for b₂, b₃ being Element of (StoneLatt b₁) holds
( b₂ "\/" b₃ = b₂ \/ b₃ & b₂ "/\" b₃ = b₂ /\ b₃ ) by Lemma33, Lemma34;

theorem Th29: :: OPENLATT:29

for b₁ being D_Lattice
for b₂, b₃ being Element of (StoneLatt b₁) holds
( b₂ [= b₃ iff b₂ c= b₃ )

proof end;

definition

let c₁ be D_Lattice;
redefine func StoneH as StoneH c₁ -> Homomorphism of a₁, StoneLatt a₁;
coherence

proof end;

end;

theorem Th30: :: OPENLATT:30

for b₁ being D_Lattice holds StoneH b₁ is isomorphism

proof end;

theorem Th31: :: OPENLATT:31

for b₁ being D_Lattice holds StoneLatt b₁ is distributive

proof end;

theorem Th32: :: OPENLATT:32

for b₁ being D_Lattice holds b₁, StoneLatt b₁ are_isomorphic

proof end;

registration

cluster upper-bounded non trivial LattStr ;
existence

proof end;

end;

theorem Th33: :: OPENLATT:33

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

proof end;

theorem Th34: :: OPENLATT:34

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

proof end;

theorem Th35: :: OPENLATT:35

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

proof end;

registration

let c₁ be non trivial H_Lattice;
cluster F_primeSet a₁ -> non empty ;
coherence

proof end;

end;

definition

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

proof end;

uniqueness ;

end;

:: deftheorem Def12 defines HTopSpace OPENLATT:def 12 :

registration

let c₁ be non trivial H_Lattice;
cluster HTopSpace a₁ -> non empty strict TopSpace-like ;
coherence

proof end;

end;

theorem Th36: :: OPENLATT:36

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

theorem Th37: :: OPENLATT:37

for b₁ being non trivial H_Lattice holds StoneS b₁ c= the carrier of (Open_setLatt (HTopSpace b₁))

proof end;

definition

let c₁ be non trivial H_Lattice;
redefine func StoneH as StoneH c₁ -> Homomorphism of a₁, Open_setLatt (HTopSpace a₁);
coherence

proof end;

end;

theorem Th38: :: OPENLATT:38

for b₁ being non trivial H_Lattice holds StoneH b₁ is monomorphism

proof end;

theorem Th39: :: OPENLATT:39

for b₁ being non trivial H_Lattice
for b₂, b₃ being Element of b₁ holds (StoneH b₁) . (b₂ => b₃) = ((StoneH b₁) . b₂) => ((StoneH b₁) . b₃)

proof end;

theorem Th40: :: OPENLATT:40

for b₁ being non trivial H_Lattice holds StoneH b₁ preserves_implication

proof end;

theorem Th41: :: OPENLATT:41

for b₁ being non trivial H_Lattice holds StoneH b₁ preserves_top

proof end;

theorem Th42: :: OPENLATT:42

for b₁ being non trivial H_Lattice holds StoneH b₁ preserves_bottom

proof end;