:: LOPCLSET semantic presentation

definition

let c₁ be non empty TopStruct ;
func OpenClosedSet c₁ -> Subset-Family of a₁ equals :: LOPCLSET:def 1
{ b₁ where B is Subset of a₁ : ( b₁ is open & b₁ is closed ) } ;
coherence

proof end;

end;

:: deftheorem Def1 defines OpenClosedSet LOPCLSET:def 1 :

registration

let c₁ be non empty TopSpace;
cluster OpenClosedSet a₁ -> non empty ;
coherence

proof end;

end;

theorem Th1: :: LOPCLSET:1

canceled;

theorem Th2: :: LOPCLSET:2

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ in OpenClosedSet b₁ holds
b₂ is open

proof end;

theorem Th3: :: LOPCLSET:3

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ in OpenClosedSet b₁ holds
b₂ is closed

proof end;

theorem Th4: :: LOPCLSET:4

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is open & b₂ is closed holds
b₂ in OpenClosedSet b₁ ;

definition

let c₁ be non empty TopSpace;
let c₂, c₃ be Element of OpenClosedSet c₁;
redefine func \/ as c₂ \/ c₃ -> Element of OpenClosedSet a₁;
coherence

proof end;

redefine func /\ as c₂ /\ c₃ -> Element of OpenClosedSet a₁;
coherence

proof end;

end;

definition

let c₁ be non empty TopSpace;
deffunc H₁( Element of OpenClosedSet c₁, Element of OpenClosedSet c₁) -> Element of OpenClosedSet c₁ = a₁ \/ a₂;
func T_join c₁ -> BinOp of OpenClosedSet a₁ means :Def2: :: LOPCLSET:def 2
for b₁, b₂ being Element of OpenClosedSet a₁ holds a₂ . b₁,b₂ = b₁ \/ b₂;
existence

proof end;

uniqueness

proof end;

deffunc H₂( Element of OpenClosedSet c₁, Element of OpenClosedSet c₁) -> Element of OpenClosedSet c₁ = a₁ /\ a₂;
func T_meet c₁ -> BinOp of OpenClosedSet a₁ means :Def3: :: LOPCLSET:def 3
for b₁, b₂ being Element of OpenClosedSet a₁ holds a₂ . b₁,b₂ = b₁ /\ b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines T_join LOPCLSET:def 2 :

:: deftheorem Def3 defines T_meet LOPCLSET:def 3 :

theorem Th5: :: LOPCLSET:5

