:: Classes of Independent Partitions
:: by Andrzej Trybulec
::
:: Received February 14, 2001
:: Copyright (c) 2001-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, SUBSET_1, MARGREL1, PARTIT1, EQREL_1, FUNCT_1,
SETFAM_1, RELAT_1, ZFMISC_1, TARSKI, RELAT_2, XBOOLEAN, BVFUNC_2,
BVFUNC_1, FUNCT_4, FUNCT_5, OPOSET_1, BINOP_1, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, MARGREL1, RELAT_1,
RELAT_2, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, BINOP_1, FUNCT_4, FUNCT_5,
EQREL_1, PARTIT1, BVFUNC_1, BVFUNC_2;
constructors SETFAM_1, FUNCT_4, XCMPLX_0, BVFUNC_1, BVFUNC_2, RELSET_1,
FUNCT_5, RELAT_2, DOMAIN_1, BINOP_1, NUMBERS;
registrations SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, EQREL_1, MARGREL1,
PARTIT1, RELSET_1, XBOOLE_0, FUNCT_2;
requirements SUBSET, BOOLE, ARITHM, NUMERALS;
begin :: Preliminaries
reserve Y for non empty set,
a for Function of Y,BOOLEAN,
G for Subset of PARTITIONS(Y),
P,Q for a_partition of Y;
definition
let Y be non empty set, G be non empty Subset of PARTITIONS Y;
redefine mode Element of G -> a_partition of Y;
end;
theorem :: PARTIT_2:1
'/\' {} PARTITIONS Y = %O Y;
theorem :: PARTIT_2:2
for R,S being Equivalence_Relation of Y holds R \/ S c= R*S;
theorem :: PARTIT_2:3
for R being Relation of Y holds R c= nabla Y;
theorem :: PARTIT_2:4
for R being Equivalence_Relation of Y holds (nabla Y)*R = nabla Y
& R*nabla Y = nabla Y;
theorem :: PARTIT_2:5
for P being a_partition of Y, x,y being Element of Y holds [x,y]
in ERl P iff x in EqClass(y,P);
theorem :: PARTIT_2:6
for P,Q,R being a_partition of Y st ERl(R) = ERl(P)*ERl(Q) for x,y
being Element of Y holds x in EqClass(y,R) iff ex z being Element of Y st x in
EqClass(z,P) & z in EqClass(y,Q);
theorem :: PARTIT_2:7
for R,S being Relation, Y being set st R is_reflexive_in Y &
S is_reflexive_in Y holds R*S is_reflexive_in Y;
theorem :: PARTIT_2:8
for R being Relation, Y being set st R is_reflexive_in Y holds Y c= field R;
theorem :: PARTIT_2:9
for Y being set, R being Relation of Y st R is_reflexive_in Y holds
Y = field R;
theorem :: PARTIT_2:10
for R,S being Equivalence_Relation of Y st R*S = S*R holds
R*S is Equivalence_Relation of Y;
begin :: Boolean-valued Functions
theorem :: PARTIT_2:11
for a,b being Function of Y,BOOLEAN st a '<' b holds
'not' b '<' 'not' a;
theorem :: PARTIT_2:12
for a,b being Function of Y,BOOLEAN, G being Subset of PARTITIONS(Y),
P being a_partition of Y st a '<' b holds All(a,P,G) '<' All(b,P,G);
theorem :: PARTIT_2:13
for a,b being Function of Y,BOOLEAN,
G being Subset of PARTITIONS(Y), P being a_partition of Y st
a '<' b holds Ex(a,P,G) '<' Ex(b,P,G);
begin
theorem :: PARTIT_2:14
G is independent implies for P,Q being Subset of PARTITIONS Y st
P c= G & Q c= G holds ERl('/\'P)*ERl('/\'Q) = ERl('/\'Q)*ERl('/\'P);
theorem :: PARTIT_2:15
G is independent implies All(All(a,P,G),Q,G) = All(All(a,Q,G),P,G);
theorem :: PARTIT_2:16
G is independent implies Ex(Ex(a,P,G),Q,G) = Ex(Ex(a,Q,G),P,G);
theorem :: PARTIT_2:17
for a being Function of Y,BOOLEAN, G being Subset of PARTITIONS(
Y), P,Q being a_partition of Y st G is independent holds Ex(All(a,P,G),Q,G) '<'
All(Ex(a,Q,G),P,G);
begin :: Moved from OPOSET_1, 2010.03.11, A.T.
reserve x,y,z for set,
S, X for non empty set,
R for Relation of X;
notation
let A,B be set;
synonym [#](A,B) for [:A,B:];
end;
definition
let A,B be set;
func {}(A,B) -> Relation of A,B equals
:: PARTIT_2:def 1
{};
redefine func [#](A,B) -> Relation of A,B;
end;
registration let A,B be set;
cluster {}(A,B) -> empty;
end;
theorem :: PARTIT_2:18
field id X = X;
theorem :: PARTIT_2:19
op1 = {[{},{}]};
theorem :: PARTIT_2:20
for A,B being set holds field {}(A,B) = {};
theorem :: PARTIT_2:21
R is_reflexive_in X implies R is reflexive & field R = X;
theorem :: PARTIT_2:22
R is_symmetric_in X implies R is symmetric;
theorem :: PARTIT_2:23
R is symmetric implies R is_symmetric_in S;
theorem :: PARTIT_2:24
R is antisymmetric implies R is_antisymmetric_in S;
theorem :: PARTIT_2:25
R is_antisymmetric_in X implies R is antisymmetric;
theorem :: PARTIT_2:26
R is transitive implies R is_transitive_in S;
theorem :: PARTIT_2:27
R is_transitive_in X implies R is transitive;
theorem :: PARTIT_2:28
R is asymmetric implies R is_asymmetric_in S;
theorem :: PARTIT_2:29
R is_asymmetric_in X implies R is asymmetric;
theorem :: PARTIT_2:30
R is irreflexive & field R c= S implies R is_irreflexive_in S;
theorem :: PARTIT_2:31
R is_irreflexive_in X implies R is irreflexive;
:: Some existence conditions on non-empty relations
registration
cluster empty -> irreflexive asymmetric transitive for Relation;
end;
:: Double negation property of the internal Complement
definition
let f be Function;
attr f is involutive means
:: PARTIT_2:def 2
for x being set st x in dom f holds f.(f.x) = x;
end;
definition
let X;
let f be UnOp of X;
redefine attr f is involutive means
:: PARTIT_2:def 3
for x being Element of X holds f.(f.x) = x;
end;
registration
cluster op1 -> involutive for Function;
end;
registration let X be set;
cluster id X -> involutive;
end;