begin
:: deftheorem Def1 defines ,... WAYBEL17:def 1 :
for S being non empty set
for a, b being Element of S
for b4 being Function of NAT,S holds
( b4 = (a,b) ,... iff for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies b4 . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies b4 . i = b ) ) );
theorem Th1:
theorem
Lm1:
for T being up-complete LATTICE
for x being Element of T holds downarrow x is closed_under_directed_sups
Lm2:
for T being up-complete Scott TopLattice
for x being Element of T holds Cl {x} = downarrow x
Lm3:
for T being up-complete Scott TopLattice
for x being Element of T holds downarrow x is closed
theorem Th3:
theorem Th4:
Lm4:
for S, T being non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopRelStr
for f being Function of S,T st f is directed-sups-preserving holds
f is continuous
begin
definition
let S,
T be
up-complete Scott TopLattice;
func SCMaps (
S,
T)
-> strict full SubRelStr of
MonMaps (
S,
T)
means :
Def2:
for
f being
Function of
S,
T holds
(
f in the
carrier of
it iff
f is
continuous );
existence
ex b1 being strict full SubRelStr of MonMaps (S,T) st
for f being Function of S,T holds
( f in the carrier of b1 iff f is continuous )
uniqueness
for b1, b2 being strict full SubRelStr of MonMaps (S,T) st ( for f being Function of S,T holds
( f in the carrier of b1 iff f is continuous ) ) & ( for f being Function of S,T holds
( f in the carrier of b2 iff f is continuous ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines SCMaps WAYBEL17:def 2 :
for S, T being up-complete Scott TopLattice
for b3 being strict full SubRelStr of MonMaps (S,T) holds
( b3 = SCMaps (S,T) iff for f being Function of S,T holds
( f in the carrier of b3 iff f is continuous ) );
begin
definition
let S be non
empty RelStr ;
let a,
b be
Element of
S;
func Net-Str (
a,
b)
-> non
empty strict NetStr of
S means :
Def3:
( the
carrier of
it = NAT & the
mapping of
it = (
a,
b)
,... & ( for
i,
j being
Element of
it for
i9,
j9 being
Element of
NAT st
i = i9 &
j = j9 holds
(
i <= j iff
i9 <= j9 ) ) );
existence
ex b1 being non empty strict NetStr of S st
( the carrier of b1 = NAT & the mapping of b1 = (a,b) ,... & ( for i, j being Element of b1
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 ) ) )
uniqueness
for b1, b2 being non empty strict NetStr of S st the carrier of b1 = NAT & the mapping of b1 = (a,b) ,... & ( for i, j being Element of b1
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 ) ) & the carrier of b2 = NAT & the mapping of b2 = (a,b) ,... & ( for i, j being Element of b2
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 ) ) holds
b1 = b2
end;
:: deftheorem Def3 defines Net-Str WAYBEL17:def 3 :
for S being non empty RelStr
for a, b being Element of S
for b4 being non empty strict NetStr of S holds
( b4 = Net-Str (a,b) iff ( the carrier of b4 = NAT & the mapping of b4 = (a,b) ,... & ( for i, j being Element of b4
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 ) ) ) );
theorem Th5:
theorem Th6:
theorem Th7:
Lm5:
for S being with_infima Poset
for a, b being Element of S st a <= b holds
lim_inf (Net-Str (a,b)) = a
theorem Th8:
:: deftheorem defines Net-Str WAYBEL17:def 4 :
for S being non empty RelStr
for D being non empty Subset of S holds Net-Str D = NetStr(# D,( the InternalRel of S |_2 D),((id the carrier of S) | D) #);
theorem Th9:
Lm6:
for R being up-complete LATTICE
for N being reflexive monotone net of R holds lim_inf N = sup N
theorem Th10:
begin
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem
Lm7:
for S, T being complete LATTICE
for D being Subset of S
for f being Function of S,T st f is monotone holds
f . ("/\" (D,S)) <= inf (f .: D)
theorem Th18:
theorem
Lm8:
for S, T being complete LATTICE
for f being Function of S,T st ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) holds
f is directed-sups-preserving
theorem Th20:
Lm9:
for S, T being complete Scott TopLattice
for f being continuous Function of S,T
for N being net of S holds f . (lim_inf N) <= lim_inf (f * N)
Lm10:
for L being continuous Scott TopLattice
for p being Element of L
for S being Subset of L st S is open & p in S holds
ex q being Element of L st
( q << p & q in S )
Lm11:
for L being lower-bounded continuous Scott TopLattice
for x being Element of L holds wayabove x is open
Lm12:
for L being lower-bounded continuous Scott TopLattice
for p being Element of L holds { (wayabove q) where q is Element of L : q << p } is Basis of
Lm13:
for T being lower-bounded continuous Scott TopLattice holds { (wayabove x) where x is Element of T : verum } is Basis of T
Lm14:
for T being lower-bounded continuous Scott TopLattice
for S being Subset of T holds Int S = union { (wayabove x) where x is Element of T : wayabove x c= S }
Lm15:
for S, T being lower-bounded continuous Scott TopLattice
for f being Function of S,T st ( for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) ) holds
f is continuous
begin
theorem
theorem Th22:
Lm16:
for S, T being complete continuous Scott TopLattice
for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds
f is directed-sups-preserving
theorem Th23:
theorem Th24:
Lm17:
for S, T being complete Scott TopLattice
for f being Function of S,T st S is algebraic & T is algebraic & ( for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) ) holds
for x being Element of S
for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) )
Lm18:
for S, T being complete Scott TopLattice
for f being Function of S,T st T is algebraic & ( for x being Element of S
for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ) holds
for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )
Lm19:
for S, T being complete Scott TopLattice
for f being Function of S,T st S is algebraic & T is algebraic & ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds
for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T)
theorem Th25:
theorem Th26:
theorem
theorem
theorem