The Mizar abstract of PBOOLE

Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993 Association of Mizar Users
The abstract of the Mizar article:: Many-sorted Sets
by
Andrzej Trybulec
Received July 7, 1993
MML identifier: PBOOLE
[ Mizar article, MML identifier index ]
environ

 vocabulary FUNCT_1, MATRIX_1, RELAT_1, CARD_1, BOOLE, ZF_REFLE, AMI_1,
      FUNCOP_1, CAT_4, LATTICES, CQC_LANG, PBOOLE;
 notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCOP_1, CQC_LANG,
      CARD_1, AMI_1, MATRIX_1;
 constructors AMI_1, MATRIX_1, FUNCOP_1, MEMBERED, XBOOLE_0;
 clusters FUNCT_1, RELAT_1, FUNCOP_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements BOOLE, SUBSET;


begin

reserve i,e,u for set;

definition let f be Function;
 redefine attr f is empty-yielding means
:: PBOOLE:def 1
 for i st i in dom f holds f.i is empty;
end;

definition
 cluster empty-yielding Function;
end;

theorem :: PBOOLE:1
   for f being Function st f is non-empty
  holds rng f is with_non-empty_elements;

theorem :: PBOOLE:2
   for f being Function holds
  f is empty-yielding iff f = {} or rng f = { {} };

reserve I for set; :: of indices

definition let I;
 canceled;

  mode ManySortedSet of I -> Function means
:: PBOOLE:def 3
 dom it = I;
end;

reserve x,X,Y,Z,V for ManySortedSet of I;

scheme Kuratowski_Function{A()-> set, F(set) -> set}:
 ex f being ManySortedSet of A() st
  for e st e in A() holds f.e in F(e)
 provided
 for e st e in A() holds F(e) <> {};

definition let I,X,Y;
 pred X in Y means
:: PBOOLE:def 4
 for i st i in I holds X.i in Y.i;
 pred X c= Y means
:: PBOOLE:def 5
 for i st i in I holds X.i c= Y.i;
 reflexivity;
end;

definition let I be non empty set,X,Y be ManySortedSet of I;
 redefine pred X in Y;
 asymmetry;
end;

scheme PSeparation { I()-> set, A() -> ManySortedSet of I(), P[set,set] } :
  ex X being ManySortedSet of I() st
   for i being set st i in I()
    for e holds e in X.i iff e in A().i & P[i,e];

theorem :: PBOOLE:3
 (for i st i in I holds X.i = Y.i) implies X = Y;

definition
 let I;
  func [0]I -> ManySortedSet of I equals
:: PBOOLE:def 6
  I --> {};
 let X,Y;
  func X \/ Y -> ManySortedSet of I means
:: PBOOLE:def 7
 for i st i in I holds it.i = X.i \/ Y.i;
  commutativity;
  idempotence;

  func X /\ Y -> ManySortedSet of I means
:: PBOOLE:def 8
 for i st i in I holds it.i = X.i /\ Y.i;
  commutativity;
  idempotence;

  func X \ Y -> ManySortedSet of I means
:: PBOOLE:def 9
 for i st i in I holds it.i = X.i \ Y.i;
  pred X overlaps Y means
:: PBOOLE:def 10
 for i st i in I holds X.i meets Y.i;
  symmetry;
  antonym X does_not_overlap Y;
  pred X misses Y means
:: PBOOLE:def 11
 for i st i in I holds X.i misses Y.i;
  symmetry;
  antonym X meets Y;
end;

definition let I,X,Y;
 func X \+\ Y -> ManySortedSet of I equals
:: PBOOLE:def 12
  (X \ Y) \/ (Y \ X);
 commutativity;
end;

theorem :: PBOOLE:4
 for i st i in I holds (X \+\ Y).i = X.i \+\ Y.i;

theorem :: PBOOLE:5
 for i st i in I holds [0]I.i = {};

theorem :: PBOOLE:6
 (for i st i in I holds X.i = {}) implies X = [0]I;

