:: OPENLATT semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
cluster Heyting -> implicative LattStr ;
coherence
for b1 being 0_Lattice st b1 is Heyting holds
b1 is implicative
by LATTICE2:def 6;
cluster implicative -> upper-bounded LattStr ;
coherence
for b1 being Lattice st b1 is implicative holds
b1 is upper-bounded
by FILTER_0:37;
end;

theorem Th1: :: OPENLATT:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace
for A, B being Subset of T holds A /\ (Int ((A ` ) \/ B)) c= B
proof end;

theorem Th2: :: OPENLATT:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
by PRE_TOPC:5;
end;

theorem Th3: :: OPENLATT:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace
for A being Subset of T holds
( A is open iff A in Topology_of T ) by PRE_TOPC:def 5;

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

Lm1: for T being non empty TopSpace
for p, q being Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) holds p "\/" q = p \/ q
by Def2;

Lm2: for T being non empty TopSpace
for p, q being Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) holds p "/\" q = p /\ q
by Def3;

theorem Th4: :: OPENLATT:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace holds the carrier of (Open_setLatt T) = Topology_of T ;

theorem Th6: :: OPENLATT:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for p, q being Element of (Open_setLatt T)
for p', q' being Element of Topology_of T st p = p' & q = q' holds
( p [= q iff p' c= q' )
proof end;

theorem Th9: :: OPENLATT:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace holds Open_setLatt T is implicative
proof end;

theorem Th10: :: OPENLATT:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 -> upper-bounded Heyting ;
coherence
Open_setLatt T is Heyting
proof end;
end;

theorem Th11: :: OPENLATT:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th13: :: OPENLATT:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

Lm3: 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th25: :: OPENLATT:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being D_Lattice holds StoneH L is one-to-one
proof 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 );

Lm4: for L being D_Lattice
for x, y being Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) holds x "\/" y = x \/ y
by Def9;

Lm5: for L being D_Lattice
for x, y being Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) holds x "/\" y = x /\ y
by Def10;

theorem Th26: :: OPENLATT:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being D_Lattice holds the carrier of (StoneLatt L) = StoneS L ;

theorem Th28: :: OPENLATT:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being D_Lattice
for p, q being Element of (StoneLatt L) holds
( p "\/" q = p \/ q & p "/\" q = p /\ q ) by Lm4, Lm5;

theorem :: OPENLATT:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th30: :: OPENLATT:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being D_Lattice holds StoneH L is isomorphism
proof end;

theorem :: OPENLATT:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being D_Lattice holds StoneLatt L is distributive
proof end;

theorem :: OPENLATT:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being D_Lattice holds L, StoneLatt L are_isomorphic
proof end;

registration
cluster upper-bounded non trivial LattStr ;
existence
not for b1 being H_Lattice holds b1 is trivial
proof end;
end;

theorem Th33: :: OPENLATT:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being non trivial H_Lattice holds (StoneH H) . (Top H) = F_primeSet H
proof end;

theorem Th34: :: OPENLATT:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being non trivial H_Lattice holds (StoneH H) . (Bottom H) = {}
proof end;

theorem Th35: :: OPENLATT:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th36: :: OPENLATT:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th38: :: OPENLATT:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being non trivial H_Lattice holds StoneH H is monomorphism
proof end;

theorem Th39: :: OPENLATT:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being non trivial H_Lattice
for p', q' being Element of H holds (StoneH H) . (p' => q') = ((StoneH H) . p') => ((StoneH H) . q')
proof end;

theorem :: OPENLATT:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being non trivial H_Lattice holds StoneH H preserves_implication
proof end;

theorem :: OPENLATT:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being non trivial H_Lattice holds StoneH H preserves_top
proof end;

theorem :: OPENLATT:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being non trivial H_Lattice holds StoneH H preserves_bottom
proof end;