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


begin

registration
cluster non empty Lattice-like lower-bounded Heyting  ->  implicative for LattStr ;
coherence
 for b1 being 0_Lattice st b1 is Heyting holds
b1 is implicative ;
cluster non empty Lattice-like implicative  ->  upper-bounded for LattStr ;
coherence
 for b1 being Lattice st b1 is implicative holds
b1 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
proofend;

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)
proofend;

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 funcP \/ Q ->  Element of Topology_of T;
coherence
 P \/ Q is Element of Topology_of T
proofend;
:: original:/\
redefine funcP /\ Q ->  Element of Topology_of T;
coherence
 P /\ Q is Element of Topology_of T
proofend;
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 b1 being BinOp of (Topology_of T) st
for P, Q being Element of Topology_of T holds b1 . (P,Q) = P \/ Q
proofend;
uniqueness
 for b1, b2 being BinOp of (Topology_of T) st ( for P, Q being Element of Topology_of T holds b1 . (P,Q) = P \/ Q ) & ( for P, Q being Element of Topology_of T holds b2 . (P,Q) = P \/ Q ) holds
b1 = b2
proofend;
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 b1 being BinOp of (Topology_of T) st
for P, Q being Element of Topology_of T holds b1 . (P,Q) = P /\ Q
proofend;
uniqueness
 for b1, b2 being BinOp of (Topology_of T) st ( for P, Q being Element of Topology_of T holds b1 . (P,Q) = P /\ Q ) & ( for P, Q being Element of Topology_of T holds b2 . (P,Q) = P /\ Q ) holds
b1 = b2
proofend;
end;

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

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

theorem Th3: :: OPENLATT:3
for T being non empty TopSpace holds LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is Lattice
proofend;

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 Th3;
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:4
for T being non empty TopSpace holds the carrier of (Open_setLatt T) = Topology_of T ;

theorem :: OPENLATT:5
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 Th6: :: OPENLATT:6
for T being non empty TopSpace
for p, q being Element of (Open_setLatt T) holds
( p [= q iff p c= q )
proofend;

theorem Th7: :: OPENLATT:7
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 )
proofend;

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

theorem Th8: :: OPENLATT:8
for T being non empty TopSpace holds
( Open_setLatt T is lower-bounded & Bottom (Open_setLatt T) = {} )
proofend;

registration
let T be non empty TopSpace;
cluster Open_setLatt T ->  Heyting ;
coherence
 Open_setLatt T is Heyting
proofend;
end;

theorem Th9: :: OPENLATT:9
for T being non empty TopSpace holds Top (Open_setLatt T) = the carrier of T
proofend;

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

theorem Th10: :: OPENLATT:10
for L being D_Lattice
for F being Filter of L holds
( F in F_primeSet L iff ( F <> the carrier of L &amp; F is prime ) )
proofend;

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 &amp; it . a =  {  F where F is Filter of L : ( F in F_primeSet L &amp; a in F )  }  );
existence
 ex b1 being Function st
for a being Element of L holds
( dom b1 = the carrier of L &amp; b1 . a =  {  F where F is Filter of L : ( F in F_primeSet L &amp; a in F )  }  )
proofend;
uniqueness
 for b1, b2 being Function st ( for a being Element of L holds
( dom b1 = the carrier of L &amp; b1 . a =  {  F where F is Filter of L : ( F in F_primeSet L &amp; a in F )  }  ) ) &amp; ( for a being Element of L holds
( dom b2 = the carrier of L &amp; b2 . a =  {  F where F is Filter of L : ( F in F_primeSet L &amp; a in F )  }  ) ) holds
b1 = b2
proofend;
end;

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

theorem Th11: :: OPENLATT:11
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 &amp; a in F ) )
proofend;

theorem Th12: :: OPENLATT:12
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 &amp; F <> the carrier of L &amp; F is prime &amp; a in F ) )
proofend;

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
proofend;
end;

theorem Th13: :: OPENLATT:13
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 )
proofend;

theorem Th14: :: OPENLATT:14
for L being D_Lattice
for a, b being Element of L holds (StoneH L) . (a "\/" b) = ((StoneH L) . a) \/ ((StoneH L) . b)
proofend;

theorem Th15: :: OPENLATT:15
for L being D_Lattice
for a, b being Element of L holds (StoneH L) . (a "/\" b) = ((StoneH L) . a) /\ ((StoneH L) . b)
proofend;

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
proofend;
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
proofend;
end;

theorem Th16: :: OPENLATT:16
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 &amp; a in x ) )
proofend;

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 &amp; not a in F ) )
proofend;

theorem Th17: :: OPENLATT:17
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 &amp; b in x &amp; not a in x )
proofend;

theorem Th18: :: OPENLATT:18
for L being D_Lattice
for b, a being Element of L
for Z being set st Z <> {} &amp; Z c= (SF_have b) \ (SF_have a) &amp; Z is c=-linear holds
ex Y being set st
( Y in (SF_have b) \ (SF_have a) &amp; ( for X1 being set st X1 in Z holds
X1 c= Y ) )
proofend;

theorem Th19: :: OPENLATT:19
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)
proofend;

theorem Th20: :: OPENLATT:20
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 &amp; not a in F &amp; b in F )
proofend;

theorem Th21: :: OPENLATT:21
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
proofend;

