The abstract of the Mizar article:

Semilattice Operations on Finite Subsets

by

Andrzej Trybulec

Received September 18, 1989

MML identifier: SETWISEO

[ Mizar article, MML identifier index ]

environ

 vocabulary BOOLE, FUNCT_1, RELAT_1, FINSUB_1, FINSET_1, BINOP_1, FUNCOP_1,
      TARSKI, SETWISEO;
 notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, RELAT_1, FUNCT_1, FINSUB_1,
      FINSET_1, FUNCT_2, BINOP_1, FUNCOP_1;
 constructors TARSKI, ENUMSET1, FINSUB_1, FINSET_1, BINOP_1, FUNCOP_1,
      XBOOLE_0;
 clusters FINSET_1, FINSUB_1, RELSET_1, XBOOLE_0, ZFMISC_1;
 requirements BOOLE, SUBSET;


begin ::  A u x i l i a r y   T h e o r e m s

 reserve x,y,z,X,Y for set;

canceled 2;

theorem :: SETWISEO:3
{x} c= {x,y,z}
;

theorem :: SETWISEO:4
{x,y} c= {x,y,z}
;

theorem :: SETWISEO:5
 X c= Y \/ {x} implies x in X or X c= Y;

theorem :: SETWISEO:6
 x in X \/ {y} iff x in X or x = y;

canceled;

theorem :: SETWISEO:8
 X \/ {x} c= Y iff x in Y & X c= Y;

canceled 2;

