:: by Jolanta Kamie\'nska

::

:: Received July 14, 1993

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

registration

coherence

for b_{1} being 0_Lattice st b_{1} is Heyting holds

b_{1} is implicative
;

coherence

for b_{1} being Lattice st b_{1} is implicative holds

b_{1} is upper-bounded
;

end;
for b

b

coherence

for b

b

theorem Th2: :: OPENLATT:2

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)

for A, B, C being Subset of T st C is open & A /\ C c= B holds

C c= Int ((A `) \/ B)

proof end;

:: deftheorem defines Topology_of OPENLATT:def 1 :

for T being TopStruct holds Topology_of T = the topology of T;

for T being TopStruct holds Topology_of T = the topology of T;

registration
end;

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

redefine func P /\ Q -> Element of Topology_of T;

coherence

P /\ Q is Element of Topology_of T

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

definition

let T be non empty TopSpace;

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

for P, Q being Element of Topology_of T holds b_{1} . (P,Q) = P \/ Q

for b_{1}, b_{2} being BinOp of (Topology_of T) st ( for P, Q being Element of Topology_of T holds b_{1} . (P,Q) = P \/ Q ) & ( for P, Q being Element of Topology_of T holds b_{2} . (P,Q) = P \/ Q ) holds

b_{1} = b_{2}

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

for P, Q being Element of Topology_of T holds b_{1} . (P,Q) = P /\ Q

for b_{1}, b_{2} being BinOp of (Topology_of T) st ( for P, Q being Element of Topology_of T holds b_{1} . (P,Q) = P /\ Q ) & ( for P, Q being Element of Topology_of T holds b_{2} . (P,Q) = P /\ Q ) holds

b_{1} = b_{2}

end;
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 for P, Q being Element of Topology_of T holds it . (P,Q) = P \/ Q;

ex b

for P, Q being Element of Topology_of T holds b

proof end;

uniqueness for b

b

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 for P, Q being Element of Topology_of T holds it . (P,Q) = P /\ Q;

ex b

for P, Q being Element of Topology_of T holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines Top_Union OPENLATT:def 2 :

for T being non empty TopSpace

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

( b_{2} = Top_Union T iff for P, Q being Element of Topology_of T holds b_{2} . (P,Q) = P \/ Q );

for T being non empty TopSpace

for b

( b

:: deftheorem Def3 defines Top_Meet OPENLATT:def 3 :

for T being non empty TopSpace

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

( b_{2} = Top_Meet T iff for P, Q being Element of Topology_of T holds b_{2} . (P,Q) = P /\ Q );

for T being non empty TopSpace

for b

( b

theorem Th3: :: OPENLATT:3

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;

LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is Lattice by Th3;

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

LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is Lattice by Th3;

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

for T being non empty TopSpace holds Open_setLatt T = LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #);

theorem :: OPENLATT:4

theorem :: OPENLATT:5

theorem Th6: :: OPENLATT:6

for T being non empty TopSpace

for p, q being Element of (Open_setLatt T) holds

( p [= q iff p c= q )

for p, q being Element of (Open_setLatt T) holds

( p [= q iff p c= q )

proof end;

theorem Th7: :: OPENLATT:7

for T being non empty TopSpace

for p, q being Element of (Open_setLatt T)

for p9, q9 being Element of Topology_of T st p = p9 & q = q9 holds

( p [= q iff p9 c= q9 )

for p, q being Element of (Open_setLatt T)

for p9, q9 being Element of Topology_of T st p = p9 & q = q9 holds

( p [= q iff p9 c= q9 )

proof end;

theorem Th8: :: OPENLATT:8

for T being non empty TopSpace holds

( Open_setLatt T is lower-bounded & Bottom (Open_setLatt T) = {} )

( Open_setLatt T is lower-bounded & Bottom (Open_setLatt T) = {} )

proof end;

definition

let L be D_Lattice;

{ F where F is Filter of L : ( F <> the carrier of L & F is prime ) } is set ;

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

{ F where F is Filter of L : ( F <> the carrier of L & F is prime ) } is set ;

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

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 Th10: :: OPENLATT:10

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

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;

ex b_{1} being Function st

for a being Element of L holds

( dom b_{1} = the carrier of L & b_{1} . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } )

for b_{1}, b_{2} being Function st ( for a being Element of L holds

( dom b_{1} = the carrier of L & b_{1} . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } ) ) & ( for a being Element of L holds

( dom b_{2} = the carrier of L & b_{2} . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } ) ) holds

b_{1} = b_{2}

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

ex b

for a being Element of L holds

( dom b

proof end;

uniqueness for b

( dom b

( dom b

b

proof end;

:: deftheorem Def6 defines StoneH OPENLATT:def 6 :

for L being D_Lattice

for b_{2} being Function holds

( b_{2} = StoneH L iff for a being Element of L holds

( dom b_{2} = the carrier of L & b_{2} . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } ) );

for L being D_Lattice

for b

( b

( dom b

theorem Th11: :: OPENLATT:11

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

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 Th12: :: OPENLATT:12

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

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;

:: deftheorem defines StoneS OPENLATT:def 7 :

for L being D_Lattice holds StoneS L = rng (StoneH L);

for L being D_Lattice holds StoneS L = rng (StoneH L);

registration
end;

theorem Th13: :: OPENLATT:13

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 )

for x being set holds

( x in StoneS L iff ex a being Element of L st x = (StoneH L) . a )

proof end;

theorem Th14: :: OPENLATT:14

for L being D_Lattice

for a, b being Element of L holds (StoneH L) . (a "\/" b) = ((StoneH L) . a) \/ ((StoneH L) . b)

for a, b being Element of L holds (StoneH L) . (a "\/" b) = ((StoneH L) . a) \/ ((StoneH L) . b)

proof end;

theorem Th15: :: OPENLATT:15

for L being D_Lattice

for a, b being Element of L holds (StoneH L) . (a "/\" b) = ((StoneH L) . a) /\ ((StoneH L) . b)

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;

{ F where F is Filter of L : a in F } is Subset-Family of L

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

{ F where F is Filter of L : a in F } is Subset-Family of L

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

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

theorem Th16: :: OPENLATT:16

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

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;

Lm1: for L being D_Lattice

for F being Filter of L

for a, b being Element of L holds

( F in (SF_have b) \ (SF_have a) iff ( b in F & not a in F ) )

proof end;

theorem Th17: :: OPENLATT:17

for L being D_Lattice

for a, b 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 )

for a, b 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 Th18: :: OPENLATT:18

for L being D_Lattice

for a, b 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 ) )

for a, b 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 Th19: :: OPENLATT:19

for L being D_Lattice

for a, b being Element of L st not b [= a holds

<.b.) in (SF_have b) \ (SF_have a)

for a, b being Element of L st not b [= a holds

<.b.) in (SF_have b) \ (SF_have a)

proof end;

theorem Th20: :: OPENLATT:20

for L being D_Lattice

for a, b 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 )

for a, b 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 Th21: :: OPENLATT:21

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

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;

registration
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

redefine func A /\ B -> Element of StoneS L;

coherence

A /\ B is Element of StoneS L

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

definition

let L be D_Lattice;

ex b_{1} being BinOp of (StoneS L) st

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

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

b_{1} = b_{2}

ex b_{1} being BinOp of (StoneS L) st

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

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

b_{1} = b_{2}

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

ex b

for A, B being Element of StoneS L holds b

proof end;

uniqueness for b

b

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

ex b

for A, B being Element of StoneS L holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def9 defines Set_Union OPENLATT:def 9 :

for L being D_Lattice

for b_{2} being BinOp of (StoneS L) holds

( b_{2} = Set_Union L iff for A, B being Element of StoneS L holds b_{2} . (A,B) = A \/ B );

for L being D_Lattice

for b

( b

:: deftheorem Def10 defines Set_Meet OPENLATT:def 10 :

for L being D_Lattice

for b_{2} being BinOp of (StoneS L) holds

( b_{2} = Set_Meet L iff for A, B being Element of StoneS L holds b_{2} . (A,B) = A /\ B );

for L being D_Lattice

for b

( b

definition

let L be D_Lattice;

LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is Lattice by Th23;

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

LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is Lattice by Th23;

:: deftheorem defines StoneLatt OPENLATT:def 11 :

for L being D_Lattice holds StoneLatt L = LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #);

for L being D_Lattice holds StoneLatt L = LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #);

theorem :: OPENLATT:25

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

end;
:: original: StoneH

redefine func StoneH L -> Homomorphism of L, StoneLatt L;

coherence

StoneH L is Homomorphism of L, StoneLatt L

proof end;

registration

let L be D_Lattice;

coherence

for b_{1} being Function of L,(StoneLatt L) st b_{1} = StoneH L holds

b_{1} is bijective

StoneLatt L is distributive

end;
coherence

for b

b

proof end;

coherence StoneLatt L is distributive

proof end;

registration

not for b_{1} being H_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 V93() Heyting implicative for H_Lattice;

existence not for b

proof end;

definition

let H be non trivial H_Lattice;

ex b_{1} being strict TopStruct st

( the carrier of b_{1} = F_primeSet H & the topology of b_{1} = { (union A) where A is Subset of (StoneS H) : verum } )

for b_{1}, b_{2} being strict TopStruct st the carrier of b_{1} = F_primeSet H & the topology of b_{1} = { (union A) where A is Subset of (StoneS H) : verum } & the carrier of b_{2} = F_primeSet H & the topology of b_{2} = { (union A) where A is Subset of (StoneS H) : verum } holds

b_{1} = b_{2}
;

end;
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 ( the carrier of it = F_primeSet H & the topology of it = { (union A) where A is Subset of (StoneS H) : verum } );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def12 defines HTopSpace OPENLATT:def 12 :

for H being non trivial H_Lattice

for b_{2} being strict TopStruct holds

( b_{2} = HTopSpace H iff ( the carrier of b_{2} = F_primeSet H & the topology of b_{2} = { (union A) where A is Subset of (StoneS H) : verum } ) );

for H being non trivial H_Lattice

for b

( b

registration

let H be non trivial H_Lattice;

coherence

( not HTopSpace H is empty & HTopSpace H is TopSpace-like )

end;
coherence

( not HTopSpace H is empty & HTopSpace H is TopSpace-like )

proof end;

theorem :: OPENLATT:31

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)

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

theorem Th33: :: OPENLATT:33

for H being non trivial H_Lattice

for p9, q9 being Element of H holds (StoneH H) . (p9 => q9) = ((StoneH H) . p9) => ((StoneH H) . q9)

for p9, q9 being Element of H holds (StoneH H) . (p9 => q9) = ((StoneH H) . p9) => ((StoneH H) . q9)

proof end;

theorem :: OPENLATT:34