:: Representation Theorem for Heyting Lattices
:: by Jolanta Kamie\'nska
::
:: Received July 14, 1993
:: Copyright (c) 1993-2011 Association of Mizar Users

begin

registration

cluster non empty Lattice-like lower-bounded Heyting -> implicative LattStr ;
coherence
for b₁ being 0_Lattice st b₁ is Heyting holds
b₁ is implicative ;
cluster non empty Lattice-like implicative -> upper-bounded LattStr ;
coherence
for b₁ being Lattice st b₁ is implicative holds
b₁ is upper-bounded ;

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
the topology of T is Subset-Family of T ;

end;

:: deftheorem defines Topology_of OPENLATT:def 1 :
for T being TopStruct holds Topology_of T = the topology of T;

registration

let T be TopSpace;
cluster Topology_of T -> non empty ;
coherence
not Topology_of T is empty ;

end;

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
P \/ Q is Element of Topology_of T

proof end;

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

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
ex b₁ being BinOp of (Topology_of T) st
for P, Q being Element of Topology_of T holds b₁ . (P,Q) = P \/ Q

proof end;

uniqueness
for b₁, b₂ being BinOp of (Topology_of T) st ( for P, Q being Element of Topology_of T holds b₁ . (P,Q) = P \/ Q ) & ( for P, Q being Element of Topology_of T holds b₂ . (P,Q) = P \/ Q ) holds
b₁ = b₂

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
ex b₁ being BinOp of (Topology_of T) st
for P, Q being Element of Topology_of T holds b₁ . (P,Q) = P /\ Q

proof end;

