environ
vocabularies HIDDEN, NUMBERS, XBOOLEAN, XXREAL_0, CARD_1, XBOOLE_0, SUBSET_1, MARGREL1, FUNCT_1, RELAT_1, TARSKI, FUNCOP_1, PARTIT1, EQREL_1, ZFMISC_1, SETFAM_1, BVFUNC_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XBOOLEAN, MARGREL1, RELAT_1, FUNCT_1, FUNCT_2, SETFAM_1, EQREL_1, ORDINAL1, NUMBERS, PARTIT1, XXREAL_0, FUNCOP_1;
definitions TARSKI, XBOOLE_0, MARGREL1, FUNCT_2;
theorems TARSKI, FUNCT_1, FUNCT_2, MARGREL1, EQREL_1, SETFAM_1, PARTIT1, XBOOLE_0, FUNCOP_1, XBOOLEAN, PARTFUN1;
schemes DOMAIN_1, FUNCT_2, FUNCT_1;
registrations SUBSET_1, XREAL_0, XBOOLEAN, EQREL_1, MARGREL1, FUNCT_2, RELSET_1, FUNCOP_1;
constructors HIDDEN, SETFAM_1, XXREAL_0, XREAL_0, PARTIT1, BINARITH, FUNCOP_1, RELSET_1, NUMBERS;
requirements HIDDEN, REAL, SUBSET, BOOLE, ARITHM, NUMERALS;
equalities XBOOLE_0, MARGREL1, XBOOLEAN;
expansions ;
definition
let Y be non
empty set ;
let a be
Function of
Y,
BOOLEAN;
let PA be
a_partition of
Y;
existence
ex b1 being Function of Y,BOOLEAN st
for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies b1 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies b1 . y = FALSE ) )
uniqueness
for b1, b2 being Function of Y,BOOLEAN st ( for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies b1 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies b1 . y = FALSE ) ) ) & ( for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies b2 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies b2 . y = FALSE ) ) ) holds
b1 = b2
end;
definition
let Y be non
empty set ;
let a be
Function of
Y,
BOOLEAN;
let PA be
a_partition of
Y;
existence
ex b1 being Function of Y,BOOLEAN st
for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies b1 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b1 . y = FALSE ) )
uniqueness
for b1, b2 being Function of Y,BOOLEAN st ( for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies b1 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b1 . y = FALSE ) ) ) & ( for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies b2 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b2 . y = FALSE ) ) ) holds
b1 = b2
end;