:: Representation Theorem for Boolean Algebras
:: by Jaros{\l}aw Stanis{\l}aw Walijewski
::
:: Received July 14, 1993
:: Copyright (c) 1993-2018 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 XBOOLE_0, PRE_TOPC, SUBSET_1, SETFAM_1, RCOMP_1, TARSKI,
ZFMISC_1, STRUCT_0, BINOP_1, FUNCT_1, LATTICES, EQREL_1, XXREAL_2,
CARD_FIL, RELAT_1, INT_2, FINSUB_1, SETWISEO, FILTER_0, LATTICE2, PBOOLE,
FINSET_1, CLASSES1, CARD_1, GROUP_6, FUNCT_2, WELLORD1, LOPCLSET;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, BINOP_1, FINSUB_1, STRUCT_0, PRE_TOPC, LATTICES,
LATTICE2, FILTER_0, FINSET_1, SETWISEO, LATTICE4, CLASSES1, CARD_1;
constructors BINOP_1, SETWISEO, PRE_TOPC, LATTICE2, FILTER_1, CLASSES1,
LATTICE4, RELSET_1, FILTER_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1,
FINSUB_1, STRUCT_0, LATTICES, PRE_TOPC, CARD_1, RELSET_1, TOPS_1,
LATTICE2;
requirements BOOLE, SUBSET;
begin
reserve T for non empty TopSpace,
X,Z for Subset of T;
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 closed};
end;
registration
let T be non empty TopSpace;
cluster OpenClosedSet(T) -> non empty;
end;
theorem :: LOPCLSET:1
X in OpenClosedSet(T) implies X is open;
theorem :: LOPCLSET:2
X in OpenClosedSet(T) implies X is closed;
theorem :: LOPCLSET:3
X is open closed implies X in OpenClosedSet(T);
reserve x,y for Element of OpenClosedSet(T);
definition
let T;
let C,D be Element of OpenClosedSet(T);
redefine func C \/ D -> Element of OpenClosedSet(T);
redefine func C /\ D -> Element of OpenClosedSet(T);
end;
definition
let T;
func T_join T -> BinOp of OpenClosedSet(T) means
:: LOPCLSET:def 2
for A,B being Element of OpenClosedSet(T) holds it.(A,B) = A \/ B;
func T_meet T -> BinOp of OpenClosedSet(T) means
:: LOPCLSET:def 3
for A,B being Element of OpenClosedSet(T) holds it.(A,B) = A /\ B;
end;
theorem :: LOPCLSET:4
for x,y be Element of LattStr(#OpenClosedSet(T),T_join T,T_meet T#),
x9,y9 be Element of OpenClosedSet(T)
st x=x9 & y=y9 holds x"\/"y = x9 \/ y9;
theorem :: LOPCLSET:5
for x,y be Element of LattStr(#OpenClosedSet(T),T_join T,T_meet T#),
x9,y9 be Element of OpenClosedSet(T)
st x=x9 & y=y9 holds x"/\"y = x9 /\ y9;
theorem :: LOPCLSET:6
{} T is Element of OpenClosedSet(T);
theorem :: LOPCLSET:7
[#] T is Element of OpenClosedSet(T);
theorem :: LOPCLSET:8
x` is Element of OpenClosedSet(T);
theorem :: LOPCLSET:9
LattStr(#OpenClosedSet(T),T_join T,T_meet T#) is Lattice;
definition
let T be non empty TopSpace;
func OpenClosedSetLatt(T) -> Lattice equals
:: LOPCLSET:def 4
LattStr(#OpenClosedSet(T),T_join T,T_meet T#);
end;
theorem :: LOPCLSET:10
for T being non empty TopSpace, x,y being Element of
OpenClosedSetLatt(T) holds x"\/"y = x \/ y;
theorem :: LOPCLSET:11
for T being non empty TopSpace , x,y being Element of
OpenClosedSetLatt(T) holds x"/\"y = x /\ y;
theorem :: LOPCLSET:12
the carrier of OpenClosedSetLatt(T) = OpenClosedSet(T);
registration
let T;
cluster OpenClosedSetLatt(T) -> Boolean;
end;
theorem :: LOPCLSET:13
[#] T is Element of OpenClosedSetLatt(T);
theorem :: LOPCLSET:14
{} T is Element of OpenClosedSetLatt(T);
reserve x,y,X for set;
registration
cluster non trivial for B_Lattice;
end;
reserve BL for non trivial B_Lattice,
a,b,c,p,q for Element of BL,
UF,F,F0,F1,F2 for Filter of BL;
definition
let BL;
func ultraset BL -> Subset-Family of BL equals
:: LOPCLSET:def 5
{F : F is being_ultrafilter};
end;
registration
let BL;
cluster ultraset BL -> non empty;
end;
theorem :: LOPCLSET:15
x in ultraset BL iff ex UF st UF = x & UF is being_ultrafilter;
theorem :: LOPCLSET:16
for a holds { F :F is being_ultrafilter & a in F} c= ultraset BL;
definition
let BL;
func UFilter BL -> Function means
:: LOPCLSET:def 6
dom it = the carrier of BL & for a being Element of BL
holds it.a = {UF: UF is being_ultrafilter & a in UF };
end;
theorem :: LOPCLSET:17
x in UFilter BL.a iff ex F st F=x & F is being_ultrafilter & a in F;
theorem :: LOPCLSET:18
F in UFilter BL.a iff F is being_ultrafilter & a in F;
theorem :: LOPCLSET:19
for F st F is being_ultrafilter holds a "\/" b in F iff a in F or b in F;
theorem :: LOPCLSET:20
UFilter BL.(a "/\" b) = UFilter BL.a /\ UFilter BL.b;
theorem :: LOPCLSET:21
UFilter BL.(a "\/" b) = UFilter BL.a \/ UFilter BL.b;
definition
let BL;
redefine func UFilter BL -> Function of the carrier of BL, bool ultraset BL;
end;
definition
let BL;
func StoneR BL -> set equals
:: LOPCLSET:def 7
rng UFilter BL;
end;
registration
let BL;
cluster StoneR BL -> non empty;
end;
theorem :: LOPCLSET:22
StoneR BL c= bool ultraset BL;
theorem :: LOPCLSET:23
x in StoneR BL iff ex a st (UFilter BL).a =x;
definition
let BL;
func StoneSpace BL -> strict TopSpace means
:: 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 };
end;
registration
let BL;
cluster StoneSpace BL -> non empty;
end;
theorem :: LOPCLSET:24
F is being_ultrafilter & not F in UFilter BL.a implies not a in F;
theorem :: LOPCLSET:25
ultraset BL \ UFilter BL.a = UFilter BL.a`;
definition
let BL;
func StoneBLattice BL -> Lattice equals
:: LOPCLSET:def 9
OpenClosedSetLatt(StoneSpace BL );
end;
registration
let BL;
cluster UFilter BL -> one-to-one;
end;
theorem :: LOPCLSET:26
union StoneR BL = ultraset BL;
theorem :: LOPCLSET:27
for X being non empty set ex Y being Element of Fin X st Y is non empty;
registration
let D be non empty set;
cluster non empty for Element of Fin D;
end;
theorem :: LOPCLSET:28
for L being non trivial B_Lattice, D being non empty Subset of L
st Bottom L in <.D.) ex B being non empty Element of Fin the carrier of L
st B c= D & FinMeet(B) = Bottom L;
theorem :: LOPCLSET:29
for L being 0_Lattice holds
not ex F being Filter of L st F is being_ultrafilter & Bottom L in F;
theorem :: LOPCLSET:30
UFilter BL.Bottom BL = {};
theorem :: LOPCLSET:31
UFilter BL.Top BL = ultraset BL;
theorem :: LOPCLSET:32
ultraset BL = union X & X is Subset of StoneR BL implies
ex Y being Element of Fin X st ultraset BL = union Y;
theorem :: LOPCLSET:33
StoneR BL = OpenClosedSet(StoneSpace BL);
definition
let BL;
redefine func UFilter BL -> Homomorphism of BL,StoneBLattice BL;
end;
theorem :: LOPCLSET:34
rng UFilter BL = the carrier of StoneBLattice BL;
registration
let BL;
cluster UFilter BL -> bijective for Function of BL,StoneBLattice BL;
end;
theorem :: LOPCLSET:35
BL,StoneBLattice BL are_isomorphic;
::$N 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;