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

definition
let T be non empty TopStruct ;
func OpenClosedSet T -> Subset-Family of T equals :: LOPCLSET:def 1
{ x where x is Subset of T : ( x is open & x is closed ) } ;
coherence
{ x where x is Subset of T : ( x is open & x is closed ) } is Subset-Family of T
proof end;
end;

:: deftheorem defines OpenClosedSet LOPCLSET:def 1 :
for T being non empty TopStruct holds OpenClosedSet T = { x where x is Subset of T : ( x is open & x is closed ) } ;

registration
let T be non empty TopSpace;
cluster OpenClosedSet T -> non empty ;
coherence
not OpenClosedSet T is empty
proof end;
end;

theorem :: LOPCLSET:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th2: :: LOPCLSET:2  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 X being Subset of T st X in OpenClosedSet T holds
X is open
proof end;

theorem Th3: :: LOPCLSET:3  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 X being Subset of T st X in OpenClosedSet T holds
X is closed
proof end;

theorem Th4: :: LOPCLSET: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
for X being Subset of T st X is open & X is closed holds
X in OpenClosedSet T ;

definition
let T be non empty TopSpace;
let C, D be Element of OpenClosedSet T;
:: original: \/
redefine func C \/ D -> Element of OpenClosedSet T;
coherence
C \/ D is Element of OpenClosedSet T
proof end;
:: original: /\
redefine func C /\ D -> Element of OpenClosedSet T;
coherence
C /\ D is Element of OpenClosedSet T
proof end;
end;