theorem :: PBOOLE:7
 x in X or x in Y implies x in X \/ Y;

theorem :: PBOOLE:8
 x in X /\ Y iff x in X & x in Y;

theorem :: PBOOLE:9
 x in X & X c= Y implies x in Y;

theorem :: PBOOLE:10
 x in X & x in Y implies X overlaps Y;

theorem :: PBOOLE:11
 X overlaps Y implies ex x st x in X & x in Y;

theorem :: PBOOLE:12
   x in X \ Y implies x in X;

begin :: Lattice properties

theorem :: PBOOLE:13
   X c= X;

definition let I,X,Y;
 redefine pred X = Y means
:: PBOOLE:def 13
     X c= Y & Y c= X;
end;

canceled;

theorem :: PBOOLE:15
 X c= Y & Y c= Z implies X c= Z;

theorem :: PBOOLE:16
 X c= X \/ Y & Y c= X \/ Y;

theorem :: PBOOLE:17
 X /\ Y c= X & X /\ Y c= Y;

theorem :: PBOOLE:18
 X c= Z & Y c= Z implies X \/ Y c= Z;

theorem :: PBOOLE:19
 Z c= X & Z c= Y implies Z c= X /\ Y;

theorem :: PBOOLE:20
   X c= Y implies X \/ Z c= Y \/ Z & Z \/ X c= Z \/ Y;

theorem :: PBOOLE:21
 X c= Y implies X /\ Z c= Y /\ Z & Z /\ X c= Z /\ Y;

theorem :: PBOOLE:22
 X c= Y & Z c= V implies X \/ Z c= Y \/ V;

theorem :: PBOOLE:23
   X c= Y & Z c= V implies X /\ Z c= Y /\ V;

theorem :: PBOOLE:24
 X c= Y implies X \/ Y = Y & Y \/ X = Y;

theorem :: PBOOLE:25
 X c= Y implies X /\ Y = X & Y /\ X = X;

theorem :: PBOOLE:26
   X /\ Y c= X \/ Z;

theorem :: PBOOLE:27
   X c= Z implies X \/ Y /\ Z = (X \/ Y) /\ Z;

theorem :: PBOOLE:28
   X = Y \/ Z iff Y c= X & Z c= X & for V st Y c= V & Z c= V holds X c= V;

theorem :: PBOOLE:29
   X = Y /\ Z iff X c= Y & X c= Z & for V st V c= Y & V c= Z holds V c= X;

canceled 4;

theorem :: PBOOLE:34
 (X \/ Y) \/ Z = X \/ (Y \/ Z);

theorem :: PBOOLE:35
 (X /\ Y) /\ Z = X /\ (Y /\ Z);

theorem :: PBOOLE:36
 X /\ (X \/ Y) = X & (X \/ Y) /\ X = X & X /\ (Y \/ X) = X & (Y \/ X) /\ X = X;

theorem :: PBOOLE:37
 X \/ (X /\ Y) = X & (X /\ Y) \/ X = X & X \/ (Y /\ X) = X & (Y /\ X) \/ X = X;

theorem :: PBOOLE:38
 X /\ (Y \/ Z) = X /\ Y \/ X /\ Z;

theorem :: PBOOLE:39
 X \/ Y /\ Z = (X \/ Y) /\ (X \/ Z) & Y /\ Z \/ X = (Y \/ X) /\ (Z \/ X);

theorem :: PBOOLE:40
   (X /\ Y) \/ (X /\ Z) = X implies X c= Y \/ Z;

theorem :: PBOOLE:41
   (X \/ Y) /\ (X \/ Z) = X implies Y /\ Z c= X;

theorem :: PBOOLE:42
   (X /\ Y) \/ (Y /\ Z) \/ (Z /\ X) = (X \/ Y) /\ (Y \/ Z) /\ (Z \/ X);

theorem :: PBOOLE:43 :: SETWISEO:7
   X \/ Y c= Z implies X c= Z & Y c= Z;