theorem Th22: :: OPENLATT:22
for L being D_Lattice
for a, b being Element of L st a <> b holds
(StoneH L) . a <> (StoneH L) . b
proofend;

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

definition
let L be D_Lattice;
let A, B be Element of StoneS L;
:: original:\/
redefine funcA \/ B ->  Element of StoneS L;
coherence
 A \/ B is Element of StoneS L
proofend;
:: original:/\
redefine funcA /\ B ->  Element of StoneS L;
coherence
 A /\ B is Element of StoneS L
proofend;
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 b1 being BinOp of (StoneS L) st
for A, B being Element of StoneS L holds b1 . (A,B) = A \/ B
proofend;
uniqueness
 for b1, b2 being BinOp of (StoneS L) st ( for A, B being Element of StoneS L holds b1 . (A,B) = A \/ B ) &amp; ( for A, B being Element of StoneS L holds b2 . (A,B) = A \/ B ) holds
b1 = b2
proofend;
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 b1 being BinOp of (StoneS L) st
for A, B being Element of StoneS L holds b1 . (A,B) = A /\ B
proofend;
uniqueness
 for b1, b2 being BinOp of (StoneS L) st ( for A, B being Element of StoneS L holds b1 . (A,B) = A /\ B ) &amp; ( for A, B being Element of StoneS L holds b2 . (A,B) = A /\ B ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines Set_Union OPENLATT:def_9_:_
 for L being D_Lattice
for b2 being BinOp of (StoneS L) holds
( b2 = Set_Union L iff for A, B being Element of StoneS L holds b2 . (A,B) = A \/ B );

:: deftheorem Def10 defines Set_Meet OPENLATT:def_10_:_
 for L being D_Lattice
for b2 being BinOp of (StoneS L) holds
( b2 = Set_Meet L iff for A, B being Element of StoneS L holds b2 . (A,B) = A /\ B );

theorem Th23: :: OPENLATT:23
for L being D_Lattice holds LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is Lattice
proofend;

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 Th23;
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:24
for L being D_Lattice holds the carrier of (StoneLatt L) = StoneS L ;

theorem :: OPENLATT:25
for L being D_Lattice
for p, q being Element of (StoneLatt L) holds
( p "\/" q = p \/ q &amp; p "/\" q = p /\ q ) by Def9, Def10;

theorem :: OPENLATT:26
for L being D_Lattice
for p, q being Element of (StoneLatt L) holds
( p [= q iff p c= q )
proofend;

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
proofend;
end;

registration
let L be D_Lattice;
cluster StoneH L ->  bijective for Function of L,(StoneLatt L);
coherence
 for b1 being Function of L,(StoneLatt L) st b1 = StoneH L holds
b1 is bijective
proofend;
cluster StoneLatt L ->  distributive ;
coherence
 StoneLatt L is distributive
proofend;
end;

theorem :: OPENLATT:27
for L being D_Lattice holds L, StoneLatt L are_isomorphic
proofend;

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 ;
existence
 not for b1 being H_Lattice holds b1 is trivial
proofend;
end;

theorem Th28: :: OPENLATT:28
for H being non trivial H_Lattice holds (StoneH H) . (Top H) = F_primeSet H
proofend;

theorem Th29: :: OPENLATT:29
for H being non trivial H_Lattice holds (StoneH H) . (Bottom H) = {}
proofend;

theorem Th30: :: OPENLATT:30
for H being non trivial H_Lattice holds StoneS H c= bool (F_primeSet H)
proofend;

registration
let H be non trivial H_Lattice;
cluster F_primeSet H ->  non empty ;
coherence
 not F_primeSet H is empty
proofend;
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 &amp; the topology of it =  {  (union A) where A is Subset of (StoneS H) : verum  }  );
existence
 ex b1 being strict TopStruct st
( the carrier of b1 = F_primeSet H &amp; the topology of b1 =  {  (union A) where A is Subset of (StoneS H) : verum  }  )
proofend;
uniqueness
 for b1, b2 being strict TopStruct st the carrier of b1 = F_primeSet H &amp; the topology of b1 =  {  (union A) where A is Subset of (StoneS H) : verum  }  &amp; the carrier of b2 = F_primeSet H &amp; the topology of b2 =  {  (union A) where A is Subset of (StoneS H) : verum  }  holds
b1 = b2 ;
end;

:: deftheorem Def12 defines HTopSpace OPENLATT:def_12_:_
 for H being non trivial H_Lattice
for b2 being strict TopStruct holds
( b2 = HTopSpace H iff ( the carrier of b2 = F_primeSet H &amp; the topology of b2 =  {  (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 &amp; HTopSpace H is TopSpace-like )
proofend;
end;

theorem :: OPENLATT:31
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 Th32: :: OPENLATT:32
for H being non trivial H_Lattice holds StoneS H c= the carrier of (Open_setLatt (HTopSpace H))
proofend;

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)
proofend;
end;

theorem Th33: :: OPENLATT:33
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)
proofend;

theorem :: OPENLATT:34
for H being non trivial H_Lattice holds StoneH H preserves_implication
proofend;

theorem :: OPENLATT:35
for H being non trivial H_Lattice holds StoneH H preserves_top
proofend;

theorem :: OPENLATT:36
for H being non trivial H_Lattice holds StoneH H preserves_bottom
proofend;