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


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
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 b1 being BinOp of (Topology_of T) st
for P, Q being Element of Topology_of T holds b1 . (P,Q) = P \/ Q
proof end;
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
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 b1 being BinOp of (Topology_of T) st
for P, Q being Element of Topology_of T holds b1 . (P,Q) = P /\ Q
proof end;
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
proof end;
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
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 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 )
proof end;

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

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

theorem Th8: :: OPENLATT:8
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 Th9: :: OPENLATT:9
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 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 & 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 b1 being Function st
for a being Element of L holds
( dom b1 = the carrier of L & b1 . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } )
proof end;
uniqueness
for b1, b2 being Function st ( for a being Element of L holds
( dom b1 = the carrier of L & b1 . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } ) ) & ( for a being Element of L holds
( dom b2 = the carrier of L & b2 . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } ) ) holds
b1 = b2
proof end;
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 & b2 . a = { F where F is Filter of L : ( F in F_primeSet L & 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 & a in F ) )
proof end;

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 & 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 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 )
proof end;

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

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)
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 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 & a in x ) )
proof end;

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

theorem Th17: :: OPENLATT:17
for L being D_Lattice
for a, b 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 Th18: :: OPENLATT:18
for L being D_Lattice
for a, b 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 Th19: :: OPENLATT:19
for L being D_Lattice
for a, b being Element of L st not b [= a holds
<.b.) in (SF_have b) \ (SF_have a)
proof end;

theorem Th20: :: OPENLATT:20
for L being D_Lattice
for a, b 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 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
proof end;

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

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 b1 being BinOp of (StoneS L) st
for A, B being Element of StoneS L holds b1 . (A,B) = A \/ B
proof end;
uniqueness
for b1, b2 being BinOp of (StoneS L) st ( for A, B being Element of StoneS L holds b1 . (A,B) = A \/ B ) & ( for A, B being Element of StoneS L holds b2 . (A,B) = A \/ B ) holds
b1 = b2
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 b1 being BinOp of (StoneS L) st
for A, B being Element of StoneS L holds b1 . (A,B) = A /\ B
proof end;
uniqueness
for b1, b2 being BinOp of (StoneS L) st ( for A, B being Element of StoneS L holds b1 . (A,B) = A /\ B ) & ( for A, B being Element of StoneS L holds b2 . (A,B) = A /\ B ) holds
b1 = b2
proof end;
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
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 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 & 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 )
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;

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
proof end;
cluster StoneLatt L -> distributive ;
coherence
StoneLatt L is distributive
proof end;
end;

theorem :: OPENLATT:27
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 V93() Heyting implicative for LattStr ;
existence
not for b1 being H_Lattice holds b1 is trivial
proof end;
end;

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

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

theorem Th30: :: OPENLATT:30
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 b1 being strict TopStruct st
( the carrier of b1 = F_primeSet H & the topology of b1 = { (union A) where A is Subset of (StoneS H) : verum } )
proof end;
uniqueness
for b1, b2 being strict TopStruct st the carrier of b1 = F_primeSet H & the topology of b1 = { (union A) where A is Subset of (StoneS H) : verum } & the carrier of b2 = F_primeSet H & 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 & 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 & HTopSpace H is TopSpace-like )
proof end;
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))
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 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)
proof end;

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

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

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