theorem :: PBOOLE:44 :: SYSREL:4
   X c= Y /\ Z implies X c= Y & X c= Z;

theorem :: PBOOLE:45 :: SYSREL:2
   X \/ Y \/ Z = (X \/ Z) \/ (Y \/ Z) &
  X \/ (Y \/ Z) = (X \/ Y) \/ (X \/ Z);

theorem :: PBOOLE:46
   X /\ Y /\ Z = (X /\ Z) /\ (Y /\ Z) &
  X /\ (Y /\ Z) = (X /\ Y) /\ (X /\ Z);

theorem :: PBOOLE:47 :: SYSREL:3
   X \/ (X \/ Y) = X \/ Y & X \/ Y \/ Y = X \/ Y;

theorem :: PBOOLE:48
   X /\ (X /\ Y) = X /\ Y & X /\ Y /\ Y = X /\ Y;

begin :: ManySortedSet with empty components

theorem :: PBOOLE:49
 [0]I c= X;

theorem :: PBOOLE:50
 X c= [0]I implies X = [0]I;

theorem :: PBOOLE:51
 X c= Y & X c= Z & Y /\ Z = [0]I implies X = [0]I;

theorem :: PBOOLE:52
   X c= Y & Y /\ Z = [0]I implies X /\ Z = [0]I;

theorem :: PBOOLE:53
 X \/ [0]I = X & [0]I \/ X = X;

theorem :: PBOOLE:54
   X \/ Y = [0]I implies X = [0]I & Y = [0]I;

theorem :: PBOOLE:55
   X /\ [0]I = [0]I & [0]I /\ X = [0]I;

theorem :: PBOOLE:56
   X c= (Y \/ Z) & X /\ Z = [0]I implies X c= Y;

theorem :: PBOOLE:57
   Y c= X & X /\ Y = [0]I implies Y = [0]I;

begin :: Difference and symmetric difference

theorem :: PBOOLE:58
 X \ Y = [0]I iff X c= Y;

theorem :: PBOOLE:59
 X c= Y implies X \ Z c= Y \ Z;

theorem :: PBOOLE:60
 X c= Y implies Z \ Y c= Z \ X;

theorem :: PBOOLE:61
   X c= Y & Z c= V implies X \ V c= Y \ Z;

theorem :: PBOOLE:62
 X \ Y c= X;

theorem :: PBOOLE:63
   X c= Y \ X implies X = [0]I;

theorem :: PBOOLE:64
   X \ X = [0]I;

theorem :: PBOOLE:65
 X \ [0]I = X;

theorem :: PBOOLE:66
 [0]I \ X = [0]I;

theorem :: PBOOLE:67
   X \ (X \/ Y) = [0]I & X \ (Y \/ X) = [0]I;

theorem :: PBOOLE:68
 X /\ (Y \ Z) = (X /\ Y) \ Z;

theorem :: PBOOLE:69
 (X \ Y) /\ Y = [0]I & Y /\ (X \ Y) = [0]I;

theorem :: PBOOLE:70
 X \ (Y \ Z) = (X \ Y) \/ X /\ Z;

theorem :: PBOOLE:71
 (X \ Y) \/ X /\ Y = X & X /\ Y \/ (X \ Y) = X;

theorem :: PBOOLE:72
   X c= Y implies Y = X \/ (Y \ X) & Y = (Y \ X) \/ X;

theorem :: PBOOLE:73
 X \/ (Y \ X) = X \/ Y & (Y \ X) \/ X = Y \/ X;

theorem :: PBOOLE:74
 X \ (X \ Y) = X /\ Y;

theorem :: PBOOLE:75
 X \ (Y /\ Z) = (X \ Y) \/ (X \ Z);

theorem :: PBOOLE:76
 X \ X /\ Y = X \ Y & X \ Y /\ X = X \ Y;

theorem :: PBOOLE:77
   X /\ Y = [0]I iff X \ Y = X;

