:: by Ewa Gr\c{a}dzka

::

:: Received May 23, 2000

:: Copyright (c) 2000-2012 Association of Mizar Users

begin

:: deftheorem Def1 defines upper WAYBEL32:def 1 :

for T being non empty TopRelStr holds

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

for T being non empty TopRelStr holds

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

registration

ex b_{1} being TopLattice st

( b_{1} is Scott & b_{1} is up-complete & b_{1} is strict )
end;

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

existence ex b

( b

proof end;

definition

let T be non empty TopSpace-like reflexive TopRelStr ;

end;
attr T is order_consistent means :Def2: :: WAYBEL32:def 2

for x being Element of T holds

( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds

for V being a_neighborhood of x holds N is_eventually_in V ) );

for x being Element of T holds

( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds

for V being a_neighborhood of x holds N is_eventually_in V ) );

:: deftheorem Def2 defines order_consistent WAYBEL32:def 2 :

for T being non empty TopSpace-like reflexive TopRelStr holds

( T is order_consistent iff for x being Element of T holds

( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds

for V being a_neighborhood of x holds N is_eventually_in V ) ) );

for T being non empty TopSpace-like reflexive TopRelStr holds

( T is order_consistent iff for x being Element of T holds

( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds

for V being a_neighborhood of x holds N is_eventually_in V ) ) );

registration

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

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

coherence for b

proof end;

registration

ex b_{1} being TopLattice st

( b_{1} is upper & b_{1} is trivial & b_{1} is up-complete & b_{1} is strict )
end;

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

existence ex b

