:: by Jaros{\l}aw Stanis{\l}aw Walijewski

::

:: Received July 14, 1993

:: Copyright (c) 1993-2018 Association of Mizar Users

definition

let T be non empty TopStruct ;

{ x where x is Subset of T : ( x is open & x is closed ) } is Subset-Family of T

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

{ x where x is Subset of T : ( x is open & x is closed ) } is Subset-Family of T

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

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

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

redefine func C /\ D -> Element of OpenClosedSet T;

coherence

C /\ D is Element of OpenClosedSet T

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

definition

let T be non empty TopSpace;

deffunc H_{1}( Element of OpenClosedSet T, Element of OpenClosedSet T) -> Element of OpenClosedSet T = $1 \/ $2;

ex b_{1} being BinOp of (OpenClosedSet T) st

for A, B being Element of OpenClosedSet T holds b_{1} . (A,B) = A \/ B

for b_{1}, b_{2} being BinOp of (OpenClosedSet T) st ( for A, B being Element of OpenClosedSet T holds b_{1} . (A,B) = A \/ B ) & ( for A, B being Element of OpenClosedSet T holds b_{2} . (A,B) = A \/ B ) holds

b_{1} = b_{2}
_{2}( Element of OpenClosedSet T, Element of OpenClosedSet T) -> Element of OpenClosedSet T = $1 /\ $2;

ex b_{1} being BinOp of (OpenClosedSet T) st

for A, B being Element of OpenClosedSet T holds b_{1} . (A,B) = A /\ B

for b_{1}, b_{2} being BinOp of (OpenClosedSet T) st ( for A, B being Element of OpenClosedSet T holds b_{1} . (A,B) = A /\ B ) & ( for A, B being Element of OpenClosedSet T holds b_{2} . (A,B) = A /\ B ) holds

b_{1} = b_{2}

end;
deffunc H

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 for A, B being Element of OpenClosedSet T holds it . (A,B) = A \/ B;

ex b

for A, B being Element of OpenClosedSet T holds b

proof end;

uniqueness for b

b

proof end;

deffunc H
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 for A, B being Element of OpenClosedSet T holds it . (A,B) = A /\ B;

ex b

for A, B being Element of OpenClosedSet T holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines T_join LOPCLSET:def 2 :

for T being non empty TopSpace

for b_{2} being BinOp of (OpenClosedSet T) holds

( b_{2} = T_join T iff for A, B being Element of OpenClosedSet T holds b_{2} . (A,B) = A \/ B );

for T being non empty TopSpace

for b

( b

:: deftheorem Def3 defines T_meet LOPCLSET:def 3 :

for T being non empty TopSpace

for b_{2} being BinOp of (OpenClosedSet T) holds

( b_{2} = T_meet T iff for A, B being Element of OpenClosedSet T holds b_{2} . (A,B) = A /\ B );

for T being non empty TopSpace

for b

( b

theorem :: LOPCLSET:4

theorem :: LOPCLSET:5

theorem :: LOPCLSET:6

theorem :: LOPCLSET:7

theorem Th8: :: LOPCLSET:8

for T being non empty TopSpace

for x being Element of OpenClosedSet T holds x ` is Element of OpenClosedSet T

for x being Element of OpenClosedSet T holds x ` is Element of OpenClosedSet T

proof end;

theorem Th9: :: LOPCLSET:9

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;

LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is Lattice by Th9;

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

LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is Lattice by Th9;

:: deftheorem defines OpenClosedSetLatt LOPCLSET:def 4 :

for T being non empty TopSpace holds OpenClosedSetLatt T = LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #);

for T being non empty TopSpace holds OpenClosedSetLatt T = LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #);

theorem :: LOPCLSET:10

theorem :: LOPCLSET:11

theorem :: LOPCLSET:12

theorem :: LOPCLSET:13

theorem :: LOPCLSET:14

registration

not for b_{1} being B_Lattice holds b_{1} is trivial
end;

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 bounded complemented Boolean for B_Lattice;

existence not for b

proof end;

definition

let BL be non trivial B_Lattice;

{ F where F is Filter of BL : F is being_ultrafilter } is Subset-Family of BL

end;
func ultraset BL -> Subset-Family of BL equals :: LOPCLSET:def 5

{ F where F is Filter of BL : F is being_ultrafilter } ;

coherence { F where F is Filter of BL : F is being_ultrafilter } ;

{ F where F is Filter of BL : F is being_ultrafilter } is Subset-Family of BL

proof 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 being_ultrafilter } ;

for BL being non trivial B_Lattice holds ultraset BL = { F where F is Filter of BL : F is being_ultrafilter } ;

theorem :: LOPCLSET:15

theorem Th16: :: LOPCLSET:16

for BL being non trivial B_Lattice

for a being Element of BL holds { F where F is Filter of BL : ( F is being_ultrafilter & a in F ) } c= ultraset BL

for a being Element of BL holds { F where F is Filter of BL : ( F is being_ultrafilter & a in F ) } c= ultraset BL

proof end;

definition

let BL be non trivial B_Lattice;

ex b_{1} being Function st

( dom b_{1} = the carrier of BL & ( for a being Element of BL holds b_{1} . a = { UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF ) } ) )