for b₁ being non empty TopSpace
for b₂, b₃ being Element of LattStr(# (OpenClosedSet b₁),(T_join b₁),(T_meet b₁) #)
for b₄, b₅ being Element of OpenClosedSet b₁ st b₂ = b₄ & b₃ = b₅ holds
b₂ "\/" b₃ = b₄ \/ b₅ by Def2;

theorem Th6: :: LOPCLSET:6

theorem Th7: :: LOPCLSET:7

for b₁ being non empty TopSpace holds {} b₁ is Element of OpenClosedSet b₁

proof end;

theorem Th8: :: LOPCLSET:8

for b₁ being non empty TopSpace holds [#] b₁ is Element of OpenClosedSet b₁

proof end;

theorem Th9: :: LOPCLSET:9

for b₁ being non empty TopSpace
for b₂ being Element of OpenClosedSet b₁ holds b₂ ` is Element of OpenClosedSet b₁

proof end;

theorem Th10: :: LOPCLSET:10

for b₁ being non empty TopSpace holds LattStr(# (OpenClosedSet b₁),(T_join b₁),(T_meet b₁) #) is Lattice

proof end;

definition

let c₁ be non empty TopSpace;
func OpenClosedSetLatt c₁ -> Lattice equals :: LOPCLSET:def 4
LattStr(# (OpenClosedSet a₁),(T_join a₁),(T_meet a₁) #);
coherence by Th10;

end;

:: deftheorem Def4 defines OpenClosedSetLatt LOPCLSET:def 4 :

theorem Th11: :: LOPCLSET:11

for b₁ being non empty TopSpace
for b₂, b₃ being Element of (OpenClosedSetLatt b₁) holds b₂ "\/" b₃ = b₂ \/ b₃ by Th5;

theorem Th12: :: LOPCLSET:12

for b₁ being non empty TopSpace
for b₂, b₃ being Element of (OpenClosedSetLatt b₁) holds b₂ "/\" b₃ = b₂ /\ b₃ by Th6;

theorem Th13: :: LOPCLSET:13

for b₁ being non empty TopSpace holds the carrier of (OpenClosedSetLatt b₁) = OpenClosedSet b₁ ;

theorem Th14: :: LOPCLSET:14

for b₁ being non empty TopSpace holds OpenClosedSetLatt b₁ is Boolean

proof end;

theorem Th15: :: LOPCLSET:15

for b₁ being non empty TopSpace holds [#] b₁ is Element of (OpenClosedSetLatt b₁) by Th8;

theorem Th16: :: LOPCLSET:16

for b₁ being non empty TopSpace holds {} b₁ is Element of (OpenClosedSetLatt b₁) by Th7;

registration

cluster non trivial LattStr ;
existence

proof end;

end;

definition

let c₁ be non trivial B_Lattice;
func ultraset c₁ -> Subset-Family of a₁ equals :: LOPCLSET:def 5
{ b₁ where B is Filter of a₁ : b₁ is_ultrafilter } ;
coherence

proof end;

end;

:: deftheorem Def5 defines ultraset LOPCLSET:def 5 :

registration

let c₁ be non trivial B_Lattice;
cluster ultraset a₁ -> non empty ;
coherence

proof end;

end;

theorem Th17: :: LOPCLSET:17

canceled;

theorem Th18: :: LOPCLSET:18

for b₁ being set
for b₂ being non trivial B_Lattice holds
( b₁ in ultraset b₂ iff ex b₃ being Filter of b₂ st
( b₃ = b₁ & b₃ is_ultrafilter ) ) ;

theorem Th19: :: LOPCLSET:19

for b₁ being non trivial B_Lattice
for b₂ being Element of b₁ holds { b₃ where B is Filter of b₁ : ( b₃ is_ultrafilter & b₂ in b₃ ) } c= ultraset b₁

proof end;

definition

let c₁ be non trivial B_Lattice;
func UFilter c₁ -> Function means :Def6: :: LOPCLSET:def 6
( dom a₂ = the carrier of a₁ & ( for b₁ being Element of a₁ holds a₂ . b₁ = { b₂ where B is Filter of a₁ : ( b₂ is_ultrafilter & b₁ in b₂ ) } ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines UFilter LOPCLSET:def 6 :

theorem Th20: :: LOPCLSET:20

for b₁ being set
for b₂ being non trivial B_Lattice
for b₃ being Element of b₂ holds
( b₁ in (UFilter b₂) . b₃ iff ex b₄ being Filter of b₂ st
( b₄ = b₁ & b₄ is_ultrafilter & b₃ in b₄ ) )

proof end;

theorem Th21: :: LOPCLSET:21

for b₁ being non trivial B_Lattice
for b₂ being Element of b₁
for b₃ being Filter of b₁ holds
( b₃ in (UFilter b₁) . b₂ iff ( b₃ is_ultrafilter & b₂ in b₃ ) )

proof end;

theorem Th22: :: LOPCLSET:22

for b₁ being non trivial B_Lattice
for b₂, b₃ being Element of b₁
for b₄ being Filter of b₁ st b₄ is_ultrafilter holds
( b₂ "\/" b₃ in b₄ iff ( b₂ in b₄ or b₃ in b₄ ) )

proof end;

theorem Th23: :: LOPCLSET:23

for b₁ being non trivial B_Lattice
for b₂, b₃ being Element of b₁ holds (UFilter b₁) . (b₂ "/\" b₃) = ((UFilter b₁) . b₂) /\ ((UFilter b₁) . b₃)

proof end;

theorem Th24: :: LOPCLSET:24

for b₁ being non trivial B_Lattice
for b₂, b₃ being Element of b₁ holds (UFilter b₁) . (b₂ "\/" b₃) = ((UFilter b₁) . b₂) \/ ((UFilter b₁) . b₃)

proof end;

definition

let c₁ be non trivial B_Lattice;
redefine func UFilter as UFilter c₁ -> Function of the carrier of a₁, bool (ultraset a₁);
coherence

proof end;

end;

definition

let c₁ be non trivial B_Lattice;
func StoneR c₁ -> set equals :: LOPCLSET:def 7
rng (UFilter a₁);
coherence ;

end;

:: deftheorem Def7 defines StoneR LOPCLSET:def 7 :

registration

let c₁ be non trivial B_Lattice;
cluster StoneR a₁ -> non empty ;
coherence

proof end;

end;

theorem Th25: :: LOPCLSET:25

for b₁ being non trivial B_Lattice holds StoneR b₁ c= bool (ultraset b₁) by RELSET_1:12;

theorem Th26: :: LOPCLSET:26

for b₁ being set
for b₂ being non trivial B_Lattice holds
( b₁ in StoneR b₂ iff ex b₃ being Element of b₂ st (UFilter b₂) . b₃ = b₁ )

proof end;

definition

let c₁ be non trivial B_Lattice;
func StoneSpace c₁ -> strict TopSpace means :Def8: :: LOPCLSET:def 8
( the carrier of a₂ = ultraset a₁ & the topology of a₂ = { (union b₁) where B is Subset-Family of (ultraset a₁) : b₁ c= StoneR a₁ } );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def8 defines StoneSpace LOPCLSET:def 8 :

registration

let c₁ be non trivial B_Lattice;
cluster StoneSpace a₁ -> non empty strict ;
coherence

proof end;

end;

theorem Th27: :: LOPCLSET:27

for b₁ being non trivial B_Lattice
for b₂ being Element of b₁
for b₃ being Filter of b₁ st b₃ is_ultrafilter & not b₃ in (UFilter b₁) . b₂ holds
not b₂ in b₃ by Th21;

theorem Th28: :: LOPCLSET:28

for b₁ being non trivial B_Lattice
for b₂ being Element of b₁ holds (ultraset b₁) \ ((UFilter b₁) . b₂) = (UFilter b₁) . (b₂ ` )

proof end;

definition

let c₁ be non trivial B_Lattice;
func StoneBLattice c₁ -> Lattice equals :: LOPCLSET:def 9
OpenClosedSetLatt (StoneSpace a₁);
coherence ;

end;

:: deftheorem Def9 defines StoneBLattice LOPCLSET:def 9 :

Lemma28: for b₁ being non trivial B_Lattice
for b₂ being Subset of (StoneSpace b₁) st b₂ in StoneR b₁ holds
b₂ is open

proof end;

theorem Th29: :: LOPCLSET:29

for b₁ being non trivial B_Lattice holds UFilter b₁ is one-to-one

proof end;

theorem Th30: :: LOPCLSET:30

for b₁ being non trivial B_Lattice holds union (StoneR b₁) = ultraset b₁

proof end;

theorem Th31: :: LOPCLSET:31

canceled;

theorem Th32: :: LOPCLSET:32

for b₁ being non empty set holds
not for b₂ being Finite_Subset of b₁ holds b₂ is empty

proof end;

registration

let c₁ be non empty set ;
cluster non empty Element of Fin a₁;
existence by Th32;

end;

theorem Th33: :: LOPCLSET:33

canceled;

theorem Th34: :: LOPCLSET:34

for b₁ being non trivial B_Lattice
for b₂ being non empty Subset of b₁ st Bottom b₁ in <.b₂.) holds
ex b₃ being non empty Finite_Subset of the carrier of b₁ st
( b₃ c= b₂ & FinMeet b₃ = Bottom b₁ )

