:: Representation Theorem for Heyting Lattices
:: by Jolanta Kamie\'nska
::
:: Received July 14, 1993
:: Copyright (c) 1993-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies LATTICE2, FILTER_0, LATTICES, PRE_TOPC, SUBSET_1, XBOOLE_0,
TOPS_1, TARSKI, RCOMP_1, SETFAM_1, BINOP_1, FUNCT_1, EQREL_1, STRUCT_0,
PBOOLE, CARD_FIL, INT_2, RELAT_1, ZFMISC_1, ORDINAL1, GROUP_6, FUNCT_2,
WELLORD1, XBOOLEAN, LATTICE4, OPENLATT;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, RELAT_1, FUNCT_1, FUNCT_2,
BINOP_1, SETFAM_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1, LATTICES,
LATTICE2, FILTER_0, LATTICE4;
constructors BINOP_1, DOMAIN_1, TOPS_1, LATTICE2, FILTER_1, LATTICE4,
RELSET_1, FILTER_0;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, LATTICES, PRE_TOPC,
FILTER_0, LATTICE2, TOPS_1;
requirements BOOLE, SUBSET;
definitions TARSKI, PRE_TOPC, FILTER_0, LATTICES, LATTICE4, FUNCT_1, STRUCT_0,
XBOOLE_0, FUNCT_2;
equalities FILTER_0, LATTICES, STRUCT_0, SUBSET_1;
expansions TARSKI, PRE_TOPC, FILTER_0, LATTICES, LATTICE4, FUNCT_1, XBOOLE_0,
FUNCT_2;
theorems PRE_TOPC, LATTICES, TOPS_1, ZFMISC_1, FILTER_0, SETFAM_1, TARSKI,
FUNCT_1, FUNCT_2, LATTICE4, RELAT_1, ORDINAL1, XBOOLE_0, XBOOLE_1,
STRUCT_0, EQREL_1;
schemes BINOP_1, DOMAIN_1, FUNCT_1, BINOP_2;
begin
registration
cluster Heyting -> implicative for 0_Lattice;
coherence;
cluster implicative -> upper-bounded for Lattice;
coherence;
end;
reserve T for TopSpace;
reserve A,B for Subset of T;
theorem Th1:
A /\ Int(A` \/ B) c= B
proof
A1: A misses A` by XBOOLE_1:79;
A /\ (A` \/ B) = (A /\ A`) \/ A /\ B by XBOOLE_1:23
.= {} \/ A /\ B by A1
.= A /\ B;
then
A2: A /\ (A` \/ B)c= B by XBOOLE_1:17;
A /\ Int(A` \/ B) c= A /\ (A` \/ B) by TOPS_1:16,XBOOLE_1:26;
hence thesis by A2;
end;
theorem Th2:
for C being Subset of T st C is open & A /\ C c= B holds C c= Int (A` \/ B)
proof
let C be Subset of T;
assume that
A1: C is open and
A2: A /\ C c= B;
A3: C c= C \/ A` by XBOOLE_1:7;
(A /\ C) \/ A` = (A \/ A`) /\ (C \/ A`) by XBOOLE_1:24
.= [#] T /\ (C \/ A`) by PRE_TOPC:2
.= C \/ A` by XBOOLE_1:28;
then C \/ A` c= B \/ A` by A2,XBOOLE_1:9;
then C c= B \/ A` by A3;
then Int(C) c= Int(A` \/ B) by TOPS_1:19;
hence thesis by A1,TOPS_1:23;
end;
definition
let T be TopStruct;
func Topology_of T -> Subset-Family of T equals
the topology of T;
coherence;
end;
registration
let T;
cluster Topology_of T -> non empty;
coherence;
end;
definition
let T be non empty TopSpace, P, Q be Element of Topology_of T;
redefine func P \/ Q -> Element of Topology_of T;
coherence
proof
reconsider A = P, B = Q as Subset of T;
A1: B is open;
A is open;
then P \/ Q is open by A1;
hence thesis;
end;
redefine func P /\ Q -> Element of Topology_of T;
coherence
proof
reconsider A = P, B = Q as Subset of T;
A2: B is open;
A is open;
then P /\ Q is open by A2;
hence thesis;
end;
end;
reserve T for non empty TopSpace;
reserve P,Q for Element of Topology_of T;
definition
let T;
func Top_Union T -> BinOp of Topology_of T means
:Def2:
it.(P,Q) = P \/ Q;
existence
proof
deffunc F(Element of Topology_of T, Element of Topology_of T) = $1 \/ $2;
thus ex F being BinOp of Topology_of T st for P,Q being Element of
Topology_of T holds F.(P,Q) = F(P,Q) from BINOP_1:sch 4;
end;
uniqueness
proof
set A = Topology_of T;
deffunc O(Element of A, Element of A) = $1 \/ $2;
thus for o1,o2 being BinOp of A st (for a,b being Element of A holds o1.(a
,b) = O(a,b)) & (for a,b being Element of A holds o2.(a,b) = O(a,b)) holds o1 =
o2 from BINOP_2:sch 2;
end;
func Top_Meet T -> BinOp of Topology_of T means
:Def3:
it.(P,Q) = P /\ Q;
existence
proof
deffunc F(Element of Topology_of T, Element of Topology_of T) = $1 /\ $2;
thus ex F being BinOp of Topology_of T st for P,Q being Element of
Topology_of T holds F.(P,Q) = F(P,Q) from BINOP_1:sch 4;
end;
uniqueness
proof
set A = Topology_of T;
deffunc O(Element of A, Element of A) = $1 /\ $2;
thus for o1,o2 being BinOp of A st (for a,b being Element of A holds o1.(a
,b) = O(a,b)) & (for a,b being Element of A holds o2.(a,b) = O(a,b)) holds o1 =
o2 from BINOP_2:sch 2;
end;
end;
theorem Th3:
for T being non empty TopSpace holds LattStr(#Topology_of T,
Top_Union T,Top_Meet T#) is Lattice
proof
let T;
set L = LattStr(#Topology_of T,Top_Union T,Top_Meet T#);
A1: now
let p,q be Element of L;
thus p "\/" q = q \/ p by Def2
.= q"\/"p by Def2;
end;
A2: now
let p,q be Element of L;
thus (p"/\"q)"\/"q = p"/\"q \/ q by Def2
.= (p /\ q) \/ q by Def3
.= q by XBOOLE_1:22;
end;
A3: now
let p,q be Element of L;
thus p"/\"(p"\/"q) = p /\ (p"\/"q) by Def3
.= p /\ (p \/ q) by Def2
.= p by XBOOLE_1:21;
end;
A4: now
let p,q,r be Element of L;
thus p"/\"(q"/\"r) = p /\ (q "/\" r) by Def3
.= p /\ (q /\ r) by Def3
.= (p /\ q) /\ r by XBOOLE_1:16
.= p "/\" q /\ r by Def3
.= (p"/\"q)"/\"r by Def3;
end;
A5: now
let p,q be Element of L;
thus p "/\" q =q /\ p by Def3
.= q"/\"p by Def3;
end;
now
let p,q,r be Element of L;
thus p"\/"(q"\/"r) = p \/ q "\/" r by Def2
.= p \/ (q \/ r) by Def2
.= (p \/ q) \/ r by XBOOLE_1:4
.= p "\/" q \/ r by Def2
.= (p"\/"q)"\/"r by Def2;
end;
then L is join-commutative join-associative meet-absorbing meet-commutative
meet-associative join-absorbing by A1,A2,A5,A4,A3;
hence thesis;
end;
definition
let T;
func Open_setLatt(T) -> Lattice equals
LattStr(#Topology_of T,Top_Union T,
Top_Meet T#);
coherence by Th3;
end;
theorem
the carrier of Open_setLatt(T) = Topology_of T;
reserve p,q for Element of Open_setLatt(T);
theorem
p "\/" q = p \/ q & p "/\" q = p /\ q by Def2,Def3;
theorem Th6:
p [= q iff p c= q
proof
p "\/" q = p \/ q by Def2;
hence thesis by XBOOLE_1:7,12;
end;
theorem Th7:
for p9,q9 being Element of Topology_of T st p=p9 & q=q9 holds p
[= q iff p9 c= q9
proof
let p9,q9 be Element of Topology_of T such that
A1: p=p9 and
A2: q=q9;
hereby
assume
A3: p [= q;
p9 \/ q9 = p"\/"q by A1,A2,Def2
.= q9 by A2,A3;
hence p9 c= q9 by XBOOLE_1:7;
end;
assume
A4: p9 c= q9;
p "\/" q = p9 \/ q9 by A1,A2,Def2
.=q by A2,A4,XBOOLE_1:12;
hence thesis;
end;
registration
let T;
cluster Open_setLatt(T) -> implicative;
coherence
proof
set OL=Open_setLatt(T);
let p,q be Element of OL;
reconsider p9=p, q9=q as Element of Topology_of T;
reconsider r9= Int(p9` \/ q9) as Element of Topology_of T by PRE_TOPC:def 2;
reconsider r=r9 as Element of OL;
take r;
A1: p "/\" r = p9 /\ r9 by Def3;
p9 /\ r c= q9 by Th1;
hence p "/\" r [= q by A1,Th7;
let r1 be Element of OL;
reconsider r2 = r1 as Element of Topology_of T;
reconsider r19= r2 as Subset of T;
A2: r19 is open;
assume
A3: p "/\" r1 [= q;
p "/\" r1 = p9 /\ r19 by Def3;
then p9 /\ r2 c= q9 by A3,Th7;
then r19 c= r9 by A2,Th2;
hence r1 [= r by Th7;
end;
end;
theorem Th8:
Open_setLatt(T) is lower-bounded & Bottom Open_setLatt(T) = {}
proof
set OL=Open_setLatt(T);
reconsider r = {} as Element of OL by PRE_TOPC:1;
A1: now
let p;
thus r"/\"p = r /\ p by Def3
.= r;
hence p"/\"r=r;
end;
thus OL is lower-bounded
by A1;
hence thesis by A1,LATTICES:def 16;
end;
registration
let T;
cluster Open_setLatt(T) -> Heyting;
coherence
proof
reconsider OL=Open_setLatt(T) as 0_Lattice by Th8;
OL is I_Lattice;
hence thesis;
end;
end;
theorem Th9:
Top Open_setLatt(T) = the carrier of T
proof
set OL=Open_setLatt(T);
reconsider B = the carrier of T as Element of OL by PRE_TOPC:def 1;
now
let p be Element of OL;
reconsider p9=p as Element of Topology_of T;
thus B"\/"p = (the carrier of T) \/ p9 by Def2
.= B by XBOOLE_1:12;
hence p"\/"B = B;
end;
hence thesis by LATTICES:def 17;
end;
reserve L for D_Lattice;
reserve F for Filter of L;
reserve a,b for Element of L;
reserve x,X,X1,X2,Y,Z for set;
definition
let L;
func F_primeSet(L) -> set equals
{ F: F <> the carrier of L & F is prime};
coherence;
end;
theorem Th10:
F in F_primeSet(L) iff F <> the carrier of L & F is prime
proof
F in F_primeSet(L) iff ex F0 being Filter of L st F0=F & F0 <> the
carrier of L & F0 is prime;
hence thesis;
end;
definition
let L;
func StoneH(L) -> Function means
:Def6:
dom it = the carrier of L & it.a = { F: F in F_primeSet(L) & a in F};
existence
proof
deffunc F(object) = { F :F in F_primeSet(L) & $1 in F};
consider f being Function such that
A1: dom f = the carrier of L &
for x being object st x in the carrier of L holds f.
x = F(x) from FUNCT_1:sch 3;
take f;
thus thesis by A1;
end;
uniqueness
proof
let f1,f2 be Function;
assume that
A2: dom f1 = the carrier of L & f1.a={ F :F in F_primeSet(L) & a in F} and
A3: dom f2 = the carrier of L & f2.a={ F :F in F_primeSet(L) & a in F};
now
let x be object;
assume x in the carrier of L;
then reconsider a=x as Element of L;
thus f1.x = { F :F in F_primeSet(L) & a in F} by A2
.= f2.x by A3;
end;
hence thesis by A2,A3;
end;
end;
theorem Th11:
F in StoneH(L).a iff F in F_primeSet(L) & a in F
proof
StoneH(L).a = {F0 where F0 is Filter of L: F0 in F_primeSet(L) & a in F0
} by Def6;
then
F in StoneH(L).a iff ex F0 being Filter of L st F=F0 & F0 in F_primeSet(
L) & a in F0;
hence thesis;
end;
theorem Th12:
x in StoneH(L).a iff ex F st F=x & F <> the carrier of L & F is
prime & a in F
proof
A1: StoneH(L).a = {F: F in F_primeSet(L) & a in F} by Def6;
hereby
assume x in StoneH(L).a;
then consider F such that
A2: x=F and
A3: F in F_primeSet(L) and
A4: a in F by A1;
A5: F is prime by A3,Th10;
F <> the carrier of L by A3,Th10;
hence ex F st F=x & F <> the carrier of L & F is prime & a in F by A2,A4,A5
;
end;
given F such that
A6: F=x and
A7: F <> the carrier of L and
A8: F is prime and
A9: a in F;
F in F_primeSet(L) by A7,A8;
hence thesis by A1,A6,A9;
end;
definition
let L;
func StoneS(L) -> set equals
rng StoneH(L);
coherence;
end;
registration
let L;
cluster StoneS(L) -> non empty;
coherence
proof
dom StoneH(L) = the carrier of L by Def6;
hence thesis by RELAT_1:42;
end;
end;
theorem Th13:
x in StoneS(L) iff ex a st x=StoneH(L).a
proof
hereby
assume x in StoneS(L);
then consider y be object such that
A1: y in dom StoneH(L) and
A2: x = StoneH(L).y by FUNCT_1:def 3;
reconsider y as Element of L by A1,Def6;
take y;
thus x=StoneH(L).y by A2;
end;
given b such that
A3: x=StoneH(L).b;
b in the carrier of L;
then b in dom StoneH(L) by Def6;
hence thesis by A3,FUNCT_1:def 3;
end;
theorem Th14:
StoneH(L).(a "\/" b) = StoneH(L).a \/ StoneH(L).b
proof
set c = a "\/" b;
hereby
set c = a "\/" b;
let x be object;
assume x in StoneH(L).c;
then consider F such that
A1: x=F and
A2: F <> the carrier of L and
A3: F is prime and
A4: c in F by Th12;
a in F or b in F by A3,A4;
then F in StoneH(L).a or F in StoneH(L).b by A2,A3,Th12;
hence x in StoneH(L).a \/ StoneH(L).b by A1,XBOOLE_0:def 3;
end;
let x be object;
assume x in StoneH(L).a \/ StoneH(L).b;
then x in StoneH(L).a or x in StoneH(L).b by XBOOLE_0:def 3;
then
(ex F st x=F & F <> the carrier of L & F is prime & a in F ) or ex F st
x=F & F <> the carrier of L & F is prime & b in F by Th12;
then consider F such that
A5: x=F and
A6: F <> the carrier of L and
A7: F is prime and
A8: a in F or b in F;
c in F by A7,A8;
hence thesis by A5,A6,A7,Th12;
end;
theorem Th15:
StoneH(L).(a "/\" b) = StoneH(L).a /\ StoneH(L).b
proof
set c = a "/\" b;
hereby
set c = a "/\" b;
let x be object;
assume x in StoneH(L).c;
then consider F such that
A1: x=F and
A2: F <> the carrier of L and
A3: F is prime and
A4: c in F by Th12;
b in F by A4,FILTER_0:8;
then
A5: F in StoneH(L).b by A2,A3,Th12;
a in F by A4,FILTER_0:8;
then F in StoneH(L).a by A2,A3,Th12;
hence x in StoneH(L).a /\ StoneH(L).b by A1,A5,XBOOLE_0:def 4;
end;
let x be object;
assume
A6: x in StoneH(L).a /\ StoneH(L).b;
then x in StoneH(L).b by XBOOLE_0:def 4;
then
A7: ex F st x=F & F <> the carrier of L & F is prime & b in F by Th12;
x in StoneH(L).a by A6,XBOOLE_0:def 4;
then ex F st x=F & F <> the carrier of L & F is prime & a in F by Th12;
then consider F such that
A8: x=F and
A9: F <> the carrier of L and
A10: F is prime and
A11: a in F and
A12: b in F by A7;
c in F by A11,A12,FILTER_0:8;
hence thesis by A8,A9,A10,Th12;
end;
definition
let L, a;
func SF_have a -> Subset-Family of L equals
{ F : a in F };
coherence
proof
set A= { F : a in F};
A c= bool the carrier of L
proof
let x be object;
assume x in A;
then ex F st x=F & a in F;
hence thesis;
end;
hence thesis;
end;
end;
registration
let L;
let a;
cluster SF_have a -> non empty;
coherence
proof
a in <.a.);
then <.a.) in { F : a in F};
hence thesis;
end;
end;
theorem Th16:
x in SF_have a iff x is Filter of L & a in x
proof
x in SF_have a iff ex F st F=x & a in F;
hence thesis;
end;
Lm1: F in SF_have b \ SF_have a iff b in F & not a in F
proof
F in SF_have b \ SF_have a iff F in SF_have b & not F in SF_have a by
XBOOLE_0:def 5;
hence thesis by Th16;
end;
theorem Th17:
x in SF_have b \ SF_have a implies x is Filter of L & b in x & not a in x
proof
assume
A1: x in SF_have b \ SF_have a;
then
A2: not x in SF_have a by XBOOLE_0:def 5;
A3: x in SF_have b by A1,XBOOLE_0:def 5;
then x is Filter of L by Th16;
hence thesis by A3,A2,Th16;
end;
theorem Th18:
for Z st Z <> {} & Z c= SF_have b \ SF_have a & Z is c=-linear
ex Y st Y in SF_have b \ SF_have a & for X1 st X1 in Z holds X1 c= Y
proof
let Z;
assume that
A1: Z <> {} and
A2: Z c= SF_have b \ SF_have a and
A3: Z is c=-linear;
reconsider Z as Subset-Family of L by A2,XBOOLE_1:1;
take Y = union Z;
Y in SF_have b \ SF_have a
proof
set X = the Element of Z;
A4: not a in Y
proof
assume a in Y;
then ex X st a in X & X in Z by TARSKI:def 4;
hence contradiction by A2,Th17;
end;
X in SF_have b \ SF_have a by A1,A2;
then
A5: b in X by Th17;
then
A6: b in Y by A1,TARSKI:def 4;
reconsider Y as non empty Subset of L by A1,A5,TARSKI:def 4;
now
let p,q be Element of L;
thus p in Y & q in Y implies p "/\" q in Y
proof
assume p in Y;
then consider X1 such that
A7: p in X1 and
A8: X1 in Z by TARSKI:def 4;
A9: X1 is Filter of L by A2,A8,Th17;
assume q in Y;
then consider X2 such that
A10: q in X2 and
A11: X2 in Z by TARSKI:def 4;
X1,X2 are_c=-comparable by A3,A8,A11,ORDINAL1:def 8;
then
A12: X1 c= X2 or X2 c= X1;
X2 is Filter of L by A2,A11,Th17;
then p "/\" q in X1 or p "/\" q in X2 by A7,A10,A9,A12,FILTER_0:8;
hence thesis by A8,A11,TARSKI:def 4;
end;
assume p "/\" q in Y;
then consider X1 such that
A13: p "/\" q in X1 and
A14: X1 in Z by TARSKI:def 4;
A15: X1 is Filter of L by A2,A14,Th17;
then
A16: q in X1 by A13,FILTER_0:8;
p in X1 by A13,A15,FILTER_0:8;
hence p in Y & q in Y by A14,A16,TARSKI:def 4;
end;
then Y is Filter of L by FILTER_0:8;
hence thesis by A4,A6,Lm1;
end;
hence thesis by ZFMISC_1:74;
end;
theorem Th19:
not b [= a implies <.b.) in SF_have b \ SF_have a
proof
assume not b [= a;
then not a in <.b.) by FILTER_0:15;
then
A1: not <.b.) in SF_have a by Th16;
b in <.b.);
then <.b.) in SF_have b;
hence thesis by A1,XBOOLE_0:def 5;
end;
theorem Th20:
not b [= a implies ex F st F in F_primeSet(L) & not a in F & b in F
proof
set A = SF_have b \ SF_have a;
assume not b [= a;
then
A1: A <> {} by Th19;
for Z st Z <> {} & Z c= SF_have b \ SF_have a & Z is c=-linear ex Y st Y
in SF_have b\ SF_have a & for X1 st X1 in Z holds X1 c= Y by Th18;
then consider Y such that
A2: Y in A and
A3: for Z st Z in A & Z <> Y holds not Y c= Z by A1,LATTICE4:1;
reconsider Y as Filter of L by A2,Th17;
A4: b in Y by A2,Th17;
A5: not a in Y by A2,Th17;
A6: Y is prime
proof
let a1,a2 be Element of L;
thus a1"\/"a2 in Y implies a1 in Y or a2 in Y
proof
set F2=<.<.a2.) \/ Y.);
set F1=<.<.a1.) \/ Y.);
assume that
A7: a1"\/"a2 in Y and
A8: not a1 in Y and
A9: not a2 in Y;
A10: <.a1.) c= F1 by LATTICE4:2;
a1 in <.a1.);
then
A11: a1 in F1 by A10;
A12: Y c= F1 by LATTICE4:2;
A13: <.a2.) c= F2 by LATTICE4:2;
a2 in <.a2.);
then
A14: a2 in F2 by A13;
A15: Y c= F2 by LATTICE4:2;
not a in F1 or not a in F2
proof
assume that
A16: a in F1 and
A17: a in F2;
consider c1 being Element of L such that
A18: c1 in Y and
A19: a1 "/\" c1 [= a by A16,LATTICE4:3;
consider c2 being Element of L such that
A20: c2 in Y and
A21: a2 "/\" c2 [= a by A17,LATTICE4:3;
set c = c1 "/\" c2;
a2 "/\" c [= a2 "/\" c2 by LATTICES:6,9;
then
A22: a2 "/\" c [= a by A21,LATTICES:7;
a1 "/\" c [= a1 "/\" c1 by LATTICES:6,9;
then a1 "/\" c [= a by A19,LATTICES:7;
then (a1 "/\" c) "\/"( a2 "/\" c) [= a by A22,FILTER_0:6;
then
A23: (a1 "\/" a2) "/\" c [= a by LATTICES:def 11;
c in Y by A18,A20,FILTER_0:8;
then (a1 "\/" a2) "/\" c in Y by A7,FILTER_0:8;
hence contradiction by A5,A23,FILTER_0:9;
end;
then F1 in A or F2 in A by A4,A12,A15,Lm1;
hence contradiction by A3,A8,A9,A11,A14,A12,A15;
end;
thus thesis by FILTER_0:10;
end;
Y <> the carrier of L by A2,Th17;
then Y in F_primeSet(L) by A6;
hence thesis by A5,A4;
end;
theorem Th21:
a <> b implies ex F st F in F_primeSet(L)
proof
assume a <> b;
then not a [= b or not b [= a by LATTICES:8;
then (ex F st F in F_primeSet(L) & not b in F & a in F) or ex F st F in
F_primeSet(L) & not a in F & b in F by Th20;
hence thesis;
end;
theorem Th22:
a <> b implies StoneH(L).a <> StoneH(L).b
proof
assume a <> b;
then not a [= b or not b [= a by LATTICES:8;
then (ex F st F in F_primeSet(L) & not b in F & a in F) or ex F st F in
F_primeSet(L) & not a in F & b in F by Th20;
then consider F such that
A1: F in F_primeSet(L) and
A2: b in F & not a in F or a in F & not b in F;
F in StoneH(L).a & not F in StoneH(L).b or F in StoneH(L).b & not F in
StoneH(L).a by A1,A2,Th11;
hence thesis;
end;
registration
let L;
cluster StoneH(L) -> one-to-one;
coherence
proof
let x1,x2 be object;
assume that
A1: x1 in dom StoneH(L) and
A2: x2 in dom StoneH(L) and
A3: StoneH(L).x1 = StoneH(L).x2;
reconsider a1=x1,a2=x2 as Element of L by A1,A2,Def6;
a1=a2 by A3,Th22;
hence thesis;
end;
end;
definition
let L;
let A,B be Element of StoneS(L);
redefine func A \/ B -> Element of StoneS(L);
coherence
proof
consider b such that
A1: B = StoneH(L).b by Th13;
consider a such that
A2: A = StoneH(L).a by Th13;
A \/ B = StoneH(L).(a "\/" b) by A2,A1,Th14;
hence thesis by Th13;
end;
redefine func A /\ B -> Element of StoneS(L);
coherence
proof
consider b such that
A3: B = StoneH(L).b by Th13;
consider a such that
A4: A = StoneH(L).a by Th13;
A /\ B = StoneH(L).(a "/\" b) by A4,A3,Th15;
hence thesis by Th13;
end;
end;
definition
let L;
func Set_Union L -> BinOp of StoneS(L) means
:Def9:
for A,B being Element of StoneS(L) holds it.(A,B) = A \/ B;
existence
proof
deffunc F(Element of StoneS(L), Element of StoneS(L)) = $1 \/ $2;
thus ex F being BinOp of StoneS(L) st for P,Q being Element of StoneS(L)
holds F.(P,Q) = F(P,Q) from BINOP_1:sch 4;
end;
uniqueness
proof
set A = StoneS(L);
deffunc O(Element of A, Element of A) = $1 \/ $2;
thus for o1,o2 being BinOp of A st (for a,b being Element of A holds o1.(a
,b) = O(a,b)) & (for a,b being Element of A holds o2.(a,b) = O(a,b)) holds o1 =
o2 from BINOP_2:sch 2;
end;
func Set_Meet L -> BinOp of StoneS(L) means
:Def10:
for A,B being Element of StoneS(L) holds it.(A,B) = A /\ B;
existence
proof
deffunc F(Element of StoneS(L), Element of StoneS(L)) = $1 /\ $2;
thus ex F being BinOp of StoneS(L) st for P,Q being Element of StoneS(L)
holds F.(P,Q) = F(P,Q) from BINOP_1:sch 4;
end;
uniqueness
proof
set A = StoneS(L);
deffunc O(Element of A, Element of A) = $1 /\ $2;
thus for o1,o2 being BinOp of A st (for a,b being Element of A holds o1.(a
,b) = O(a,b)) & (for a,b being Element of A holds o2.(a,b) = O(a,b)) holds o1 =
o2 from BINOP_2:sch 2;
end;
end;
theorem Th23:
LattStr(#StoneS(L),Set_Union L,Set_Meet L#) is Lattice
proof
set SL = LattStr(#StoneS(L),Set_Union L,Set_Meet L#);
A1: now
let p,q be Element of SL;
thus p "\/" q = q \/ p by Def9
.= q"\/"p by Def9;
end;
A2: now
let p,q be Element of SL;
thus (p"/\"q)"\/"q = (p"/\"q) \/ q by Def9
.= (p /\ q) \/ q by Def10
.= q by XBOOLE_1:22;
end;
A3: now
let p,q be Element of SL;
thus p"/\"(p"\/"q) = p /\ (p"\/"q) by Def10
.= p /\ (p \/ q) by Def9
.= p by XBOOLE_1:21;
end;
A4: now
let p,q,r be Element of SL;
thus p"/\"(q"/\"r) = p /\ (q "/\" r) by Def10
.= p /\ (q /\ r) by Def10
.= (p /\ q) /\ r by XBOOLE_1:16
.= (p "/\" q) /\ r by Def10
.= (p"/\"q)"/\"r by Def10;
end;
A5: now
let p,q be Element of SL;
thus p "/\" q =q /\ p by Def10
.= q"/\"p by Def10;
end;
now
let p,q,r be Element of SL;
thus p"\/"(q"\/"r) = p \/ (q "\/" r) by Def9
.= p \/ (q \/ r) by Def9
.= (p \/ q) \/ r by XBOOLE_1:4
.= (p "\/" q) \/ r by Def9
.= (p"\/"q)"\/"r by Def9;
end;
then
SL is join-commutative join-associative meet-absorbing meet-commutative
meet-associative join-absorbing by A1,A2,A5,A4,A3;
hence thesis;
end;
definition
let L;
func StoneLatt L -> Lattice equals
LattStr(#StoneS(L),Set_Union L,Set_Meet L
#);
coherence by Th23;
end;
reserve p,q for Element of StoneLatt(L);
theorem
for L holds the carrier of StoneLatt(L) = StoneS(L);
theorem
p "\/" q = p \/ q & p "/\" q = p /\ q by Def9,Def10;
theorem
p [= q iff p c= q
proof
p "\/" q = p \/ q by Def9;
hence thesis by XBOOLE_1:7,12;
end;
definition
let L;
::$N Stone Representation Theorem for Heyting Lattices
redefine func StoneH(L) -> Homomorphism of L,StoneLatt L;
coherence
proof
dom StoneH(L) = the carrier of L by Def6;
then reconsider
f=StoneH(L) as Function of the carrier of L, the carrier of
StoneLatt L by FUNCT_2:1;
now
let a,b;
thus f.(a "\/" b) = f.(a) \/ f.(b) by Th14
.=f.a "\/" f.b by Def9;
thus f.(a "/\" b) = f.(a) /\ f.(b) by Th15
.=f.(a) "/\" f.(b) by Def10;
end;
hence thesis by LATTICE4:def 1;
end;
end;
registration
let L;
cluster StoneH(L) -> bijective for Function of L,StoneLatt L;
coherence
proof
StoneH(L) is one-to-one onto;
hence thesis;
end;
cluster StoneLatt(L) -> distributive;
coherence
proof
StoneH(L) is onto;
hence thesis by LATTICE4:11;
end;
end;
theorem
L,StoneLatt L are_isomorphic
proof
take StoneH(L);
thus thesis;
end;
registration
cluster non trivial for H_Lattice;
existence
proof
set T = the non empty TopSpace;
set OL=Open_setLatt(T);
the carrier of T = Top OL by Th9;
then reconsider a= the carrier of T as Element of OL;
{} = Bottom OL by Th8;
then reconsider b= {} as Element of OL;
take OL,a,b;
thus thesis;
end;
end;
reserve H for non trivial H_Lattice;
reserve p9,q9 for Element of H;
theorem Th28:
StoneH(H).(Top H) = F_primeSet(H)
proof
hereby
let x be object;
assume x in StoneH(H).(Top H);
then
ex F being Filter of H st F=x & F <> the carrier of H & F is prime
& Top H in F by Th12;
hence x in F_primeSet(H);
end;
let x be object;
assume x in F_primeSet(H);
then consider F being Filter of H such that
A1: F=x and
A2: F <> the carrier of H and
A3: F is prime;
Top H in F by FILTER_0:11;
hence thesis by A1,A2,A3,Th12;
end;
theorem Th29:
StoneH(H).(Bottom H) = {}
proof
set x = the Element of StoneH(H).(Bottom H);
assume StoneH(H).(Bottom H) <> {};
then
ex F being Filter of H st F=x & F <> the carrier of H & F is prime &
Bottom H in F by Th12;
hence contradiction by FILTER_0:26;
end;
theorem Th30:
StoneS(H) c= bool F_primeSet(H)
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in StoneS(H);
then consider p9 such that
A1: x=StoneH(H).p9 by Th13;
A2: x={F where F is Filter of H:F in F_primeSet(H) & p9 in F} by A1,Def6;
xx c= F_primeSet(H)
proof
let y be object;
assume y in xx;
then
ex F being Filter of H st y=F & F in F_primeSet(H) & p9 in F by A2;
hence thesis;
end;
hence thesis;
end;
registration
let H;
cluster F_primeSet(H) -> non empty;
coherence
proof
ex p9,q9 st p9 <> q9 by STRUCT_0:def 10;
then ex F being Filter of H st F in F_primeSet(H) by Th21;
hence thesis;
end;
end;
definition
let H;
func HTopSpace H -> strict TopStruct means
:Def12:
the carrier of it =
F_primeSet(H) & the topology of it =the set of all
union A where A is Subset of StoneS(H);
existence
proof
set FS= F_primeSet(H);
set top=the set of all union A where A is Subset of StoneS(H);
A1: StoneS(H) c= bool FS by Th30;
top c= bool FS
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in top;
then consider A being Subset of StoneS(H) such that
A2: x=union A;
A c= bool FS by A1;
then xx c= union bool FS by A2,ZFMISC_1:77;
then x is Subset of FS by ZFMISC_1:81;
hence thesis;
end;
then reconsider top as Subset-Family of FS;
take TopStruct(#FS,top#);
thus thesis;
end;
uniqueness;
end;
registration
let H;
cluster HTopSpace H -> non empty TopSpace-like;
coherence
proof
reconsider A1={StoneH(H).(Top H)} as Subset of StoneS(H);
set TS = HTopSpace H;
A1: the topology of TS =the set of all union A where A is Subset of StoneS(H)
by Def12;
A2: the carrier of TS = F_primeSet(H) by Def12;
hence HTopSpace H is non empty;
F_primeSet(H) = StoneH(H).(Top H) by Th28;
then F_primeSet(H)=union A1 by ZFMISC_1:25;
hence the carrier of TS in the topology of TS by A2,A1;
hereby
let a be Subset-Family of TS;
defpred P[set] means union $1 in a;
set B= {A where A is Subset of StoneS(H) :P[A]};
set X= {union A where A is Subset of StoneS(H) : A in B};
assume
A3: a c= the topology of TS;
A4: a = X
proof
hereby
let x be object;
assume
A5: x in a;
then x in the topology of TS by A3;
then consider A be Subset of StoneS(H) such that
A6: x=union A by A1;
A in B by A5,A6;
hence x in X by A6;
end;
let x be object;
assume x in X;
then consider A be Subset of StoneS(H) such that
A7: x=union A and
A8: A in B;
ex A9 be Subset of StoneS(H) st A=A9 & union A9 in a by A8;
hence thesis by A7;
end;
reconsider B as Subset-Family of StoneS H from DOMAIN_1:sch 7;
union union B = union a by A4,EQREL_1:54;
hence union a in the topology of TS by A1;
end;
let a,b be Subset of TS;
assume that
A9: a in the topology of TS and
A10: b in the topology of TS;
consider A being Subset of StoneS(H) such that
A11: a = union A by A1,A9;
consider B being Subset of StoneS(H) such that
A12: b = union B by A1,A10;
INTERSECTION(A,B) c= StoneS(H)
proof
let x be object;
assume x in INTERSECTION(A,B);
then consider X,Y being set such that
A13: X in A and
A14: Y in B and
A15: x = X /\ Y by SETFAM_1:def 5;
consider p9 such that
A16: X=StoneH(H).p9 by A13,Th13;
consider q9 such that
A17: Y=StoneH(H).q9 by A14,Th13;
x = StoneH(H).(p9 "/\" q9) by A15,A16,A17,Th15;
hence thesis;
end;
then reconsider C=INTERSECTION(A,B) as Subset of StoneS(H);
union A /\ union B = union C by SETFAM_1:28;
hence thesis by A1,A11,A12;
end;
end;
theorem
the carrier of Open_setLatt(HTopSpace H) = the set of all
union A where A is Subset
of StoneS(H) by Def12;
theorem Th32:
StoneS(H) c= the carrier of Open_setLatt(HTopSpace H)
proof
let x be object;
set carrO = the carrier of Open_setLatt(HTopSpace H);
assume x in StoneS(H);
then reconsider z={x} as Subset of StoneS(H) by ZFMISC_1:31;
A1: union z = x by ZFMISC_1:25;
carrO = the set of all union A where A is Subset of StoneS(H) by Def12;
hence thesis by A1;
end;
definition
let H;
redefine func StoneH(H) -> Homomorphism of H,Open_setLatt(HTopSpace H);
coherence
proof
set LH=Open_setLatt(HTopSpace H);
reconsider g=StoneH(H) as Function of the carrier of H, the carrier of
StoneLatt(H);
StoneS(H) c= the carrier of LH by Th32;
then reconsider f=g as Function of the carrier of H, the carrier of LH by
FUNCT_2:6;
now
let p9,q9;
thus f.(p9 "\/" q9) = StoneH(H).p9 \/ StoneH(H).q9 by Th14
.= f.p9 "\/" f.q9 by Def2;
thus f.(p9 "/\" q9) = StoneH(H).p9 /\ StoneH(H).q9 by Th15
.= f.p9 "/\" f.q9 by Def3;
end;
hence thesis by LATTICE4:def 1;
end;
end;
theorem Th33:
StoneH(H).(p9 => q9) = (StoneH(H).p9) => (StoneH(H).q9)
proof
A1: the carrier of Open_setLatt(HTopSpace H) = the set of all
union A where A is Subset of
StoneS(H) by Def12;
A2: now
let r be Element of Open_setLatt(HTopSpace H);
r in the carrier of Open_setLatt(HTopSpace H);
then consider A being Subset of StoneS(H) such that
A3: r = union A by A1;
assume StoneH(H).p9 "/\" r [= StoneH(H).q9;
then StoneH(H).p9 "/\" r c= StoneH(H).q9 by Th6;
then StoneH(H).p9 /\ union A c= StoneH(H).q9 by A3,Def3;
then
A4: union INTERSECTION ({StoneH(H).p9}, A) c= StoneH(H).q9 by SETFAM_1:25;
now
let x;
assume
A5: x in A;
then consider x9 being Element of H such that
A6: x=StoneH(H).x9 by Th13;
StoneH(H).p9 in {StoneH(H).p9} by TARSKI:def 1;
then StoneH(H).p9 /\ x in INTERSECTION ({StoneH(H).p9}, A) by A5,
SETFAM_1:def 5;
then StoneH(H).p9 /\ StoneH(H).x9 c= StoneH(H).q9 by A4,A6,SETFAM_1:41;
then StoneH(H).(p9 "/\" x9) c= StoneH(H).q9 by Th15;
then StoneH(H).(p9 "/\" x9) [= StoneH(H).q9 by Th6;
then (p9 "/\" x9) [= q9 by LATTICE4:5;
then x9 [= p9 => q9 by FILTER_0:def 7;
then StoneH(H).x9 [= StoneH(H).(p9 => q9) by LATTICE4:4;
hence x c= StoneH(H).(p9 => q9) by A6,Th6;
end;
then union A c= StoneH(H).(p9 => q9) by ZFMISC_1:76;
hence r [= StoneH(H).(p9 => q9) by A3,Th6;
end;
p9 "/\" (p9 => q9) [= q9 by FILTER_0:def 7;
then StoneH(H).(p9 "/\" (p9 => q9)) [= StoneH(H).q9 by LATTICE4:4;
then StoneH(H).p9"/\" StoneH(H).(p9 => q9) [= StoneH(H).q9 by LATTICE4:def 1;
hence thesis by A2,FILTER_0:def 7;
end;
theorem
StoneH(H) preserves_implication
by Th33;
theorem
StoneH(H) preserves_top
proof
StoneH(H).(Top H) = F_primeSet(H) by Th28
.= the carrier of HTopSpace H by Def12
.= Top (Open_setLatt(HTopSpace H)) by Th9;
hence thesis;
end;
theorem
StoneH(H) preserves_bottom
proof
StoneH(H).(Bottom H) = {} by Th29
.= Bottom (Open_setLatt(HTopSpace H)) by Th8;
hence thesis;
end;