:: Manysorted Sets
::  by Andrzej Trybulec
::
:: Received July 7, 1993
:: Copyright (c) 1993-2021 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 FUNCT_1, RELAT_1, SETFAM_1, XBOOLE_0, SUBSET_1, PARTFUN1,
      FUNCOP_1, TARSKI, FUNCT_2, ZFMISC_1, MEMBER_1, FUNCT_4, PBOOLE, NAT_1,
      SETLIM_2;
 notations TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
      ORDINAL1, PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1;
 constructors SETFAM_1, FUNCOP_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_4;
 registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, FUNCT_4,
      RELAT_1;
 requirements BOOLE, SUBSET;


begin

reserve i,j,e,u for object;

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

registration
  let I;
  cluster total for I-defined Function;
end;

definition
  let I;
  mode ManySortedSet of I is total I-defined Function;
end;

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

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

definition
  let I,X,Y;
  pred X in Y means
:: PBOOLE:def 1

  for i being object st i in I holds X.i in Y.i;
  pred X c= Y means
:: PBOOLE:def 2

  for i being object 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 :: PBOOLE:sch 2
  PSeparation { I()-> set, A() -> ManySortedSet of I(), P[object,object] } :
   ex X being ManySortedSet of I() st
    for i being object st i in I()
     for e being object holds e in X.i iff e in A().i & P[i,e];

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

definition
  let I;
  func EmptyMS I -> ManySortedSet of I equals
:: PBOOLE:def 3
  I --> {};
  let X,Y;
  func X (\/) Y -> ManySortedSet of I means
:: PBOOLE:def 4

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

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

  for i being object st i in I holds it.i = X.i \ Y.i;
  pred X overlaps Y means
:: PBOOLE:def 7

  for i being object st i in I holds X.i meets Y.i;
  symmetry;
  pred X misses Y means
:: PBOOLE:def 8

  for i being object st i in I holds X.i misses Y.i;
  symmetry;
end;

notation
  let I;
  let X,Y;
  antonym X meets Y for X misses Y;
end;

definition
  let I,X,Y;
  func X (\+\) Y -> ManySortedSet of I equals