proof end;

theorem Th35: :: LOPCLSET:35

for b₁ being 0_Lattice
for b₂ being Filter of b₁ holds
( not b₂ is_ultrafilter or not Bottom b₁ in b₂ )

proof end;

theorem Th36: :: LOPCLSET:36

for b₁ being non trivial B_Lattice holds (UFilter b₁) . (Bottom b₁) = {}

proof end;

theorem Th37: :: LOPCLSET:37

for b₁ being non trivial B_Lattice holds (UFilter b₁) . (Top b₁) = ultraset b₁

proof end;

theorem Th38: :: LOPCLSET:38

for b₁ being set
for b₂ being non trivial B_Lattice st ultraset b₂ = union b₁ & b₁ is Subset of (StoneR b₂) holds
ex b₃ being Finite_Subset of b₁ st ultraset b₂ = union b₃

proof end;

Lemma35: for b₁ being non trivial B_Lattice holds StoneR b₁ c= OpenClosedSet (StoneSpace b₁)

proof end;

theorem Th39: :: LOPCLSET:39

canceled;

theorem Th40: :: LOPCLSET:40

for b₁ being non trivial B_Lattice holds StoneR b₁ = OpenClosedSet (StoneSpace b₁)

proof end;

definition

let c₁ be non trivial B_Lattice;
redefine func UFilter as UFilter c₁ -> Homomorphism of a₁, StoneBLattice a₁;
coherence

proof end;

end;

theorem Th41: :: LOPCLSET:41

for b₁ being non trivial B_Lattice holds rng (UFilter b₁) = the carrier of (StoneBLattice b₁)

proof end;

theorem Th42: :: LOPCLSET:42

for b₁ being non trivial B_Lattice holds UFilter b₁ is isomorphism

proof end;

theorem Th43: :: LOPCLSET:43

for b₁ being non trivial B_Lattice holds b₁, StoneBLattice b₁ are_isomorphic

proof end;

theorem Th44: :: LOPCLSET:44

for b₁ being non trivial B_Lattice ex b₂ being non empty TopSpace st b₁, OpenClosedSetLatt b₂ are_isomorphic

proof end;