Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users

The abstract of the Mizar article:

Predicate Calculus for Boolean Valued Functions. Part IV

by
Shunichi Kobayashi, and
Yatsuka Nakamura

Received August 17, 1999

MML identifier: BVFUNC12
[ Mizar article, MML identifier index ]


environ

 vocabulary FUNCT_2, MARGREL1, PARTIT1, EQREL_1, ZF_LANG, BVFUNC_2;
 notation XBOOLE_0, SUBSET_1, MARGREL1, VALUAT_1, FRAENKEL, EQREL_1, BVFUNC_1,
      BVFUNC_2;
 constructors BVFUNC_2, BVFUNC_1;
 clusters MARGREL1, XBOOLE_0;


begin :: Chap. 1  Predicate Calculus

reserve Y for non empty set;

canceled 4;

theorem :: BVFUNC12:5
for a being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
A,B being a_partition of Y holds
'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G);

theorem :: BVFUNC12:6
for a being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
A,B being a_partition of Y holds
'not' Ex(All(a,A,G),B,G) = All(Ex('not' a,A,G),B,G);

theorem :: BVFUNC12:7
for a being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
A,B being a_partition of Y holds
'not' All(All(a,A,G),B,G) = Ex(Ex('not' a,A,G),B,G);

canceled 3;

theorem :: BVFUNC12:11
for a being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
A,B being a_partition of Y st G is independent holds
Ex(All(a,A,G),B,G) '<' Ex(Ex(a,B,G),A,G);

theorem :: BVFUNC12:12
for a being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
A,B being a_partition of Y holds
All(All(a,A,G),B,G) '<' All(Ex(a,A,G),B,G);

theorem :: BVFUNC12:13
for a being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
A,B being a_partition of Y holds
All(All(a,A,G),B,G) '<' Ex(All(a,A,G),B,G);

theorem :: BVFUNC12:14
for a being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
A,B being a_partition of Y holds
All(All(a,A,G),B,G) '<' Ex(Ex(a,A,G),B,G);

theorem :: BVFUNC12:15
for a being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
A,B being a_partition of Y holds
All(Ex(a,A,G),B,G) '<' Ex(Ex(a,A,G),B,G);

theorem :: BVFUNC12:16
for a being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
A,B being a_partition of Y holds
Ex(All(a,A,G),B,G) '<' Ex(Ex(a,A,G),B,G);


Back to top