for b_{1}, b_{2} being Function st dom b_{1} = the carrier of BL & ( for a being Element of BL holds b_{1} . a = { UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF ) } ) & dom b_{2} = the carrier of BL & ( for a being Element of BL holds b_{2} . a = { UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF ) } ) holds

b_{1} = b_{2}

end;
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 being_ultrafilter & a in UF ) } ) );

existence ( dom it = the carrier of BL & ( for a being Element of BL holds it . a = { UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF ) } ) );

ex b

( dom b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines UFilter LOPCLSET:def 6 :

for BL being non trivial B_Lattice

for b_{2} being Function holds

( b_{2} = UFilter BL iff ( dom b_{2} = the carrier of BL & ( for a being Element of BL holds b_{2} . a = { UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF ) } ) ) );

for BL being non trivial B_Lattice

for b

( b

theorem Th17: :: LOPCLSET:17

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 being_ultrafilter & a in F ) )

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 being_ultrafilter & a in F ) )

proof end;

theorem Th18: :: LOPCLSET:18

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 being_ultrafilter & a in F ) )

for a being Element of BL

for F being Filter of BL holds

( F in (UFilter BL) . a iff ( F is being_ultrafilter & a in F ) )

proof end;

theorem Th19: :: LOPCLSET:19

for BL being non trivial B_Lattice

for a, b being Element of BL

for F being Filter of BL st F is being_ultrafilter holds

( a "\/" b in F iff ( a in F or b in F ) )

for a, b being Element of BL

for F being Filter of BL st F is being_ultrafilter holds

( a "\/" b in F iff ( a in F or b in F ) )

proof end;

theorem Th20: :: LOPCLSET:20

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)

for a, b being Element of BL holds (UFilter BL) . (a "/\" b) = ((UFilter BL) . a) /\ ((UFilter BL) . b)

proof end;

theorem Th21: :: LOPCLSET:21

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)

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

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

:: deftheorem defines StoneR LOPCLSET:def 7 :

for BL being non trivial B_Lattice holds StoneR BL = rng (UFilter BL);

for BL being non trivial B_Lattice holds StoneR BL = rng (UFilter BL);

theorem Th23: :: LOPCLSET:23

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 )

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;

ex b_{1} being strict TopSpace st

( the carrier of b_{1} = ultraset BL & the topology of b_{1} = { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } )

for b_{1}, b_{2} being strict TopSpace st the carrier of b_{1} = ultraset BL & the topology of b_{1} = { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } & the carrier of b_{2} = ultraset BL & the topology of b_{2} = { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } holds

b_{1} = b_{2}
;

end;
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 ( the carrier of it = ultraset BL & the topology of it = { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def8 defines StoneSpace LOPCLSET:def 8 :

for BL being non trivial B_Lattice

for b_{2} being strict TopSpace holds

( b_{2} = StoneSpace BL iff ( the carrier of b_{2} = ultraset BL & the topology of b_{2} = { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } ) );

for BL being non trivial B_Lattice

for b

( b

theorem :: LOPCLSET:24

theorem Th25: :: LOPCLSET:25

for BL being non trivial B_Lattice

for a being Element of BL holds (ultraset BL) \ ((UFilter BL) . a) = (UFilter BL) . (a `)

for a being Element of BL holds (ultraset BL) \ ((UFilter BL) . a) = (UFilter BL) . (a `)

proof end;

definition
end;

:: deftheorem defines StoneBLattice LOPCLSET:def 9 :

for BL being non trivial B_Lattice holds StoneBLattice BL = OpenClosedSetLatt (StoneSpace BL);

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;

registration

let D be non empty set ;

existence

not for b_{1} being Element of Fin D holds b_{1} is empty
by Th27;

end;
existence

not for b

theorem Th28: :: LOPCLSET:28

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 Element of Fin the carrier of L st

( B c= D & FinMeet B = Bottom L )

for D being non empty Subset of L st Bottom L in <.D.) holds

ex B being non empty Element of Fin the carrier of L st

( B c= D & FinMeet B = Bottom L )

proof end;

theorem Th29: :: LOPCLSET:29

for L being 0_Lattice

for F being Filter of L holds

( not F is being_ultrafilter or not Bottom L in F )

for F being Filter of L holds

( not F is being_ultrafilter or not Bottom L in F )

proof end;

theorem Th32: :: LOPCLSET:32

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 Element of Fin X st ultraset BL = union Y

for BL being non trivial B_Lattice st ultraset BL = union X & X is Subset of (StoneR BL) holds

ex Y being Element of Fin 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;

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

end;
:: original: UFilter

redefine func UFilter BL -> Homomorphism of BL, StoneBLattice BL;

coherence

UFilter BL is Homomorphism of BL, StoneBLattice BL

proof end;

registration

let BL be non trivial B_Lattice;

coherence

for b_{1} being Function of BL,(StoneBLattice BL) st b_{1} = UFilter BL holds

b_{1} is bijective

end;
coherence

for b

b

proof end;

:: Stone Representation Theorem for Boolean Algebras

theorem :: LOPCLSET:36

for BL being non trivial B_Lattice ex T being non empty TopSpace st BL, OpenClosedSetLatt T are_isomorphic

proof end;