definition
let T be non empty TopSpace;
deffunc H1( Element of OpenClosedSet T, Element of OpenClosedSet T) -> Element of OpenClosedSet T = $1 \/ $2;
func T_join T -> BinOp of OpenClosedSet T means :Def2: :: LOPCLSET:def 2
for A, B being Element of OpenClosedSet T holds it . A,B = A \/ B;
existence
ex b1 being BinOp of OpenClosedSet T st
for A, B being Element of OpenClosedSet T holds b1 . A,B = A \/ B
proof end;
uniqueness
for b1, b2 being BinOp of OpenClosedSet T st ( for A, B being Element of OpenClosedSet T holds b1 . A,B = A \/ B ) & ( for A, B being Element of OpenClosedSet T holds b2 . A,B = A \/ B ) holds
b1 = b2
proof end;
deffunc H2( Element of OpenClosedSet T, Element of OpenClosedSet T) -> Element of OpenClosedSet T = $1 /\ $2;
func T_meet T -> BinOp of OpenClosedSet T means :Def3: :: LOPCLSET:def 3
for A, B being Element of OpenClosedSet T holds it . A,B = A /\ B;
existence
ex b1 being BinOp of OpenClosedSet T st
for A, B being Element of OpenClosedSet T holds b1 . A,B = A /\ B
proof end;
uniqueness
for b1, b2 being BinOp of OpenClosedSet T st ( for A, B being Element of OpenClosedSet T holds b1 . A,B = A /\ B ) & ( for A, B being Element of OpenClosedSet T holds b2 . A,B = A /\ B ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines T_join LOPCLSET:def 2 :
for T being non empty TopSpace
for b2 being BinOp of OpenClosedSet T holds
( b2 = T_join T iff for A, B being Element of OpenClosedSet T holds b2 . A,B = A \/ B );

:: deftheorem Def3 defines T_meet LOPCLSET:def 3 :
for T being non empty TopSpace
for b2 being BinOp of OpenClosedSet T holds
( b2 = T_meet T iff for A, B being Element of OpenClosedSet T holds b2 . A,B = A /\ B );

theorem Th5: :: LOPCLSET: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
for x, y being Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #)
for x', y' being Element of OpenClosedSet T st x = x' & y = y' holds
x "\/" y = x' \/ y' by Def2;

theorem Th6: :: LOPCLSET: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 x, y being Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #)
for x', y' being Element of OpenClosedSet T st x = x' & y = y' holds
x "/\" y = x' /\ y' by Def3;

theorem Th7: :: LOPCLSET: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 holds {} T is Element of OpenClosedSet T
proof end;

theorem Th8: :: LOPCLSET: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 holds [#] T is Element of OpenClosedSet T
proof end;

theorem Th9: :: LOPCLSET: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
for x being Element of OpenClosedSet T holds x ` is Element of OpenClosedSet T
proof end;

theorem Th10: :: LOPCLSET: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 LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is Lattice
proof end;

definition
let T be non empty TopSpace;
func OpenClosedSetLatt T -> Lattice equals :: LOPCLSET:def 4
LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #);
coherence
LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is Lattice
by Th10;
end;

:: deftheorem defines OpenClosedSetLatt LOPCLSET:def 4 :
for T being non empty TopSpace holds OpenClosedSetLatt T = LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #);

theorem Th11: :: LOPCLSET: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
for x, y being Element of (OpenClosedSetLatt T) holds x "\/" y = x \/ y by Th5;

theorem Th12: :: LOPCLSET:12  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 x, y being Element of (OpenClosedSetLatt T) holds x "/\" y = x /\ y by Th6;

theorem :: LOPCLSET:13  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 (OpenClosedSetLatt T) = OpenClosedSet T ;

theorem Th14: :: LOPCLSET:14  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 OpenClosedSetLatt T is Boolean
proof end;

theorem Th15: :: LOPCLSET:15  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 [#] T is Element of (OpenClosedSetLatt T) by Th8;

theorem Th16: :: LOPCLSET:16  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 {} T is Element of (OpenClosedSetLatt T) by Th7;

registration
cluster non trivial LattStr ;
existence
not for b1 being B_Lattice holds b1 is trivial
proof end;
end;

definition
let BL be non trivial B_Lattice;
func ultraset BL -> Subset-Family of BL equals :: LOPCLSET:def 5
{ F where F is Filter of BL : F is_ultrafilter } ;
coherence
{ F where F is Filter of BL : F is_ultrafilter } is Subset-Family of BL
proof end;
end;

:: deftheorem defines ultraset LOPCLSET:def 5 :
for BL being non trivial B_Lattice holds ultraset BL = { F where F is Filter of BL : F is_ultrafilter } ;

registration
let BL be non trivial B_Lattice;
cluster ultraset BL -> non empty ;
coherence
not ultraset BL is empty
proof end;
end;

theorem :: LOPCLSET:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LOPCLSET:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for BL being non trivial B_Lattice holds
( x in ultraset BL iff ex UF being Filter of BL st
( UF = x & UF is_ultrafilter ) ) ;

theorem Th19: :: LOPCLSET:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for BL being non trivial B_Lattice
for a being Element of BL holds { F where F is Filter of BL : ( F is_ultrafilter & a in F ) } c= ultraset BL
proof end;

definition
let BL be non trivial B_Lattice;
func UFilter BL -> Function means :Def6: :: LOPCLSET:def 6
( dom it = the carrier of BL & ( for a being Element of BL holds it . a = { UF where UF is Filter of BL : ( UF is_ultrafilter & a in UF ) } ) );
existence
ex b1 being Function st
( dom b1 = the carrier of BL & ( for a being Element of BL holds b1 . a = { UF where UF is Filter of BL : ( UF is_ultrafilter & a in UF ) } ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = the carrier of BL & ( for a being Element of BL holds b1 . a = { UF where UF is Filter of BL : ( UF is_ultrafilter & a in UF ) } ) & dom b2 = the carrier of BL & ( for a being Element of BL holds b2 . a = { UF where UF is Filter of BL : ( UF is_ultrafilter & a in UF ) } ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines UFilter LOPCLSET:def 6 :
for BL being non trivial B_Lattice
for b2 being Function holds
( b2 = UFilter BL iff ( dom b2 = the carrier of BL & ( for a being Element of BL holds b2 . a = { UF where UF is Filter of BL : ( UF is_ultrafilter & a in UF ) } ) ) );

theorem Th20: :: LOPCLSET:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for BL being non trivial B_Lattice
for a being Element of BL holds
( x in (UFilter BL) . a iff ex F being Filter of BL st
( F = x & F is_ultrafilter & a in F ) )
proof end;

theorem Th21: :: LOPCLSET:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for BL being non trivial B_Lattice
for a being Element of BL
for F being Filter of BL holds
( F in (UFilter BL) . a iff ( F is_ultrafilter & a in F ) )
proof end;

theorem Th22: :: LOPCLSET:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for BL being non trivial B_Lattice
for a, b being Element of BL
for F being Filter of BL st F is_ultrafilter holds
( a "\/" b in F iff ( a in F or b in F ) )
proof end;

theorem Th23: :: LOPCLSET:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for BL being non trivial B_Lattice
for a, b being Element of BL holds (UFilter BL) . (a "/\" b) = ((UFilter BL) . a) /\ ((UFilter BL) . b)
proof end;

theorem Th24: :: LOPCLSET:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for BL being non trivial B_Lattice
for a, b being Element of BL holds (UFilter BL) . (a "\/" b) = ((UFilter BL) . a) \/ ((UFilter BL) . b)
proof end;

definition
let BL be non trivial B_Lattice;
:: original: UFilter
redefine func UFilter BL -> Function of the carrier of BL, bool (ultraset BL);
coherence
UFilter BL is Function of the carrier of BL, bool (ultraset BL)
proof end;
end;

definition
let BL be non trivial B_Lattice;
func StoneR BL -> set equals :: LOPCLSET:def 7
rng (UFilter BL);
coherence
rng (UFilter BL) is set
;
end;

:: deftheorem defines StoneR LOPCLSET:def 7 :
for BL being non trivial B_Lattice holds StoneR BL = rng (UFilter BL);

registration
let BL be non trivial B_Lattice;
cluster StoneR BL -> non empty ;
coherence
not StoneR BL is empty
proof end;
end;

theorem Th25: :: LOPCLSET:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for BL being non trivial B_Lattice holds StoneR BL c= bool (ultraset BL) by RELSET_1:12;

theorem Th26: :: LOPCLSET:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for BL being non trivial B_Lattice holds
( x in StoneR BL iff ex a being Element of BL st (UFilter BL) . a = x )
proof end;

definition
let BL be non trivial B_Lattice;
func StoneSpace BL -> strict TopSpace means :Def8: :: LOPCLSET:def 8
( the carrier of it = ultraset BL & the topology of it = { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } );
existence
ex b1 being strict TopSpace st
( the carrier of b1 = ultraset BL & the topology of b1 = { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } )
proof end;
uniqueness
for b1, b2 being strict TopSpace st the carrier of b1 = ultraset BL & the topology of b1 = { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } & the carrier of b2 = ultraset BL & the topology of b2 = { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } holds
b1 = b2
;
end;

:: deftheorem Def8 defines StoneSpace LOPCLSET:def 8 :
for BL being non trivial B_Lattice
for b2 being strict TopSpace holds
( b2 = StoneSpace BL iff ( the carrier of b2 = ultraset BL & the topology of b2 = { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } ) );

registration
let BL be non trivial B_Lattice;
cluster StoneSpace BL -> non empty strict ;
coherence
not StoneSpace BL is empty
proof end;
end;

theorem :: LOPCLSET:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for BL being non trivial B_Lattice
for a being Element of BL
for F being Filter of BL st F is_ultrafilter & not F in (UFilter BL) . a holds
not a in F by Th21;

theorem Th28: :: LOPCLSET:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for BL being non trivial B_Lattice
for a being Element of BL holds (ultraset BL) \ ((UFilter BL) . a) = (UFilter BL) . (a ` )
proof end;

definition
let BL be non trivial B_Lattice;
func StoneBLattice BL -> Lattice equals :: LOPCLSET:def 9
OpenClosedSetLatt (StoneSpace BL);
coherence
OpenClosedSetLatt (StoneSpace BL) is Lattice
;
end;

:: deftheorem defines StoneBLattice LOPCLSET:def 9 :
for BL being non trivial B_Lattice holds StoneBLattice BL = OpenClosedSetLatt (StoneSpace BL);

Lm1: for BL being non trivial B_Lattice
for p being Subset of (StoneSpace BL) st p in StoneR BL holds
p is open
proof end;

theorem Th29: :: LOPCLSET:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for BL being non trivial B_Lattice holds UFilter BL is one-to-one
proof end;

theorem :: LOPCLSET:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for BL being non trivial B_Lattice holds union (StoneR BL) = ultraset BL
proof end;

theorem :: LOPCLSET:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th32: :: LOPCLSET:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set holds
not for Y being Finite_Subset of X holds Y is empty
proof end;

registration
let D be non empty set ;
cluster non empty Element of Fin D;
existence
not for b1 being Finite_Subset of D holds b1 is empty
by Th32;
end;

theorem :: LOPCLSET:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th34: :: LOPCLSET:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non trivial B_Lattice
for D being non empty Subset of L st Bottom L in <.D.) holds
ex B being non empty Finite_Subset of the carrier of L st
( B c= D & FinMeet B = Bottom L )
proof end;