theorem :: PBOOLE:78
 (X \/ Y) \ Z = (X \ Z) \/ (Y \ Z);

theorem :: PBOOLE:79
 (X \ Y) \ Z = X \ (Y \/ Z);

theorem :: PBOOLE:80 ::  TSEP_1, LEMMA3
   (X /\ Y) \ Z = (X \ Z) /\ (Y \ Z);

theorem :: PBOOLE:81
 (X \/ Y) \ Y = X \ Y;

theorem :: PBOOLE:82
   X c= Y \/ Z implies X \ Y c= Z & X \ Z c= Y;

theorem :: PBOOLE:83
 (X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X);

theorem :: PBOOLE:84
 (X \ Y) \ Y = X \ Y;

theorem :: PBOOLE:85
   X \ (Y \/ Z) = (X \ Y) /\ (X \ Z);

theorem :: PBOOLE:86
   X \ Y = Y \ X implies X = Y;

theorem :: PBOOLE:87
   X /\ (Y \ Z) = X /\ Y \ X /\ Z;

theorem :: PBOOLE:88 :: NORMFORM:2
   X \ Y c= Z implies X c= Y \/ Z;

theorem :: PBOOLE:89
   X \ Y c= X \+\ Y;

canceled;

theorem :: PBOOLE:91
   X \+\ [0]I = X & [0]I \+\ X = X;

theorem :: PBOOLE:92
   X \+\ X = [0]I;

canceled;

theorem :: PBOOLE:94
   X \/ Y = (X \+\ Y) \/ X /\ Y;

theorem :: PBOOLE:95
 X \+\ Y = (X \/ Y) \ X /\ Y;

theorem :: PBOOLE:96
   (X \+\ Y) \ Z = (X \ (Y \/ Z)) \/ (Y \ (X \/ Z));

theorem :: PBOOLE:97
   X \ (Y \+\ Z) = X \ (Y \/ Z) \/ X /\ Y /\ Z;

theorem :: PBOOLE:98
 (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z);

theorem :: PBOOLE:99
  X \ Y c= Z & Y \ X c= Z implies X \+\ Y c= Z;

theorem :: PBOOLE:100  :: FINSUB_1:3
 X \/ Y = X \+\ (Y \ X);

theorem :: PBOOLE:101
 X /\ Y = X \+\ (X \ Y);

theorem :: PBOOLE:102  :: FINSUB_1:5
 X \ Y = X \+\ (X /\ Y);

theorem :: PBOOLE:103
 Y \ X = X \+\ (X \/ Y);

theorem :: PBOOLE:104 :: FINSUB_1:4
   X \/ Y = X \+\ Y \+\ X /\ Y;

theorem :: PBOOLE:105 :: FINSUB_1:6
   X /\ Y = X \+\ Y \+\ (X \/ Y);

begin :: Meeting and overlap(p?)ing

theorem :: PBOOLE:106
   X overlaps Y or X overlaps Z implies X overlaps Y \/ Z;

canceled;

theorem :: PBOOLE:108
 X overlaps Y & Y c= Z implies X overlaps Z;

theorem :: PBOOLE:109
 X overlaps Y & X c= Z implies Z overlaps Y;

theorem :: PBOOLE:110  :: NORMFORM:1
 X c= Y & Z c= V & X overlaps Z implies Y overlaps V;

theorem :: PBOOLE:111
   X overlaps Y /\ Z implies X overlaps Y & X overlaps Z;

theorem :: PBOOLE:112 :: BORSUK_1:1
   X overlaps Z & X c= V implies X overlaps Z /\ V;

theorem :: PBOOLE:113
   X overlaps Y \ Z implies X overlaps Y;

theorem :: PBOOLE:114 :: PROB_2:7, RPR_1:36
   Y does_not_overlap Z implies X /\ Y does_not_overlap X /\ Z;

theorem :: PBOOLE:115 :: AMI_2:1
   X overlaps Y \ Z implies Y overlaps X \ Z;