uniqueness
for b₁, b₂ being BinOp of (Topology_of T) st ( for P, Q being Element of Topology_of T holds b₁ . (P,Q) = P /\ Q ) & ( for P, Q being Element of Topology_of T holds b₂ . (P,Q) = P /\ Q ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines Top_Union OPENLATT:def 2 :
for T being non empty TopSpace
for b₂ being BinOp of (Topology_of T) holds
( b₂ = Top_Union T iff for P, Q being Element of Topology_of T holds b₂ . (P,Q) = P \/ Q );

:: deftheorem Def3 defines Top_Meet OPENLATT:def 3 :
for T being non empty TopSpace
for b₂ being BinOp of (Topology_of T) holds
( b₂ = Top_Meet T iff for P, Q being Element of Topology_of T holds b₂ . (P,Q) = P /\ Q );

theorem :: OPENLATT:3

canceled;

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
LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is Lattice by Th4;

end;

:: deftheorem defines Open_setLatt OPENLATT:def 4 :
for T being non empty TopSpace holds Open_setLatt T = LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #);

theorem :: OPENLATT:5

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

theorem :: 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 p9, q9 being Element of Topology_of T st p = p9 & q = q9 holds
( p [= q iff p9 c= q9 )

proof end;

theorem :: OPENLATT:9

canceled;

registration

let T be non empty TopSpace;
cluster Open_setLatt T -> implicative ;
coherence
Open_setLatt T is implicative

proof end;

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 -> Heyting ;
coherence
Open_setLatt T is Heyting

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
{ F where F is Filter of L : ( F <> the carrier of L & F is prime ) } is set ;

end;

:: deftheorem defines F_primeSet OPENLATT:def 5 :
for L being D_Lattice holds F_primeSet L = { F where F is Filter of L : ( F <> the carrier of L & F is prime ) } ;

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
ex b₁ being Function st
for a being Element of L holds
( dom b₁ = the carrier of L & b₁ . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } )

proof end;

uniqueness
for b₁, b₂ being Function st ( for a being Element of L holds
( dom b₁ = the carrier of L & b₁ . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } ) ) & ( for a being Element of L holds
( dom b₂ = the carrier of L & b₂ . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines StoneH OPENLATT:def 6 :
for L being D_Lattice
for b₂ being Function holds
( b₂ = StoneH L iff for a being Element of L holds
( dom b₂ = the carrier of L & b₂ . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } ) );

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
rng (StoneH L) is set ;

end;

:: deftheorem defines StoneS OPENLATT:def 7 :
for L being D_Lattice holds StoneS L = rng (StoneH L);

registration

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

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
{ F where F is Filter of L : a in F } is Subset-Family of L

proof end;

end;

:: deftheorem defines SF_have OPENLATT:def 8 :
for L being D_Lattice
for a being Element of L holds SF_have a = { F where F is Filter of L : a in F } ;

registration

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

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;

Lm1: 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 :: OPENLATT:25

canceled;

registration

let L be D_Lattice;
cluster StoneH L -> one-to-one ;
coherence
StoneH L is one-to-one

proof end;

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
A \/ B is Element of StoneS L

proof end;

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

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
ex b₁ being BinOp of (StoneS L) st
for A, B being Element of StoneS L holds b₁ . (A,B) = A \/ B

proof end;

uniqueness
for b₁, b₂ being BinOp of (StoneS L) st ( for A, B being Element of StoneS L holds b₁ . (A,B) = A \/ B ) & ( for A, B being Element of StoneS L holds b₂ . (A,B) = A \/ B ) holds
b₁ = b₂

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
ex b₁ being BinOp of (StoneS L) st
for A, B being Element of StoneS L holds b₁ . (A,B) = A /\ B

proof end;

uniqueness
for b₁, b₂ being BinOp of (StoneS L) st ( for A, B being Element of StoneS L holds b₁ . (A,B) = A /\ B ) & ( for A, B being Element of StoneS L holds b₂ . (A,B) = A /\ B ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines Set_Union OPENLATT:def 9 :
for L being D_Lattice
for b₂ being BinOp of (StoneS L) holds
( b₂ = Set_Union L iff for A, B being Element of StoneS L holds b₂ . (A,B) = A \/ B );

:: deftheorem Def10 defines Set_Meet OPENLATT:def 10 :
for L being D_Lattice
for b₂ being BinOp of (StoneS L) holds
( b₂ = Set_Meet L iff for A, B being Element of StoneS L holds b₂ . (A,B) = A /\ B );

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
LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is Lattice by Th26;

end;

:: deftheorem defines StoneLatt OPENLATT:def 11 :
for L being D_Lattice holds StoneLatt L = LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #);

theorem :: OPENLATT:27

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

theorem :: 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 Def9, Def10;

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
StoneH L is Homomorphism of L, StoneLatt L

proof end;

end;

theorem :: OPENLATT:30

canceled;

theorem :: OPENLATT:31

canceled;

registration

let L be D_Lattice;
cluster StoneH L -> bijective Function of L,(StoneLatt L);
coherence
for b₁ being Function of L,(StoneLatt L) st b₁ = StoneH L holds
b₁ is bijective

proof end;

cluster StoneLatt L -> distributive ;
coherence
StoneLatt L is distributive

proof end;

end;

theorem :: OPENLATT:32

for L being D_Lattice holds L, StoneLatt L are_isomorphic

proof end;

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 LattStr ;
existence
not for b₁ being H_Lattice holds b₁ is trivial

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
not F_primeSet H is empty

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
ex b₁ being strict TopStruct st
( the carrier of b₁ = F_primeSet H & the topology of b₁ = { (union A) where A is Subset of (StoneS H) : verum } )

proof end;

uniqueness
for b₁, b₂ being strict TopStruct st the carrier of b₁ = F_primeSet H & the topology of b₁ = { (union A) where A is Subset of (StoneS H) : verum } & the carrier of b₂ = F_primeSet H & the topology of b₂ = { (union A) where A is Subset of (StoneS H) : verum } holds
b₁ = b₂ ;

end;

:: deftheorem Def12 defines HTopSpace OPENLATT:def 12 :
for H being non trivial H_Lattice
for b₂ being strict TopStruct holds
( b₂ = HTopSpace H iff ( the carrier of b₂ = F_primeSet H & the topology of b₂ = { (union A) where A is Subset of (StoneS H) : verum } ) );

registration

let H be non trivial H_Lattice;
cluster HTopSpace H -> non empty strict TopSpace-like ;
coherence
( not HTopSpace H is empty & HTopSpace H is TopSpace-like )

proof end;

end;

theorem :: 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

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

proof end;

definition

let H be non trivial H_Lattice;
:: original: StoneH
redefine func StoneH H -> Homomorphism of H, Open_setLatt (HTopSpace H);
coherence
StoneH H is Homomorphism of H, Open_setLatt (HTopSpace H)

proof end;

end;

theorem :: OPENLATT:38

canceled;

theorem Th39: :: OPENLATT:39

for H being non trivial H_Lattice
for p9, q9 being Element of H holds (StoneH H) . (p9 => q9) = ((StoneH H) . p9) => ((StoneH H) . q9)

proof end;

theorem :: OPENLATT:40

for H being non trivial H_Lattice holds StoneH H preserves_implication

proof end;

theorem :: OPENLATT:41

for H being non trivial H_Lattice holds StoneH H preserves_top

proof end;

theorem :: OPENLATT:42

for H being non trivial H_Lattice holds StoneH H preserves_bottom

proof end;