:: PBOOLE:def 9
  (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 being object holds EmptyMS I.i = {};

theorem :: PBOOLE:6
  (for i being object st i in I holds X.i = {}) implies X = EmptyMS 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

definition
  let I,X,Y;
  redefine pred X = Y means
:: PBOOLE:def 10
  for i being object st i in I holds X.i = Y.i;
end;

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

theorem :: PBOOLE:14
  X c= X (\/) Y;

theorem :: PBOOLE:15
  X (/\) Y c= X;

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

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

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

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

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

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

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

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

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

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

theorem :: PBOOLE:26
  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:27
  X = Y (/\) Z iff X c= Y & X c= Z & for V st V c= Y & V c= Z holds V c= X;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

begin :: ManySortedSet with empty components

theorem :: PBOOLE:43
  EmptyMS I c= X;

theorem :: PBOOLE:44
  X c= EmptyMS I implies X = EmptyMS I;

theorem :: PBOOLE:45
  X c= Y & X c= Z & Y (/\) Z = EmptyMS I implies X = EmptyMS I;

theorem :: PBOOLE:46
  X c= Y & Y (/\) Z = EmptyMS I implies X (/\) Z = EmptyMS I;

theorem :: PBOOLE:47
  X (\/) EmptyMS I = X & EmptyMS I (\/) X = X;

theorem :: PBOOLE:48
  X (\/) Y = EmptyMS I implies X = EmptyMS I;

theorem :: PBOOLE:49
  X (/\) EmptyMS I = EmptyMS I;

theorem :: PBOOLE:50
  X c= (Y (\/) Z) & X (/\) Z = EmptyMS I implies X c= Y;

theorem :: PBOOLE:51
  Y c= X & X (/\) Y = EmptyMS I implies Y = EmptyMS I;

begin :: Difference and symmetric difference

theorem :: PBOOLE:52
  X (\) Y = EmptyMS I iff X c= Y;

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

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

theorem :: PBOOLE:55
  X c= Y & Z c= V implies X (\) V c= Y (\) Z;

theorem :: PBOOLE:56
  X (\) Y c= X;

theorem :: PBOOLE:57
  X c= Y (\) X implies X = EmptyMS I;

theorem :: PBOOLE:58
  X (\) X = EmptyMS I;

theorem :: PBOOLE:59
  X (\) EmptyMS I = X;

theorem :: PBOOLE:60
  EmptyMS I (\) X = EmptyMS I;

theorem :: PBOOLE:61
  X (\) (X (\/) Y) = EmptyMS I;

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

theorem :: PBOOLE:63
  (X (\) Y) (/\) Y = EmptyMS I;

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

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

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

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

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

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

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

theorem :: PBOOLE:71
  X (/\) Y = EmptyMS I iff X (\) Y = X;

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

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

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

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

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

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

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

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

theorem :: PBOOLE:80
  X (\) Y = Y (\) X implies X = Y;

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

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

theorem :: PBOOLE:83
  X (\) Y c= X (\+\) Y;

theorem :: PBOOLE:84
  X (\+\) EmptyMS I = X;

theorem :: PBOOLE:85
  X (\+\) X = EmptyMS I;

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

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

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

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

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

theorem :: PBOOLE:91
  X (\) Y c= Z & Y (\) X c= Z implies X (\+\) Y c= Z;

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

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

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

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

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

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

begin :: Meeting and overlap(p?)ing

theorem :: PBOOLE:98
  X overlaps Y or X overlaps Z implies X overlaps Y (\/) Z;

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

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

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

theorem :: PBOOLE:102
  X overlaps Y (/\) Z implies X overlaps Y & X overlaps Z;

theorem :: PBOOLE:103
  X overlaps Z & X c= V implies X overlaps Z (/\) V;

theorem :: PBOOLE:104
  X overlaps Y (\) Z implies X overlaps Y;

theorem :: PBOOLE:105
  Y does not overlap Z implies X (/\) Y does not overlap X (/\) Z;

theorem :: PBOOLE:106
  X overlaps Y (\) Z implies Y overlaps X (\) Z;

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

theorem :: PBOOLE:108
  Y misses X (\) Y;

theorem :: PBOOLE:109
  X (/\) Y misses X (\) Y;

theorem :: PBOOLE:110
  X (/\) Y misses X (\+\) Y;

theorem :: PBOOLE:111
  X misses Y implies X (/\) Y = EmptyMS I;

theorem :: PBOOLE:112
  X <> EmptyMS I implies X meets X;

theorem :: PBOOLE:113
  X c= Y & X c= Z & Y misses Z implies X = EmptyMS I;

theorem :: PBOOLE:114
  Z (\/) V = X (\/) Y & X misses Z & Y misses V implies X = V & Y = Z;

theorem :: PBOOLE:115
  X misses Y implies X (\) Y = X;

theorem :: PBOOLE:116
  X misses Y implies (X (\/) Y) (\) Y = X;

theorem :: PBOOLE:117
  X (\) Y = X implies X misses Y;

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

begin :: Roughly speaking

definition
  let I,X,Y;
  pred X [= Y means
:: PBOOLE:def 11

  for x st x in X holds x in Y;
  reflexivity;
end;

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

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

begin :: Non empty set of sorts

theorem :: PBOOLE:121
  EmptyMS {} in EmptyMS {};

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

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

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

theorem :: PBOOLE:124
  not ex x st x in EmptyMS I;

theorem :: PBOOLE:125
  x in X & x in Y implies X (/\) Y <> EmptyMS I;

theorem :: PBOOLE:126
  X does not overlap EmptyMS I;

theorem :: PBOOLE:127
  X (/\) Y = EmptyMS I implies X does not overlap Y;

theorem :: PBOOLE:128
  X overlaps X implies X <> EmptyMS 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 12

  for i being object st i in I holds X.i is empty;
  redefine attr X is non-empty means
:: PBOOLE:def 13

  for i being object st i in I holds X.i is non empty;
end;

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

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

theorem :: PBOOLE:129
  X is empty-yielding iff X = EmptyMS I;

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

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

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

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

reserve X for non-empty ManySortedSet of I;

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

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

theorem :: PBOOLE:136
  (for x holds x in X iff x in Y & x in Z) implies X = Y (/\) Z;

begin :: Addenda

scheme :: PBOOLE:sch 3
  MSSEx { I() -> set, P[object,object] }:
  ex f being ManySortedSet of I() st
   for i being object st i in I() holds P[i,f.i]
provided
 for i being object st i in I() ex j being object st P[i,j];

scheme :: PBOOLE:sch 4
  MSSLambda { I() -> set, F(object) -> object }:
ex f being ManySortedSet of I() st
  for i being object st i in I() holds f.i = F(i);

registration
  let I be set;
  cluster Function-yielding for ManySortedSet of I;
end;

definition
  let I be set;
  mode ManySortedFunction of I is Function-yielding ManySortedSet of I;
end;

theorem :: PBOOLE:137
  not ex M being non-empty ManySortedSet of I st {} in rng M;

definition
  let M be Function;
  mode Component of M is Element of rng M;
end;

theorem :: PBOOLE:138
  for I being non empty set for M being ManySortedSet of I, A being
  Component of M ex i being object st i in I & A = M.i;

theorem :: PBOOLE:139
  for M being ManySortedSet of I, i st i in I holds M.i is Component of M;

definition
  let I;
  let B be ManySortedSet of I;
  mode Element of B -> ManySortedSet of I means
:: PBOOLE:def 14
    for i being object st i in I holds it.i is Element of B.i;
end;

begin :: Many Sorted Functions

definition
  let I;
  let A be ManySortedSet of I, B be ManySortedSet of I;
  mode ManySortedFunction of A,B -> ManySortedSet of I means
:: PBOOLE:def 15
 for i st i in I holds it.i is Function of A.i, B.i;
end;

registration
  let I;
  let A be ManySortedSet of I, B be ManySortedSet of I;
  cluster ->Function-yielding for ManySortedFunction of A,B;
end;

registration
  let I be set;
  let J be non empty set;
  let O be Function of I,J;
  let F be ManySortedSet of J;
  cluster F*O -> total for I-defined Function;
end;

reserve D for non empty set,
  n for Nat;

scheme :: PBOOLE:sch 5
  LambdaDMS {D()->non empty set, F(object)->object}:
  ex X be ManySortedSet of D() st
  for d be Element of D() holds X.d = F(d);

registration
  let J be non empty set, B be non-empty ManySortedSet of J, j be Element of J;
  cluster B.j -> non empty;
end;

reserve X,Y for ManySortedSet of I;

definition
  let I, X,Y;
  func [|X,Y|] -> ManySortedSet of I means
:: PBOOLE:def 16
  for i being object st i in I holds it.i = [:X.i,Y.i:];
end;

definition
  let I, X, Y;
  func (Funcs) (X,Y) -> ManySortedSet of I means
:: PBOOLE:def 17
  for i being object st i in I holds it.i = Funcs(X.i,Y.i);
end;

definition
  let I be set, M be ManySortedSet of I;
  mode ManySortedSubset of M -> ManySortedSet of I means
:: PBOOLE:def 18

  it c= M;
end;

registration
  let I be set, M be non-empty ManySortedSet of I;
  cluster non-empty for ManySortedSubset of M;
end;

definition
  let F,G be Function-yielding Function;
  func G**F -> Function means
:: PBOOLE:def 19

  dom it = (dom F) /\ (dom G) &
  for i be object st i in dom it holds it.i = (G.i)*(F.i);
end;

registration
  let F,G be Function-yielding Function;
  cluster G**F -> Function-yielding;
end;

definition
  let I be set, A be ManySortedSet of I, F be ManySortedFunction of I;
  func F.:.:A -> ManySortedSet of I means
:: PBOOLE:def 20
  for i be set st i in I holds it.i = (F.i).:(A.i);
end;

registration
  let I;
  cluster EmptyMS I -> empty-yielding;
end;

scheme :: PBOOLE:sch 6
  MSSExD { I() -> non empty set, P[object,object] }:
  ex f being ManySortedSet of I()
  st for i being Element of I() holds P[i,f.i]
provided
 for i being Element of I() ex j being object st P[i,j];

registration
  let A be non empty set;
  cluster non-empty -> non empty-yielding for ManySortedSet of A;
end;

registration
  let X be non empty set;
  cluster -> non empty for ManySortedSet of X;
end;

theorem :: PBOOLE:140
  for F, G, H be Function-yielding Function holds
  (H ** G) ** F = H ** (G ** F);

registration
 let I be set, f be non-empty ManySortedSet of I;
 cluster total for I-defined f-compatible Function;
end;

theorem :: PBOOLE:141
 for I being set, f being non-empty ManySortedSet of I
 for p being f-compatible I-defined Function
  ex s being f-compatible ManySortedSet of I st p c= s;

theorem :: PBOOLE:142
  for I,A be set
  for s,ss being ManySortedSet of I
  holds (ss +* s | A) | A = s | A;

registration
 let X be non empty set, Y be set;
 cluster X-valued for ManySortedSet of Y;
end;

theorem :: PBOOLE:143
  for I,Y being non empty set, M be Y-valued ManySortedSet of I,
     x be Element of I
  holds M.x = M/.x;

theorem :: PBOOLE:144
 for f being Function, M being ManySortedSet of I
   holds (f+*M)|I = M;

theorem :: PBOOLE:145
 for I being set, Y being non empty set
 for p being Y-valued I-defined Function
  ex s being Y-valued ManySortedSet of I st p c= s;

theorem :: PBOOLE:146
 X c= Y & Y c= X implies X = Y;

definition let I be non empty set, A,B be ManySortedSet of I;
 redefine pred A = B means
:: PBOOLE:def 21
  for i being Element of I holds A.i = B.i;
end;

registration
  let X be with_non-empty_elements set;
  cluster id X -> non-empty;
end;

scheme :: PBOOLE:sch 7
  MSSLambda { I() -> set, F(object) -> object }:
  ex f being ManySortedSet of I() st
  for i being set st i in I() holds f.i = F(i);