:: by Grzegorz Bancerek

::

:: Received June 21, 1998

:: Copyright (c) 1998-2016 Association of Mizar Users

:: deftheorem Def1 defines lower WAYBEL19:def 1 :

for T being non empty TopRelStr holds

( T is lower iff { ((uparrow x) `) where x is Element of T : verum } is prebasis of T );

for T being non empty TopRelStr holds

( T is lower iff { ((uparrow x) `) where x is Element of T : verum } is prebasis of T );

Lm1: now :: thesis: for LL, T being non empty RelStr st RelStr(# the carrier of LL, the InternalRel of LL #) = RelStr(# the carrier of T, the InternalRel of T #) holds

{ ((uparrow x) `) where x is Element of LL : verum } = { ((uparrow x) `) where x is Element of T : verum }

{ ((uparrow x) `) where x is Element of LL : verum } = { ((uparrow x) `) where x is Element of T : verum }

let LL, T be non empty RelStr ; :: thesis: ( RelStr(# the carrier of LL, the InternalRel of LL #) = RelStr(# the carrier of T, the InternalRel of T #) implies { ((uparrow x) `) where x is Element of LL : verum } = { ((uparrow x) `) where x is Element of T : verum } )

assume A1: RelStr(# the carrier of LL, the InternalRel of LL #) = RelStr(# the carrier of T, the InternalRel of T #) ; :: thesis: { ((uparrow x) `) where x is Element of LL : verum } = { ((uparrow x) `) where x is Element of T : verum }

set BB = { ((uparrow x) `) where x is Element of T : verum } ;

set A = { ((uparrow x) `) where x is Element of LL : verum } ;

thus { ((uparrow x) `) where x is Element of LL : verum } = { ((uparrow x) `) where x is Element of T : verum } :: thesis: verum

end;
assume A1: RelStr(# the carrier of LL, the InternalRel of LL #) = RelStr(# the carrier of T, the InternalRel of T #) ; :: thesis: { ((uparrow x) `) where x is Element of LL : verum } = { ((uparrow x) `) where x is Element of T : verum }

set BB = { ((uparrow x) `) where x is Element of T : verum } ;

set A = { ((uparrow x) `) where x is Element of LL : verum } ;

thus { ((uparrow x) `) where x is Element of LL : verum } = { ((uparrow x) `) where x is Element of T : verum } :: thesis: verum

proof

assume a in { ((uparrow x) `) where x is Element of T : verum } ; :: thesis: a in { ((uparrow x) `) where x is Element of LL : verum }

then consider x being Element of T such that

A3: a = (uparrow x) ` ;

reconsider y = x as Element of LL by A1;

a = (uparrow y) ` by A1, A3, WAYBEL_0:13;

hence a in { ((uparrow x) `) where x is Element of LL : verum } ; :: thesis: verum

end;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { ((uparrow x) `) where x is Element of T : verum } c= { ((uparrow x) `) where x is Element of LL : verum }

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((uparrow x) `) where x is Element of T : verum } or a in { ((uparrow x) `) where x is Element of LL : verum } )
let a be object ; :: thesis: ( a in { ((uparrow x) `) where x is Element of LL : verum } implies a in { ((uparrow x) `) where x is Element of T : verum } )

assume a in { ((uparrow x) `) where x is Element of LL : verum } ; :: thesis: a in { ((uparrow x) `) where x is Element of T : verum }

then consider x being Element of LL such that

A2: a = (uparrow x) ` ;

reconsider y = x as Element of T by A1;

a = (uparrow y) ` by A1, A2, WAYBEL_0:13;

hence a in { ((uparrow x) `) where x is Element of T : verum } ; :: thesis: verum

end;
assume a in { ((uparrow x) `) where x is Element of LL : verum } ; :: thesis: a in { ((uparrow x) `) where x is Element of T : verum }

then consider x being Element of LL such that

A2: a = (uparrow x) ` ;

reconsider y = x as Element of T by A1;

a = (uparrow y) ` by A1, A2, WAYBEL_0:13;

hence a in { ((uparrow x) `) where x is Element of T : verum } ; :: thesis: verum

assume a in { ((uparrow x) `) where x is Element of T : verum } ; :: thesis: a in { ((uparrow x) `) where x is Element of LL : verum }

then consider x being Element of T such that

A3: a = (uparrow x) ` ;

reconsider y = x as Element of LL by A1;

a = (uparrow y) ` by A1, A3, WAYBEL_0:13;

hence a in { ((uparrow x) `) where x is Element of LL : verum } ; :: thesis: verum

registration

for b_{1} being 1 -element TopSpace-like reflexive TopRelStr holds b_{1} is lower
end;

cluster 1 -element TopSpace-like reflexive -> 1 -element TopSpace-like reflexive lower for TopRelStr ;

coherence for b

proof end;

registration

ex b_{1} being TopLattice st

( b_{1} is lower & b_{1} is trivial & b_{1} is complete & b_{1} is strict )
end;

cluster non empty trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete strict non void lower for TopRelStr ;

existence ex b

( b

proof end;

registration

let R be non empty RelStr ;

existence

ex b_{1} being correct strict TopAugmentation of R st b_{1} is lower
by Th1;

end;
existence

ex b

theorem Th2: :: WAYBEL19:2

for L1, L2 being non empty TopSpace-like lower TopRelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds

the topology of L1 = the topology of L2

the topology of L1 = the topology of L2

proof end;

definition

let R be non empty RelStr ;

for b_{1}, b_{2} being Subset-Family of R st ( for T being correct lower TopAugmentation of R holds b_{1} = the topology of T ) & ( for T being correct lower TopAugmentation of R holds b_{2} = the topology of T ) holds

b_{1} = b_{2}

ex b_{1} being Subset-Family of R st

for T being correct lower TopAugmentation of R holds b_{1} = the topology of T

end;
func omega R -> Subset-Family of R means :Def2: :: WAYBEL19:def 2

for T being correct lower TopAugmentation of R holds it = the topology of T;

uniqueness for T being correct lower TopAugmentation of R holds it = the topology of T;

for b

b

proof end;

existence ex b

for T being correct lower TopAugmentation of R holds b

proof end;

:: deftheorem Def2 defines omega WAYBEL19:def 2 :

for R being non empty RelStr

for b_{2} being Subset-Family of R holds

( b_{2} = omega R iff for T being correct lower TopAugmentation of R holds b_{2} = the topology of T );

for R being non empty RelStr

for b

( b

theorem Th3: :: WAYBEL19:3

for R1, R2 being non empty RelStr st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds

omega R1 = omega R2

omega R1 = omega R2

proof end;

theorem Th4: :: WAYBEL19:4

for T being non empty lower TopRelStr

for x being Point of T holds

( (uparrow x) ` is open & uparrow x is closed )

for x being Point of T holds

( (uparrow x) ` is open & uparrow x is closed )

proof end;

theorem Th5: :: WAYBEL19:5

for T being non empty transitive lower TopRelStr

for A being Subset of T st A is open holds

A is lower

for A being Subset of T st A is open holds

A is lower

proof end;

theorem Th6: :: WAYBEL19:6

for T being non empty transitive lower TopRelStr

for A being Subset of T st A is closed holds

A is upper

for A being Subset of T st A is closed holds

A is upper

proof end;

theorem Th7: :: WAYBEL19:7

for T being non empty TopSpace-like TopRelStr holds

( T is lower iff { ((uparrow F) `) where F is Subset of T : F is finite } is Basis of T )

( T is lower iff { ((uparrow F) `) where F is Subset of T : F is finite } is Basis of T )

proof end;

theorem Th8: :: WAYBEL19:8

for S, T being complete lower TopLattice

for f being Function of S,T st ( for X being non empty Subset of S holds f preserves_inf_of X ) holds

f is continuous

for f being Function of S,T st ( for X being non empty Subset of S holds f preserves_inf_of X ) holds

f is continuous

proof end;

theorem Th9: :: WAYBEL19:9

for S, T being complete lower TopLattice

for f being Function of S,T st f is infs-preserving holds

f is continuous

for f being Function of S,T st f is infs-preserving holds

f is continuous

proof end;

theorem Th10: :: WAYBEL19:10

for T being complete lower TopLattice

for BB being prebasis of T

for F being non empty filtered Subset of T st ( for A being Subset of T st A in BB & inf F in A holds

F meets A ) holds

inf F in Cl F

for BB being prebasis of T

for F being non empty filtered Subset of T st ( for A being Subset of T st A in BB & inf F in A holds

F meets A ) holds

inf F in Cl F

proof end;

theorem Th11: :: WAYBEL19:11

for S, T being complete lower TopLattice

for f being Function of S,T st f is continuous holds

f is filtered-infs-preserving

for f being Function of S,T st f is continuous holds

f is filtered-infs-preserving

proof end;

theorem :: WAYBEL19:12

for S, T being complete lower TopLattice

for f being Function of S,T st f is continuous & ( for X being finite Subset of S holds f preserves_inf_of X ) holds

f is infs-preserving

for f being Function of S,T st f is continuous & ( for X being finite Subset of S holds f preserves_inf_of X ) holds

f is infs-preserving

proof end;

theorem :: WAYBEL19:13

for T being non empty TopSpace-like reflexive transitive lower TopRelStr

for x being Point of T holds Cl {x} = uparrow x

for x being Point of T holds Cl {x} = uparrow x

proof end;

registration

for b_{1} being non empty TopPoset st b_{1} is lower holds

b_{1} is T_0
end;

cluster non empty TopSpace-like reflexive transitive antisymmetric lower -> non empty T_0 for TopRelStr ;

coherence for b

b

proof end;

registration

let R be non empty lower-bounded RelStr ;

coherence

for b_{1} being TopAugmentation of R holds b_{1} is lower-bounded

end;
coherence

for b

proof end;

theorem Th14: :: WAYBEL19:14

for S, T being non empty RelStr

for s being Element of S

for t being Element of T holds (uparrow [s,t]) ` = [:((uparrow s) `), the carrier of T:] \/ [: the carrier of S,((uparrow t) `):]

for s being Element of S

for t being Element of T holds (uparrow [s,t]) ` = [:((uparrow s) `), the carrier of T:] \/ [: the carrier of S,((uparrow t) `):]

proof end;

theorem Th15: :: WAYBEL19:15

for S, T being non empty lower-bounded Poset

for S9 being correct lower TopAugmentation of S

for T9 being correct lower TopAugmentation of T holds omega [:S,T:] = the topology of [:S9,T9:]

for S9 being correct lower TopAugmentation of S

for T9 being correct lower TopAugmentation of T holds omega [:S,T:] = the topology of [:S9,T9:]

proof end;

theorem :: WAYBEL19:17

for T, T2 being complete lower TopLattice st T2 is TopAugmentation of [:T,T:] holds

for f being Function of T2,T st f = inf_op T holds

f is continuous

for f being Function of T2,T st f = inf_op T holds

f is continuous

proof end;

scheme :: WAYBEL19:sch 1

TopInd{ F_{1}() -> TopLattice, P_{1}[ set ] } :

provided

TopInd{ F

provided

A1:
ex K being prebasis of F_{1}() st

for A being Subset of F_{1}() st A in K holds

P_{1}[A]
and

A2: for F being Subset-Family of F_{1}() st ( for A being Subset of F_{1}() st A in F holds

P_{1}[A] ) holds

P_{1}[ union F]
and

A3: for A1, A2 being Subset of F_{1}() st P_{1}[A1] & P_{1}[A2] holds

P_{1}[A1 /\ A2]
and

A4: P_{1}[ [#] F_{1}()]

for A being Subset of F

P

A2: for F being Subset-Family of F

P

P

A3: for A1, A2 being Subset of F

P

A4: P

proof end;

theorem :: WAYBEL19:18

for L1, L2 being non empty reflexive antisymmetric up-complete RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & ( for x being Element of L1 holds

( waybelow x is directed & not waybelow x is empty ) ) & L1 is satisfying_axiom_of_approximation holds

L2 is satisfying_axiom_of_approximation

( waybelow x is directed & not waybelow x is empty ) ) & L1 is satisfying_axiom_of_approximation holds

L2 is satisfying_axiom_of_approximation

proof end;

registration

let T be non empty continuous Poset;

coherence

for b_{1} being TopAugmentation of T holds b_{1} is continuous

end;
coherence

for b

proof end;

theorem Th19: :: WAYBEL19:19

for T, S being TopSpace

for R being Refinement of T,S

for W being Subset of R st ( W in the topology of T or W in the topology of S ) holds

W is open

for R being Refinement of T,S

for W being Subset of R st ( W in the topology of T or W in the topology of S ) holds

W is open

proof end;

theorem Th21: :: WAYBEL19:21

for T, S being TopSpace st the carrier of T = the carrier of S holds

for R being Refinement of T,S

for V being Subset of T

for W being Subset of R st W = V & V is closed holds

W is closed

for R being Refinement of T,S

for V being Subset of T

for W being Subset of R st W = V & V is closed holds

W is closed

proof end;

theorem Th22: :: WAYBEL19:22

for T being non empty TopSpace

for K, O being set st K c= O & O c= the topology of T holds

( ( K is Basis of T implies O is Basis of T ) & ( K is prebasis of T implies O is prebasis of T ) )

for K, O being set st K c= O & O c= the topology of T holds

( ( K is Basis of T implies O is Basis of T ) & ( K is prebasis of T implies O is prebasis of T ) )

proof end;

theorem Th23: :: WAYBEL19:23

for T1, T2 being non empty TopSpace st the carrier of T1 = the carrier of T2 holds

for T being Refinement of T1,T2

for B1 being prebasis of T1

for B2 being prebasis of T2 holds B1 \/ B2 is prebasis of T

for T being Refinement of T1,T2

for B1 being prebasis of T1

for B2 being prebasis of T2 holds B1 \/ B2 is prebasis of T

proof end;

theorem :: WAYBEL19:24

for T1, S1, T2, S2 being non empty TopSpace

for R1 being Refinement of T1,S1

for R2 being Refinement of T2,S2

for f being Function of T1,T2

for g being Function of S1,S2

for h being Function of R1,R2 st h = f & h = g & f is continuous & g is continuous holds

h is continuous

for R1 being Refinement of T1,S1

for R2 being Refinement of T2,S2

for f being Function of T1,T2

for g being Function of S1,S2

for h being Function of R1,R2 st h = f & h = g & f is continuous & g is continuous holds

h is continuous

proof end;

theorem Th25: :: WAYBEL19:25

for T being non empty TopSpace

for K being prebasis of T

for N being net of T

for p being Point of T st ( for A being Subset of T st p in A & A in K holds

N is_eventually_in A ) holds

p in Lim N

for K being prebasis of T

for N being net of T

for p being Point of T st ( for A being Subset of T st p in A & A in K holds

N is_eventually_in A ) holds

p in Lim N

proof end;

theorem Th26: :: WAYBEL19:26

for T being non empty TopSpace

for N being net of T

for S being Subset of T st N is_eventually_in S holds

Lim N c= Cl S

for N being net of T

for S being Subset of T st N is_eventually_in S holds

Lim N c= Cl S

proof end;

theorem Th27: :: WAYBEL19:27

for R being non empty RelStr

for X being non empty Subset of R holds

( the mapping of (X +id) = id X & the mapping of (X opp+id) = id X )

for X being non empty Subset of R holds

( the mapping of (X +id) = id X & the mapping of (X opp+id) = id X )

proof end;

theorem Th28: :: WAYBEL19:28

for R being non empty reflexive antisymmetric RelStr

for x being Element of R holds (uparrow x) /\ (downarrow x) = {x}

for x being Element of R holds (uparrow x) /\ (downarrow x) = {x}

proof end;

:: deftheorem Def3 defines Lawson WAYBEL19:def 3 :

for T being non empty reflexive TopRelStr holds

( T is Lawson iff (omega T) \/ (sigma T) is prebasis of T );

for T being non empty reflexive TopRelStr holds

( T is Lawson iff (omega T) \/ (sigma T) is prebasis of T );

theorem Th29: :: WAYBEL19:29

for R being complete LATTICE

for LL being correct lower TopAugmentation of R

for S being Scott TopAugmentation of R

for T being correct TopAugmentation of R holds

( T is Lawson iff T is Refinement of S,LL )

for LL being correct lower TopAugmentation of R

for S being Scott TopAugmentation of R

for T being correct TopAugmentation of R holds

( T is Lawson iff T is Refinement of S,LL )

proof end;

registration

let R be complete LATTICE;

ex b_{1} being TopAugmentation of R st

( b_{1} is Lawson & b_{1} is strict & b_{1} is correct )

end;
cluster non empty correct reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V199() up-complete /\-complete strict non void Lawson for TopAugmentation of R;

existence ex b

( b

proof end;

registration

ex b_{1} being TopLattice st

( b_{1} is Scott & b_{1} is complete & b_{1} is strict )

ex b_{1} being complete strict TopLattice st

( b_{1} is Lawson & b_{1} is continuous )
end;

cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete strict Scott non void for TopRelStr ;

existence ex b

( b

proof end;

cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V199() continuous up-complete /\-complete strict non void Lawson for TopRelStr ;

existence ex b

( b

proof end;

theorem Th30: :: WAYBEL19:30

for T being complete Lawson TopLattice holds (sigma T) \/ { ((uparrow x) `) where x is Element of T : verum } is prebasis of T

proof end;

theorem :: WAYBEL19:31

for T being complete Lawson TopLattice holds (sigma T) \/ { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } is prebasis of T

proof end;

theorem :: WAYBEL19:32

for T being complete Lawson TopLattice holds { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } is Basis of T

proof end;

definition

let T be complete LATTICE;

for b_{1}, b_{2} being Subset-Family of T st ( for S being correct Lawson TopAugmentation of T holds b_{1} = the topology of S ) & ( for S being correct Lawson TopAugmentation of T holds b_{2} = the topology of S ) holds

b_{1} = b_{2}

ex b_{1} being Subset-Family of T st

for S being correct Lawson TopAugmentation of T holds b_{1} = the topology of S

end;
func lambda T -> Subset-Family of T means :Def4: :: WAYBEL19:def 4

for S being correct Lawson TopAugmentation of T holds it = the topology of S;

uniqueness for S being correct Lawson TopAugmentation of T holds it = the topology of S;

for b

b

proof end;

existence ex b

for S being correct Lawson TopAugmentation of T holds b

proof end;

:: deftheorem Def4 defines lambda WAYBEL19:def 4 :

for T being complete LATTICE

for b_{2} being Subset-Family of T holds

( b_{2} = lambda T iff for S being correct Lawson TopAugmentation of T holds b_{2} = the topology of S );

for T being complete LATTICE

for b

( b

theorem :: WAYBEL19:34

for R being complete LATTICE

for T being correct lower TopAugmentation of R

for S being correct Scott TopAugmentation of R

for M being Refinement of S,T holds lambda R = the topology of M

for T being correct lower TopAugmentation of R

for S being correct Scott TopAugmentation of R

for M being Refinement of S,T holds lambda R = the topology of M

proof end;

Lm2: for T being LATTICE

for F being Subset-Family of T st ( for A being Subset of T st A in F holds

A is property(S) ) holds

union F is property(S)

proof end;

Lm3: for T being LATTICE

for A1, A2 being Subset of T st A1 is property(S) & A2 is property(S) holds

A1 /\ A2 is property(S)

proof end;

Lm4: for T being LATTICE holds [#] T is property(S)

proof end;

theorem Th35: :: WAYBEL19:35

for T being up-complete lower TopLattice

for A being Subset of T st A is open holds

A is property(S)

for A being Subset of T st A is open holds

A is property(S)

proof end;

theorem Th37: :: WAYBEL19:37

for S being complete Scott TopLattice

for T being correct Lawson TopAugmentation of S

for A being Subset of S st A is open holds

for C being Subset of T st C = A holds

C is open

for T being correct Lawson TopAugmentation of S

for A being Subset of S st A is open holds

for C being Subset of T st C = A holds

C is open

proof end;

theorem Th38: :: WAYBEL19:38

for T being complete Lawson TopLattice

for x being Element of T holds

( uparrow x is closed & downarrow x is closed & {x} is closed )

for x being Element of T holds

( uparrow x is closed & downarrow x is closed & {x} is closed )

proof end;

theorem Th39: :: WAYBEL19:39

for T being complete Lawson TopLattice

for x being Element of T holds

( (uparrow x) ` is open & (downarrow x) ` is open & {x} ` is open )

for x being Element of T holds

( (uparrow x) ` is open & (downarrow x) ` is open & {x} ` is open )

proof end;

theorem Th40: :: WAYBEL19:40

for T being complete continuous Lawson TopLattice

for x being Element of T holds

( wayabove x is open & (wayabove x) ` is closed )

for x being Element of T holds

( wayabove x is open & (wayabove x) ` is closed )

proof end;

theorem :: WAYBEL19:41

for S being complete Scott TopLattice

for T being correct Lawson TopAugmentation of S

for A being upper Subset of T st A is open holds

for C being Subset of S st C = A holds

C is open

for T being correct Lawson TopAugmentation of S

for A being upper Subset of T st A is open holds

for C being Subset of S st C = A holds

C is open

proof end;

theorem :: WAYBEL19:42

for T being complete Lawson TopLattice

for A being lower Subset of T holds

( A is closed iff A is closed_under_directed_sups )

for A being lower Subset of T holds

( A is closed iff A is closed_under_directed_sups )

proof end;

theorem :: WAYBEL19:43

for T being complete Lawson TopLattice

for F being non empty filtered Subset of T holds Lim (F opp+id) = {(inf F)}

for F being non empty filtered Subset of T holds Lim (F opp+id) = {(inf F)}

proof end;

registration

for b_{1} being complete TopLattice st b_{1} is Lawson holds

( b_{1} is T_1 & b_{1} is compact )
end;

cluster TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Lawson -> T_1 complete compact for TopRelStr ;

coherence for b

( b

proof end;

registration

for b_{1} being complete continuous TopLattice st b_{1} is Lawson holds

b_{1} is Hausdorff
end;

cluster TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete continuous Lawson -> Hausdorff complete continuous for TopRelStr ;

coherence for b

b

proof end;