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