environ
vocabularies HIDDEN, LATTICES, LATTICE3, SUBSET_1, STRUCT_0, EQREL_1, XBOOLE_0, PBOOLE, XXREAL_0, REWRITE1, WELLORD2, RELAT_1, ZFMISC_1, RELAT_2, ORDERS_2, TARSKI, SETFAM_1, CAT_1, YELLOW_0, WELLORD1, ORDINAL2, PRE_TOPC, RCOMP_1, PRALG_1, FUNCT_1, FUNCOP_1, CARD_3, RLVECT_2, NEWTON, FUNCT_2, SEQM_3, ORDERS_3, YELLOW_1, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, RELSET_1, SETFAM_1, FUNCT_1, WELLORD2, ORDERS_1, CARD_3, PBOOLE, TOLER_1, PARTFUN1, FUNCT_2, STRUCT_0, ORDERS_2, TOPS_2, LATTICES, ORDERS_3, LATTICE3, PRE_TOPC, FUNCOP_1, PRALG_1, YELLOW_0;
definitions LATTICE3, XBOOLE_0, TOPS_2, TARSKI, RELAT_1, PRALG_1;
theorems TARSKI, LATTICES, LATTICE3, YELLOW_0, STRUCT_0, RELAT_1, ORDERS_2, RELSET_1, ZFMISC_1, WELLORD2, SETFAM_1, PRE_TOPC, FUNCT_1, FUNCOP_1, PBOOLE, CARD_3, FUNCT_2, PRALG_1, ORDERS_3, XBOOLE_0, XBOOLE_1, PARTFUN1;
schemes RELSET_1, FUNCT_2;
registrations SUBSET_1, RELSET_1, PARTFUN1, FUNCOP_1, STRUCT_0, LATTICES, PRE_TOPC, ORDERS_2, LATTICE3, YELLOW_0;
constructors HIDDEN, SETFAM_1, WELLORD2, TOLER_1, TOPS_2, LATTICE3, YELLOW_0, PRALG_1, ORDERS_3, CARD_3, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities LATTICE3, XBOOLE_0, RELAT_1;
expansions LATTICE3, XBOOLE_0, TOPS_2, TARSKI;
Lm1:
for X being set
for x, y being Element of (BoolePoset X) holds
( x /\ y in bool X & x \/ y in bool X )
Lm2:
for T being non empty TopSpace holds InclPoset the topology of T is lower-bounded
Lm3:
for T being non empty TopSpace holds InclPoset the topology of T is complete
Lm4:
for T being non empty TopSpace holds not InclPoset the topology of T is trivial
definition
let I be
set ;
let J be
RelStr-yielding ManySortedSet of
I;
existence
ex b1 being strict RelStr st
( the carrier of b1 = product (Carrier J) & ( for x, y being Element of b1 st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being object st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) )
uniqueness
for b1, b2 being strict RelStr st the carrier of b1 = product (Carrier J) & ( for x, y being Element of b1 st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being object st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) & the carrier of b2 = product (Carrier J) & ( for x, y being Element of b2 st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being object st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) holds
b1 = b2
end;
Lm5:
for X being set
for Y being non empty RelStr
for x being Element of (Y |^ X) holds
( x in the carrier of (product (X --> Y)) & x is Function of X, the carrier of Y )