theorem :: SETWISEO:11
 for X,Y for f being Function holds f.:(Y \ f"X) = f.:Y \ X;

reserve X,Y for non empty set,
        f for Function of X,Y;

theorem :: SETWISEO:12
  for x being Element of X holds x in f"{f.x};

theorem :: SETWISEO:13
  for x being Element of X holds f.:{x} = {f.x};

scheme SubsetEx { A() -> non empty set, P[set] } :
  ex B being Subset of A() st
   for x being Element of A() holds x in B iff P[x];

:: Theorems related to Fin ...

theorem :: SETWISEO:14
 for B being Element of Fin X
   for x st x in B holds x is Element of X;

theorem :: SETWISEO:15
  for A being (Element of Fin X), B being set
 for f being Function of X,Y st
   for x being Element of X holds x in A implies f.x in B
  holds f.:A c= B;

theorem :: SETWISEO:16
 for X being set for B being Element of Fin X
   for A being set st A c= B holds A is Element of Fin X;

canceled;

theorem :: SETWISEO:18
 for B being Element of Fin X st B <> {}
   ex x being Element of X st x in B;

theorem :: SETWISEO:19
  for A being Element of Fin X holds f.:A = {} implies A = {};

definition let X be set;
 cluster empty Element of Fin X;
end;

definition let X be set;
 func {}.X -> empty Element of Fin X equals
:: SETWISEO:def 1
     {};
end;

scheme FinSubFuncEx{ A()->non empty set
, B()->(Element of Fin A()), P[set,set] } :
 ex f being Function of A(), Fin A() st
  for b,a being Element of A() holds a in f.b iff a in B() & P[a,b];

:: theorems related to BinOp of ...

definition let X be non empty set, F be BinOp of X;
 attr F is having_a_unity means
:: SETWISEO:def 2
 ex x being Element of X st x is_a_unity_wrt F;
  synonym F has_a_unity;
end;

canceled 2;

theorem :: SETWISEO:22
 for X being non empty set, F being BinOp of X holds
  F has_a_unity iff the_unity_wrt F is_a_unity_wrt F;

theorem :: SETWISEO:23
for X being non empty set, F being BinOp of X st F has_a_unity
  for x being Element of X holds
    F.(the_unity_wrt F, x) = x &
    F.(x, the_unity_wrt F) = x;

   ::  M a i n   p a r t

definition let X be non empty set;
 cluster non empty Element of Fin X;
end;

definition let X be non empty set, x be Element of X;
 redefine func {x} -> Element of Fin X;
 let y be Element of X;
  func {x,y} -> Element of Fin X;
 let z be Element of X;
  func {x,y,z} -> Element of Fin X;
end;

definition let X be set; let A,B be Element of Fin X;
 redefine func A \/ B -> Element of Fin X;
end;

definition let X be set; let A,B be Element of Fin X;
 redefine func A \ B -> Element of Fin X;
end;

scheme FinSubInd1{ X() -> non empty set, P[set] } :
  for B being Element of Fin X() holds P[B]
 provided
  P[{}.X()] and
  for B' being (Element of Fin X()), b being Element of X()
      holds P[B'] & not b in B' implies P[B' \/ {b}];

scheme FinSubInd2{ X() -> non empty set, P[Element of Fin X()] } :
  for B being Element of Fin X() st B <> {} holds P[B]
 provided
  for x being Element of X() holds P[{x}] and
  for B1,B2 being Element of Fin X() st B1 <> {} & B2 <> {}
      holds P[B1] & P[B2] implies P[B1 \/ B2];

scheme FinSubInd3{ X() -> non empty set, P[set] } :
  for B being Element of Fin X() holds P[B]
 provided
  P[{}.X()] and
  for B' being (Element of Fin X()), b being Element of X()
      holds P[B'] implies P[B' \/ {b}];

definition let X, Y be non empty set;
 let F be BinOp of Y;
 let B be Element of Fin X; let f be Function of X,Y;
 assume that
 B <> {} or F has_a_unity and
 F is commutative and
 F is associative;
  func F $$ (B,f) -> Element of Y means
:: SETWISEO:def 3
   ex G being Function of Fin X, Y st it = G.B &
          (for e being Element of Y st e is_a_unity_wrt F holds G.{} = e) &
          (for x being Element of X holds G.{x} = f.x) &
           for B' being Element of Fin X st B' c= B & B' <> {}
           for x being Element of X st x in B \ B'
            holds G.(B' \/ {x}) = F.(G.B',f.x);
end;

canceled;

theorem :: SETWISEO:25
for X, Y being non empty set for F being BinOp of Y
for B being Element of Fin X for f being Function of X,Y st
  (B <> {} or F has_a_unity) &
  F is idempotent & F is commutative & F is associative
for IT being Element of Y holds
  IT = F $$ (B,f) iff
   ex G being Function of Fin X, Y st IT = G.B &
    (for e being Element of Y st e is_a_unity_wrt F holds G.{} = e) &
    (for x being Element of X holds G.{x} = f.x) &
     for B' being Element of Fin X st B' c= B & B' <> {}
      for x being Element of X st x in B holds G.(B' \/ {x}) = F.(G.B',f.x);

 reserve X, Y for non empty set,
         F for (BinOp of Y),
         B for (Element of Fin X),
         f for Function of X,Y;

theorem :: SETWISEO:26
 F is commutative & F is associative
  implies for b being Element of X holds F $$ ({b},f) = f.b;

theorem :: SETWISEO:27
 F is idempotent & F is commutative & F is associative
  implies for a,b being Element of X holds F $$ ({a,b},f) = F.(f.a, f.b);

theorem :: SETWISEO:28
 F is idempotent & F is commutative & F is associative
  implies for a,b,c being Element of X holds
   F $$ ({a,b,c},f) = F.(F.(f.a, f.b), f.c);

   :: I f   B   i s   n o n   e m p t y

theorem :: SETWISEO:29
 F is idempotent & F is commutative & F is associative & B <> {} implies
   for x being Element of X holds F $$(B \/ {x}, f) = F.(F $$(B,f),f.x);

theorem :: SETWISEO:30
 F is idempotent & F is commutative & F is associative
  implies
   for B1,B2 being Element of Fin X st B1 <> {} & B2 <> {}
      holds F $$ (B1 \/ B2,f) = F.(F $$ (B1,f),F $$ (B2,f));

theorem :: SETWISEO:31
    F is commutative & F is associative & F is idempotent implies
   for x being Element of X st x in B holds F.(f.x,F$$(B,f)) = F$$(B,f);

theorem :: SETWISEO:32
    F is commutative & F is associative & F is idempotent implies
   for B,C being Element of Fin X st B <> {} & B c= C
    holds F.(F$$(B,f),F$$(C,f)) = F$$(C,f);

theorem :: SETWISEO:33
 B <> {} & F is commutative & F is associative & F is idempotent implies
    for a being Element of Y st
      for b being Element of X st b in B holds f.b = a
     holds F$$(B,f) = a;

theorem :: SETWISEO:34
  F is commutative & F is associative & F is idempotent implies
    for a being Element of Y st f.:B = {a} holds F$$(B,f) = a;

theorem :: SETWISEO:35
 F is commutative & F is associative & F is idempotent implies
  for f,g being Function of X,Y
   for A,B being Element of Fin X st A <> {} & f.:A = g.:B
    holds F$$(A,f) = F$$(B,g);

theorem :: SETWISEO:36
   for F,G being BinOp of Y st
 F is idempotent &
 F is commutative & F is associative & G is_distributive_wrt F
   for B being Element of Fin X st B <> {}
     for f being Function of X,Y
    for a being Element of Y
    holds G.(a,F$$(B,f)) = F$$(B,G[;](a,f));

theorem :: SETWISEO:37
   for F,G being BinOp of Y st
 F is idempotent &
 F is commutative & F is associative & G is_distributive_wrt F
   for B being Element of Fin X st B <> {}
     for f being Function of X,Y
    for a being Element of Y
    holds G.(F$$(B,f),a) = F$$(B,G[:](f,a));

definition let X, Y be non empty set; let f be Function of X,Y;
 let A be Element of Fin X;
 redefine func f.:A -> Element of Fin Y;
end;

theorem :: SETWISEO:38
 for A, X, Y being non empty set for F being BinOp of A
  st F is idempotent & F is commutative & F is associative
   for B being Element of Fin X st B <> {}
    for f being Function of X,Y holds
     for g being Function of Y,A holds F$$(f.:B,g) = F$$(B,g*f);

theorem :: SETWISEO:39
  F is commutative & F is associative & F is idempotent
  implies
  for Z being non empty set
  for G being BinOp of Z st
    G is commutative & G is associative & G is idempotent
   for f being Function of X, Y
   for g being Function of Y,Z st
     for x,y being Element of Y holds g.(F.(x,y)) = G.(g.x,g.y)
    for B being Element of Fin X st B <> {} holds g.(F$$(B,f)) = G$$(B,g*f);

   :: I f   F   h a s   a   u n i t y

theorem :: SETWISEO:40
 F is commutative & F is associative & F has_a_unity
  implies for f holds F$$({}.X,f) = the_unity_wrt F;

theorem :: SETWISEO:41
 F is idempotent & F is commutative & F is associative & F has_a_unity
  implies for x being Element of X holds F $$(B \/ {x}, f) = F.(F $$(B,f),f.x);

theorem :: SETWISEO:42
   F is idempotent & F is commutative & F is associative & F has_a_unity
  implies
   for B1,B2 being Element of Fin X
      holds F $$ (B1 \/ B2,f) = F.(F $$ (B1,f),F $$ (B2,f));

theorem :: SETWISEO:43
   F is commutative & F is associative & F is idempotent & F has_a_unity
  implies
   for f,g being Function of X,Y
    for A,B being Element of Fin X st f.:A = g.:B
     holds F$$(A,f) = F$$(B,g);

theorem :: SETWISEO:44
 for A, X, Y being non empty set for F being BinOp of A
  st F is idempotent & F is commutative & F is associative & F has_a_unity
   for B being Element of Fin X
    for f being Function of X,Y holds
     for g being Function of Y,A holds F$$(f.:B,g) = F$$(B,g*f);

theorem :: SETWISEO:45
    F is commutative & F is associative & F is idempotent & F has_a_unity
  implies
  for Z being non empty set
  for G being BinOp of Z st
    G is commutative & G is associative & G is idempotent & G has_a_unity
   for f being Function of X, Y
   for g being Function of Y,Z st
     g.the_unity_wrt F = the_unity_wrt G &
     for x,y being Element of Y holds g.(F.(x,y)) = G.(g.x,g.y)
    for B being Element of Fin X holds g.(F$$(B,f)) = G$$(B,g*f);

:: Funkcja wprowadzona powyzej konieczna jest do zakastowania
:: wyniku operacji unii. Jest to Element of  DOMAIN ,
:: co nie rozszerza sie do Element of  DOMAIN

 definition let A be set;
  func FinUnion A -> BinOp of Fin A means
:: SETWISEO:def 4
 for x,y being Element of Fin A holds
        it.(x,y) = (x \/ y);
 end;

reserve A for set,
        x,y,z for Element of Fin A;

canceled 3;

theorem :: SETWISEO:49
 FinUnion A is idempotent;

theorem :: SETWISEO:50
 FinUnion A is commutative;

theorem :: SETWISEO:51
 FinUnion A is associative;

theorem :: SETWISEO:52
  {}.A is_a_unity_wrt FinUnion A;

theorem :: SETWISEO:53
 FinUnion A has_a_unity;

theorem :: SETWISEO:54
   the_unity_wrt FinUnion A is_a_unity_wrt FinUnion A;

theorem :: SETWISEO:55
 the_unity_wrt FinUnion A = {};

reserve X,Y for non empty set, A for set,
        f for (Function of X, Fin A),
        i,j,k for (Element of X);

definition let X be non empty set, A be set;
 let B be Element of Fin X; let f be Function of X, Fin A;
  func FinUnion(B,f) -> Element of Fin A equals
:: SETWISEO:def 5
  FinUnion A $$(B,f);
end;

theorem :: SETWISEO:56
   FinUnion({i},f) = f.i;

theorem :: SETWISEO:57
   FinUnion({i,j},f) = f.i \/ f.j;

theorem :: SETWISEO:58
   FinUnion({i,j,k},f) = f.i \/ f.j \/ f.k;

theorem :: SETWISEO:59
  FinUnion({}.X,f) = {};

theorem :: SETWISEO:60
 for B being Element of Fin X holds
  FinUnion(B \/ {i}, f) = FinUnion(B,f) \/ f.i;

theorem :: SETWISEO:61
 for B being Element of Fin X holds FinUnion(B,f) = union (f.:B);

theorem :: SETWISEO:62
   for B1,B2 being Element of Fin X holds
  FinUnion(B1 \/ B2, f) = FinUnion(B1,f) \/ FinUnion(B2,f);

theorem :: SETWISEO:63
   for B being Element of Fin X
  for f being Function of X,Y holds
   for g being Function of Y,Fin A holds FinUnion(f.:B,g) = FinUnion(B,g*f);

theorem :: SETWISEO:64
  for A,X being non empty set, Y being set
  for G being BinOp of A st
     G is commutative & G is associative & G is idempotent
   for B being Element of Fin X st B <> {}
   for f being (Function of X,Fin Y), g being Function of Fin Y,A st
    for x,y being Element of Fin Y holds g.(x \/ y) = G.(g.x,g.y)
   holds g.(FinUnion(B,f)) = G$$(B,g*f);

theorem :: SETWISEO:65
  for Z being non empty set, Y being set
  for G being BinOp of Z st
    G is commutative & G is associative & G is idempotent & G has_a_unity
   for f being Function of X, Fin Y
   for g being Function of Fin Y,Z st
     g.{}.Y = the_unity_wrt G &
     for x,y being Element of Fin Y holds g.(x \/ y) = G.(g.x,g.y)
    for B being Element of Fin X holds g.(FinUnion(B,f)) = G$$(B,g*f);

definition let A be set;
 func singleton A -> Function of A, Fin A means
:: SETWISEO:def 6
 for x being set st x in A holds it.x = {x};
end;

canceled;

theorem :: SETWISEO:67
 for A being non empty set for f being Function of A, Fin A holds
  f = singleton A iff for x being Element of A holds f.x = {x};

theorem :: SETWISEO:68
 for x being set, y being Element of X holds x in singleton X.y iff x = y;

theorem :: SETWISEO:69
   for x,y,z being Element of X st x in singleton X.z & y in singleton X.z
   holds x = y;

theorem :: SETWISEO:70
 for B being Element of Fin X, x being set holds
  x in FinUnion(B, f) iff ex i being Element of X st i in B & x in f.i;

theorem :: SETWISEO:71
    for B being Element of Fin X holds FinUnion(B, singleton X) = B;



theorem :: SETWISEO:72
    for Y,Z being set
   for f being Function of X, Fin Y
   for g being Function of Fin Y, Fin Z st
     g.{}.Y = {}.Z &
     for x,y being Element of Fin Y holds g.(x \/ y) = g.x \/ g.y
    for B being Element of Fin X holds g.(FinUnion(B,f)) = FinUnion(B,g*f);