( b

proof end;

theorem Th1: :: WAYBEL32:1

for T being non empty up-complete upper TopPoset

for A being Subset of T st A is open holds

A is upper

for A being Subset of T st A is open holds

A is upper

proof end;

theorem Th3: :: WAYBEL32:3

for R being non empty reflexive transitive antisymmetric up-complete RelStr ex T being TopAugmentation of R st T is Scott

proof end;

theorem :: WAYBEL32:4

for R being non empty up-complete Poset

for T being TopAugmentation of R st T is Scott holds

T is correct ;

for T being TopAugmentation of R st T is Scott holds

T is correct ;

registration

let R be non empty reflexive transitive antisymmetric up-complete RelStr ;

coherence

for b_{1} being TopAugmentation of R st b_{1} is Scott holds

b_{1} is correct
;

end;
coherence

for b

b

registration

let R be non empty reflexive transitive antisymmetric up-complete RelStr ;

ex b_{1} being TopAugmentation of R st

( b_{1} is Scott & b_{1} is correct )

end;
cluster non empty correct reflexive transitive antisymmetric up-complete Scott for TopAugmentation of R;

existence ex b

( b

proof end;

theorem Th5: :: WAYBEL32:5

for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr

for x being Element of T holds Cl {x} = downarrow x

for x being Element of T holds Cl {x} = downarrow x

proof end;

theorem Th7: :: WAYBEL32:7

for R being /\-complete Semilattice

for Z being net of R

for D being Subset of R st D = { ("/\" ( { (Z . k) where k is Element of Z : k >= j } ,R)) where j is Element of Z : verum } holds

( not D is empty & D is directed )

for Z being net of R

for D being Subset of R st D = { ("/\" ( { (Z . k) where k is Element of Z : k >= j } ,R)) where j is Element of Z : verum } holds

( not D is empty & D is directed )

proof end;

theorem Th8: :: WAYBEL32:8

for R being /\-complete Semilattice

for S being Subset of R

for a being Element of R st a in S holds

"/\" (S,R) <= a

for S being Subset of R

for a being Element of R st a in S holds

"/\" (S,R) <= a

proof end;

theorem Th10: :: WAYBEL32:10

for R being /\-complete Semilattice

for S being Subset of R holds

( S in the topology of (ConvergenceSpace (Scott-Convergence R)) iff ( S is inaccessible & S is upper ) )

for S being Subset of R holds

( S in the topology of (ConvergenceSpace (Scott-Convergence R)) iff ( S is inaccessible & S is upper ) )

proof end;

theorem Th11: :: WAYBEL32:11

for R being up-complete /\-complete Semilattice

for T being TopAugmentation of R st the topology of T = sigma R holds

T is Scott

for T being TopAugmentation of R st the topology of T = sigma R holds

T is Scott

proof end;

registration

let R be up-complete /\-complete Semilattice;

ex b_{1} being TopAugmentation of R st

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

end;
cluster non empty correct reflexive transitive antisymmetric up-complete strict Scott for TopAugmentation of R;

existence ex b

( b

proof end;

theorem :: WAYBEL32:12

for S being up-complete /\-complete Semilattice

for T being Scott TopAugmentation of S holds sigma S = the topology of T

for T being Scott TopAugmentation of S holds sigma S = the topology of T

proof end;

theorem :: WAYBEL32:13

for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr holds T is T_0-TopSpace

proof end;

registration

let R be non empty reflexive transitive antisymmetric up-complete RelStr ;

coherence

for b_{1} being TopAugmentation of R holds b_{1} is up-complete
;

end;
coherence

for b

theorem Th14: :: WAYBEL32:14

for R being non empty reflexive transitive antisymmetric up-complete RelStr

for T being Scott TopAugmentation of R

for x being Element of T

for A being upper Subset of T st not x in A holds

(downarrow x) ` is a_neighborhood of A

for T being Scott TopAugmentation of R

for x being Element of T

for A being upper Subset of T st not x in A holds

(downarrow x) ` is a_neighborhood of A

proof end;

theorem :: WAYBEL32:15

for R being non empty reflexive transitive antisymmetric up-complete TopRelStr

for T being Scott TopAugmentation of R

for S being upper Subset of T ex F being Subset-Family of T st

( S = meet F & ( for X being Subset of T st X in F holds

X is a_neighborhood of S ) )

for T being Scott TopAugmentation of R

for S being upper Subset of T ex F being Subset-Family of T st

( S = meet F & ( for X being Subset of T st X in F holds

X is a_neighborhood of S ) )

proof end;

theorem :: WAYBEL32:16

for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr

for S being Subset of T holds

( S is open iff ( S is upper & S is property(S) ) )

for S being Subset of T holds

( S is open iff ( S is upper & S is property(S) ) )

proof end;

theorem Th17: :: WAYBEL32:17

for R being non empty reflexive transitive antisymmetric up-complete TopRelStr

for S being non empty directed Subset of R

for a being Element of R st a in S holds

a <= "\/" (S,R)

for S being non empty directed Subset of R

for a being Element of R st a in S holds

a <= "\/" (S,R)

proof end;

::Remark 1.4 (vi)

registration

let T be non empty reflexive transitive antisymmetric up-complete TopRelStr ;

coherence

for b_{1} being Subset of T st b_{1} is lower holds

b_{1} is property(S)

end;
coherence

for b

b

proof end;

theorem Th19: :: WAYBEL32:19

for R being complete connected LATTICE

for T being Scott TopAugmentation of R

for x being Element of T holds (downarrow x) ` is open

for T being Scott TopAugmentation of R

for x being Element of T holds (downarrow x) ` is open

proof end;

theorem :: WAYBEL32:20

for R being complete connected LATTICE

for T being Scott TopAugmentation of R

for S being Subset of T holds

( S is open iff ( S = the carrier of T or S in { ((downarrow x) `) where x is Element of T : verum } ) )

for T being Scott TopAugmentation of R

for S being Subset of T holds

( S is open iff ( S = the carrier of T or S in { ((downarrow x) `) where x is Element of T : verum } ) )

proof end;

registration

let R be non empty up-complete Poset;

existence

ex b_{1} being correct TopAugmentation of R st b_{1} is order_consistent ;

end;
cluster non empty correct reflexive transitive antisymmetric up-complete order_consistent for TopAugmentation of R;

correctness existence

ex b

proof end;

registration

existence

ex b_{1} being TopLattice st

( b_{1} is order_consistent & b_{1} is complete );

end;

cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete order_consistent for TopRelStr ;

correctness existence

ex b

( b

proof end;

theorem Th21: :: WAYBEL32:21

for R being non empty TopRelStr

for A being Subset of R st ( for x being Element of R holds downarrow x = Cl {x} ) & A is open holds

A is upper

for A being Subset of R st ( for x being Element of R holds downarrow x = Cl {x} ) & A is open holds

A is upper

proof end;

theorem :: WAYBEL32:22

for R being non empty TopRelStr

for A being Subset of R st ( for x being Element of R holds downarrow x = Cl {x} ) holds

for A being Subset of R st A is closed holds

A is lower

for A being Subset of R st ( for x being Element of R holds downarrow x = Cl {x} ) holds

for A being Subset of R st A is closed holds

A is lower

proof end;

definition

let S be non empty 1-sorted ;

let R be non empty RelStr ;

let f be Function of the carrier of R, the carrier of S;

ex b_{1} being non empty strict NetStr over S st

( RelStr(# the carrier of b_{1}, the InternalRel of b_{1} #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b_{1} = f )

for b_{1}, b_{2} being non empty strict NetStr over S st RelStr(# the carrier of b_{1}, the InternalRel of b_{1} #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b_{1} = f & RelStr(# the carrier of b_{2}, the InternalRel of b_{2} #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b_{2} = f holds

b_{1} = b_{2}
;

end;
let R be non empty RelStr ;

let f be Function of the carrier of R, the carrier of S;

func R *' f -> non empty strict NetStr over S means :Def3: :: WAYBEL32:def 3

( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of it = f );

existence ( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of it = f );

ex b

( RelStr(# the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def3 defines *' WAYBEL32:def 3 :

for S being non empty 1-sorted

for R being non empty RelStr

for f being Function of the carrier of R, the carrier of S

for b_{4} being non empty strict NetStr over S holds

( b_{4} = R *' f iff ( RelStr(# the carrier of b_{4}, the InternalRel of b_{4} #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b_{4} = f ) );

for S being non empty 1-sorted

for R being non empty RelStr

for f being Function of the carrier of R, the carrier of S

for b

( b

registration

let S be non empty 1-sorted ;

let R be non empty transitive RelStr ;

let f be Function of the carrier of R, the carrier of S;

coherence

R *' f is transitive

end;
let R be non empty transitive RelStr ;

let f be Function of the carrier of R, the carrier of S;

coherence

R *' f is transitive

proof end;

registration

let S be non empty 1-sorted ;

let R be non empty directed RelStr ;

let f be Function of the carrier of R, the carrier of S;

coherence

R *' f is directed

end;
let R be non empty directed RelStr ;

let f be Function of the carrier of R, the carrier of S;

coherence

R *' f is directed

proof end;

definition

let R be non empty RelStr ;

let N be prenet of R;

ex b_{1} being strict prenet of R ex f being Function of N,R st

( b_{1} = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) )

for b_{1}, b_{2} being strict prenet of R st ex f being Function of N,R st

( b_{1} = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) & ex f being Function of N,R st

( b_{2} = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) holds

b_{1} = b_{2}

end;
let N be prenet of R;

func inf_net N -> strict prenet of R means :Def4: :: WAYBEL32:def 4

ex f being Function of N,R st

( it = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) );

existence ex f being Function of N,R st

( it = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def4 defines inf_net WAYBEL32:def 4 :

for R being non empty RelStr

for N being prenet of R

for b_{3} being strict prenet of R holds

( b_{3} = inf_net N iff ex f being Function of N,R st

( b_{3} = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) );

for R being non empty RelStr

for N being prenet of R

for b

( b

( b

registration
end;

registration

let R be non empty reflexive antisymmetric /\-complete RelStr ;

let N be net of R;

coherence

inf_net N is monotone

end;
let N be net of R;

coherence

inf_net N is monotone

proof end;

registration

let R be non empty reflexive antisymmetric /\-complete RelStr ;

let N be net of R;

coherence

inf_net N is eventually-directed ;

end;
let N be net of R;

coherence

inf_net N is eventually-directed ;

theorem Th23: :: WAYBEL32:23

for R being non empty RelStr

for N being net of R holds rng the mapping of (inf_net N) = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum }

for N being net of R holds rng the mapping of (inf_net N) = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum }

proof end;

theorem :: WAYBEL32:25

for R being up-complete /\-complete LATTICE

for N being net of R

for i being Element of N holds sup (inf_net N) = lim_inf (N | i)

for N being net of R

for i being Element of N holds sup (inf_net N) = lim_inf (N | i)

proof end;

theorem Th26: :: WAYBEL32:26

for R being /\-complete Semilattice

for N being net of R

for V being upper Subset of R st inf_net N is_eventually_in V holds

N is_eventually_in V

for N being net of R

for V being upper Subset of R st inf_net N is_eventually_in V holds

N is_eventually_in V

proof end;

theorem :: WAYBEL32:27

for R being /\-complete Semilattice

for N being net of R

for V being lower Subset of R st N is_eventually_in V holds

inf_net N is_eventually_in V

for N being net of R

for V being lower Subset of R st N is_eventually_in V holds

inf_net N is_eventually_in V

proof end;

theorem Th28: :: WAYBEL32:28

for R being non empty up-complete /\-complete order_consistent TopLattice

for N being net of R

for x being Element of R st x <= lim_inf N holds

x is_a_cluster_point_of N

for N being net of R

for x being Element of R st x <= lim_inf N holds

x is_a_cluster_point_of N

proof end;

theorem :: WAYBEL32:29

for R being non empty up-complete /\-complete order_consistent TopLattice

for N being eventually-directed net of R

for x being Element of R holds

( x <= lim_inf N iff x is_a_cluster_point_of N )

for N being eventually-directed net of R

for x being Element of R holds

( x <= lim_inf N iff x is_a_cluster_point_of N )

proof end;