environ
vocabularies HIDDEN, XBOOLE_0, SUBSET_1, FUNCT_1, NUMBERS, RELAT_1, TARSKI, WAYBEL_9, STRUCT_0, WAYBEL_0, RELAT_2, ORDERS_2, SEQM_3, XXREAL_0, WAYBEL11, YELLOW_0, LATTICE3, ORDINAL2, PRE_TOPC, RCOMP_1, FUNCOP_1, WAYBEL_3, REWRITE1, NEWTON, CARD_3, CAT_1, YELLOW_1, FUNCT_2, ARYTM_3, LATTICES, WELLORD1, YELLOW_2, EQREL_1, CARD_FIL, RLVECT_3, ZFMISC_1, SETFAM_1, YELLOW_8, TOPS_1, WAYBEL_8, WAYBEL17, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, RELAT_1, SETFAM_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, FUNCT_3, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, TOLER_1, ORDERS_2, LATTICE3, YELLOW_0, ORDERS_3, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_3, FUNCOP_1, WAYBEL_8, WAYBEL_9, WAYBEL11, WAYBEL_2, CANTOR_1, YELLOW_8, XXREAL_0;
definitions TARSKI, XBOOLE_0, WAYBEL_0, PRE_TOPC, RELAT_1, LATTICE3, YELLOW_0, WAYBEL_1, WAYBEL_3, WAYBEL11, YELLOW_8, TOPS_2;
theorems WAYBEL11, WAYBEL_0, TOPS_1, TARSKI, FUNCT_1, FUNCT_2, TOPS_2, YELLOW_0, YELLOW_2, WAYBEL_3, WAYBEL_1, RELAT_1, WAYBEL_4, ZFMISC_1, WAYBEL_2, WAYBEL_8, NAT_1, ORDERS_2, SCHEME1, WAYBEL_9, FUNCT_3, WAYBEL13, YELLOW_8, YELLOW_1, FUNCOP_1, WAYBEL10, RELSET_1, SETFAM_1, XBOOLE_0, XBOOLE_1, XXREAL_0, EQREL_1;
schemes PARTFUN1, RELSET_1, FRAENKEL, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, FUNCT_2, FUNCOP_1, MEMBERED, ABIAN, STRUCT_0, TOPS_1, LATTICE3, WAYBEL_0, YELLOW_1, WAYBEL_2, WAYBEL_3, WAYBEL_9, WAYBEL10, WAYBEL11, PRE_TOPC, RELSET_1, XXREAL_0, NAT_1;
constructors HIDDEN, DOMAIN_1, NAT_1, TOLER_1, ABIAN, TOPS_1, NATTRA_1, LATTICE3, CANTOR_1, ORDERS_3, WAYBEL_1, WAYBEL_3, WAYBEL_8, YELLOW_8, WAYBEL11, MEMBERED, RELSET_1, TOPS_2, WAYBEL_2;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities WAYBEL_0, WAYBEL_3, WAYBEL11, WELLORD1, SUBSET_1, STRUCT_0;
expansions TARSKI, XBOOLE_0, WAYBEL_0, PRE_TOPC, LATTICE3, WAYBEL_1, WAYBEL_3, WAYBEL11;
Lm1:
for T being up-complete LATTICE
for x being Element of T holds downarrow x is directly_closed
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
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
definition
let S be non
empty RelStr ;
let a,
b be
Element of
S;
existence
ex b1 being non empty strict NetStr over 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 over 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;
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
Lm6:
for R being up-complete LATTICE
for N being reflexive monotone net of R holds lim_inf N = sup N
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)
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
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
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
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)