theorem :: PBOOLE:116
 X meets Y & Y c= Z implies X meets Z;

canceled;

theorem :: PBOOLE:118
 Y misses X \ Y;

theorem :: PBOOLE:119
   X /\ Y misses X \ Y;

theorem :: PBOOLE:120
   X /\ Y misses X \+\ Y;

theorem :: PBOOLE:121
 X misses Y implies X /\ Y = [0]I;

theorem :: PBOOLE:122
   X <> [0]I implies X meets X;

theorem :: PBOOLE:123
   X c= Y & X c= Z & Y misses Z implies X = [0]I;

theorem :: PBOOLE:124  :: SETWISEO:9
   Z \/ V = X \/ Y & X misses Z & Y misses V
  implies X = V & Y = Z;

canceled;

theorem :: PBOOLE:126  :: FINSUB_1:1
 X misses Y implies X \ Y = X;

theorem :: PBOOLE:127 :: FINSUB_1:2
   X misses Y implies (X \/ Y) \ Y = X;

theorem :: PBOOLE:128 :: RPR_1:32
   X \ Y = X implies X misses Y;

theorem :: PBOOLE:129 :: RLVECT_2:102
   X \ Y misses Y \ X;

begin :: Roughly speaking

definition let I,X,Y;
 pred X [= Y means
:: PBOOLE:def 14
 for x st x in X holds x in Y;
 reflexivity;
end;

theorem :: PBOOLE:130
   X c= Y implies X [= Y;

theorem :: PBOOLE:131
   X [= X;

theorem :: PBOOLE:132
   X [= Y & Y [= Z implies X [= Z;

begin :: Non empty set of sorts

theorem :: PBOOLE:133
   [0]{} in [0]{};

theorem :: PBOOLE:134
   for X being ManySortedSet of {} holds X = {};

reserve I for non empty set,
        x,X,Y for ManySortedSet of I;

theorem :: PBOOLE:135
   X overlaps Y implies X meets Y;

theorem :: PBOOLE:136
 not ex x st x in [0]I;

theorem :: PBOOLE:137
    x in X & x in Y implies X /\ Y <> [0]I;

theorem :: PBOOLE:138
   X does_not_overlap [0]I & [0]I does_not_overlap X;

theorem :: PBOOLE:139
 X /\ Y = [0]I implies X does_not_overlap Y;

theorem :: PBOOLE:140
   X overlaps X implies X <> [0]I;

begin :: Empty and non-empty ManySortedSets

reserve I for set,
        x,X,Y,Z for ManySortedSet of I;

definition let I be set;
 let X be ManySortedSet of I;
 redefine attr X is empty-yielding means
:: PBOOLE:def 15
 for i st i in I holds X.i is empty;
 attr X is non-empty means
:: PBOOLE:def 16
 for i st i in I holds X.i is non empty;
end;

definition let I be set;
 cluster empty-yielding ManySortedSet of I;
 cluster non-empty ManySortedSet of I;
end;

definition let I be non empty set;
 cluster non-empty -> non empty-yielding ManySortedSet of I;
 cluster empty-yielding -> non non-empty ManySortedSet of I;
end;

theorem :: PBOOLE:141
   X is empty-yielding iff X = [0]I;

theorem :: PBOOLE:142
   Y is empty-yielding & X c= Y implies X is empty-yielding;

theorem :: PBOOLE:143
 X is non-empty & X c= Y implies Y is non-empty;

theorem :: PBOOLE:144
 X is non-empty & X [= Y implies X c= Y;

theorem :: PBOOLE:145
   X is non-empty & X [= Y implies Y is non-empty;

reserve X for non-empty ManySortedSet of I;

theorem :: PBOOLE:146
   ex x st x in X;

theorem :: PBOOLE:147
 (for x holds x in X iff x in Y) implies X = Y;

theorem :: PBOOLE:148
    (for x holds x in X iff x in Y & x in Z) implies X = Y /\ Z;
The abstract of the Mizar article:

Many-sorted Sets
