The Mizar article:

Predicate Calculus for Boolean Valued Functions. Part IV

by
Shunichi Kobayashi, and
Yatsuka Nakamura

Received August 17, 1999

Copyright (c) 1999 Association of Mizar Users

MML identifier: BVFUNC12
[ 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;
 theorems BVFUNC_1, BVFUNC_2, PARTIT_2, BVFUNC_4;

begin :: Chap. 1  Predicate Calculus

reserve Y for non empty set;

canceled 4;

theorem 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)
proof
  let a be Element of Funcs(Y,BOOLEAN);
  let G be Subset of PARTITIONS(Y);
  let A,B be a_partition of Y;
    'not' All(Ex(a,A,G),B,G) = Ex('not' Ex(a,A,G),B,G) by BVFUNC_2:20;
  hence thesis by BVFUNC_2:21;
end;

theorem 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)
proof
  let a be Element of Funcs(Y,BOOLEAN);
  let G be Subset of PARTITIONS(Y);
  let A,B be a_partition of Y;
    'not' Ex(All(a,A,G),B,G) = All('not' All(a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by BVFUNC_2:20;
end;

theorem 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)
proof
  let a be Element of Funcs(Y,BOOLEAN);
  let G be Subset of PARTITIONS(Y);
  let A,B be a_partition of Y;
    Ex('not' All(a,A,G),B,G) = Ex(Ex('not' a,A,G),B,G) by BVFUNC_2:20;
  hence thesis by BVFUNC_2:20;
end;

Lm1:
 for a,b being Element of Funcs(Y,BOOLEAN),
     G being Subset of PARTITIONS(Y),
     P being a_partition of Y st a '<' b holds
 All(a,P,G) '<' Ex(b,P,G)
 proof
  let a,b be Element of Funcs(Y,BOOLEAN),
      G be Subset of PARTITIONS(Y),
      P be a_partition of Y;
  assume a '<' b;
then A1:All(a,P,G) '<' All(b,P,G) by PARTIT_2:13;
    All(b,P,G) '<' Ex(b,P,G) by BVFUNC_4:18;
  hence thesis by A1,BVFUNC_1:18;
 end;

canceled 3;

theorem 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)
proof
  let a be Element of Funcs(Y,BOOLEAN);
  let G be Subset of PARTITIONS(Y);
  let A,B be a_partition of Y;
  assume G is independent;
then A1:Ex(Ex(a,B,G),A,G) = Ex(Ex(a,A,G),B,G) by PARTIT_2:18;
    All(a,A,G) '<' Ex(a,A,G) by Lm1;
  hence thesis by A1,PARTIT_2:15;
end;

theorem 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)
proof
  let a be Element of Funcs(Y,BOOLEAN);
  let G be Subset of PARTITIONS(Y);
  let A,B be a_partition of Y;
    All(a,A,G) '<' Ex(a,A,G) by Lm1;
  hence thesis by PARTIT_2:13;
end;

theorem 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) by Lm1;

theorem 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)
proof
  let a be Element of Funcs(Y,BOOLEAN);
  let G be Subset of PARTITIONS(Y);
  let A,B be a_partition of Y;
    All(a,A,G) '<' Ex(a,A,G) by Lm1;
  hence thesis by Lm1;
end;

theorem 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) by Lm1;

theorem 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)
proof
  let a be Element of Funcs(Y,BOOLEAN);
  let G be Subset of PARTITIONS(Y);
  let A,B be a_partition of Y;
    All(a,A,G) '<' Ex(a,A,G) by Lm1;
  hence thesis by PARTIT_2:15;
end;


Back to top