theorem Th35: :: LOPCLSET:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being 0_Lattice
for F being Filter of L holds
( not F is_ultrafilter or not Bottom L in F )
proof end;

theorem Th36: :: LOPCLSET:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for BL being non trivial B_Lattice holds (UFilter BL) . (Bottom BL) = {}
proof end;

theorem :: LOPCLSET:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for BL being non trivial B_Lattice holds (UFilter BL) . (Top BL) = ultraset BL
proof end;

theorem Th38: :: LOPCLSET:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for BL being non trivial B_Lattice st ultraset BL = union X & X is Subset of (StoneR BL) holds
ex Y being Finite_Subset of X st ultraset BL = union Y
proof end;

Lm2: for BL being non trivial B_Lattice holds StoneR BL c= OpenClosedSet (StoneSpace BL)
proof end;

theorem :: LOPCLSET:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th40: :: LOPCLSET:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for BL being non trivial B_Lattice holds StoneR BL = OpenClosedSet (StoneSpace BL)
proof end;

definition
let BL be non trivial B_Lattice;
:: original: UFilter
redefine func UFilter BL -> Homomorphism of BL, StoneBLattice BL;
coherence
UFilter BL is Homomorphism of BL, StoneBLattice BL
proof end;
end;

theorem Th41: :: LOPCLSET:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for BL being non trivial B_Lattice holds rng (UFilter BL) = the carrier of (StoneBLattice BL)
proof end;

theorem Th42: :: LOPCLSET:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for BL being non trivial B_Lattice holds UFilter BL is isomorphism
proof end;

theorem Th43: :: LOPCLSET:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for BL being non trivial B_Lattice holds BL, StoneBLattice BL are_isomorphic
proof end;

theorem :: LOPCLSET:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for BL being non trivial B_Lattice ex T being non empty TopSpace st BL, OpenClosedSetLatt T are_isomorphic
proof end;