:: Semilattice Operations on Finite Subsets
:: by Andrzej Trybulec
::
:: Copyright (c) 1990-2021 Association of Mizar Users

theorem Th1: :: SETWISEO:1
for x, y, z being set holds {x} c= {x,y,z}
proof end;

theorem Th2: :: SETWISEO:2
for x, y, z being set holds {x,y} c= {x,y,z}
proof end;

theorem :: SETWISEO:3
canceled;

theorem :: SETWISEO:4
canceled;

theorem :: SETWISEO:5
canceled;

::\$CT 3
theorem Th3: :: SETWISEO:6
for X, Y being set
for f being Function holds f .: (Y \ (f " X)) = (f .: Y) \ X
proof end;

theorem Th4: :: SETWISEO:7
for X, Y being non empty set
for f being Function of X,Y
for x being Element of X holds x in f " {(f . x)}
proof end;

theorem Th5: :: SETWISEO:8
for X, Y being non empty set
for f being Function of X,Y
for x being Element of X holds Im (f,x) = {(f . x)}
proof end;

:: Theorems related to Fin ...
theorem Th6: :: SETWISEO:9
for X being non empty set
for B being Element of Fin X
for x being set st x in B holds
x is Element of X
proof end;

theorem :: SETWISEO:10
for X, Y being non empty set
for A being Element of Fin X
for B being set
for f being Function of X,Y st ( for x being Element of X st x in A holds
f . x in B ) holds
f .: A c= B
proof end;

theorem Th8: :: SETWISEO:11
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
proof end;

Lm1: for X, Y being non empty set
for f being Function of X,Y
for A being Element of Fin X holds f .: A is Element of Fin Y

by FINSUB_1:def 5;

theorem Th9: :: SETWISEO:12
for X being non empty set
for B being Element of Fin X st B <> {} holds
ex x being Element of X st x in B
proof end;

theorem Th10: :: SETWISEO:13
for X, Y being non empty set
for f being Function of X,Y
for A being Element of Fin X st f .: A = {} holds
A = {}
proof end;

registration
let X be set ;
cluster empty finite for Element of Fin X;
existence
ex b1 being Element of Fin X st b1 is empty
proof end;
end;

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

:: deftheorem defines {}. SETWISEO:def 1 :
for X being set holds {}. X = {} ;

scheme :: SETWISEO:sch 1
FinSubFuncEx{ F1() -> non empty set , F2() -> Element of Fin F1(), P1[ set , set ] } :
ex f being Function of F1(),(Fin F1()) st
for b, a being Element of F1() holds
( a in f . b iff ( a in F2() & P1[a,b] ) )
proof end;

:: theorems related to BinOp of ...
definition
let X be non empty set ;
let 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;
end;

:: deftheorem defines having_a_unity SETWISEO:def 2 :
for X being non empty set
for F being BinOp of X holds
( F is having_a_unity iff ex x being Element of X st x is_a_unity_wrt F );

theorem Th11: :: SETWISEO:14
for X being non empty set
for F being BinOp of X holds
( F is having_a_unity iff the_unity_wrt F is_a_unity_wrt F ) by BINOP_1:def 8;

theorem Th12: :: SETWISEO:15
for X being non empty set
for F being BinOp of X st F is having_a_unity holds
for x being Element of X holds
( F . ((),x) = x & F . (x,()) = x )
proof end;

:: Main part
registration
let X be non empty set ;
cluster non empty finite for Element of Fin X;
existence
not for b1 being Element of Fin X holds b1 is empty
proof end;
end;

notation
let X be non empty set ;
let x be Element of X;
synonym {.x.} for {X};
let y be Element of X;
synonym {.x,y.} for {X,x};
let z be Element of X;
synonym {.x,y,z.} for {X,x,y};
end;

definition
let X be non empty set ;
let x be Element of X;
:: original: {.
redefine func {.x.} -> Element of Fin X;
coherence
is Element of Fin X
proof end;
let y be Element of X;
:: original: {.
redefine func {.x,y.} -> Element of Fin X;
coherence
{.y,.} is Element of Fin X
proof end;
let z be Element of X;
:: original: {.
redefine func {.x,y,z.} -> Element of Fin X;
coherence
{.y,z,.} is Element of Fin X
proof end;
end;

definition
let X be set ;
let A, B be Element of Fin X;
:: original: \/
redefine func A \/ B -> Element of Fin X;
coherence
A \/ B is Element of Fin X
by FINSUB_1:1;
end;

definition
let X be set ;
let A, B be Element of Fin X;
:: original: \
redefine func A \ B -> Element of Fin X;
coherence
A \ B is Element of Fin X
by FINSUB_1:1;
end;

scheme :: SETWISEO:sch 2
FinSubInd1{ F1() -> non empty set , P1[ set ] } :
for B being Element of Fin F1() holds P1[B]
provided
A1: P1[ {}. F1()] and
A2: for B9 being Element of Fin F1()
for b being Element of F1() st P1[B9] & not b in B9 holds
P1[B9 \/ {b}]
proof end;

scheme :: SETWISEO:sch 3
FinSubInd2{ F1() -> non empty set , P1[ Element of Fin F1()] } :
for B being non empty Element of Fin F1() holds P1[B]
provided
A1: for x being Element of F1() holds P1[{.x.}] and
A2: for B1, B2 being non empty Element of Fin F1() st P1[B1] & P1[B2] holds
P1[B1 \/ B2]
proof end;

scheme :: SETWISEO:sch 4
FinSubInd3{ F1() -> non empty set , P1[ set ] } :
for B being Element of Fin F1() holds P1[B]
provided
A1: P1[ {}. F1()] and
A2: for B9 being Element of Fin F1()
for b being Element of F1() st P1[B9] holds
P1[B9 \/ {b}]
proof end;

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
A1: ( B <> {} or F is having_a_unity ) and
A2: F is commutative and
A3: F is associative ;
func F $$(B,f) -> Element of Y means :Def3: :: 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ); existence ex b1 being Element of Y ex G being Function of (Fin X),Y st ( b1 = 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) proof end; uniqueness for b1, b2 being Element of Y st ex G being Function of (Fin X),Y st ( b1 = 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) & ex G being Function of (Fin X),Y st ( b2 = 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) holds b1 = b2 proof end; end; :: deftheorem Def3 defines$$ SETWISEO:def 3 :
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 is having_a_unity ) & F is commutative & F is associative holds
for b6 being Element of Y holds
( b6 = F $$(B,f) iff ex G being Function of (Fin X),Y st ( b6 = 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) ); theorem Th13: :: SETWISEO:16 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 is having_a_unity ) & F is idempotent & F is commutative & F is associative holds 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds
for x being Element of X st x in B holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) )
proof end;

theorem Th14: :: SETWISEO:17
for X, Y being non empty set
for F being BinOp of Y
for f being Function of X,Y st F is commutative & F is associative holds
for b being Element of X holds F $$({.b.},f) = f . b proof end; theorem Th15: :: SETWISEO:18 for X, Y being non empty set for F being BinOp of Y for f being Function of X,Y st F is idempotent & F is commutative & F is associative holds for a, b being Element of X holds F$$ ({.a,b.},f) = F . ((f . a),(f . b))
proof end;

theorem Th16: :: SETWISEO:19
for X, Y being non empty set
for F being BinOp of Y
for f being Function of X,Y st F is idempotent & F is commutative & F is associative holds
for a, b, c being Element of X holds F $$({.a,b,c.},f) = F . ((F . ((f . a),(f . b))),(f . c)) proof end; :: If B is non empty theorem Th17: :: SETWISEO:20 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 F is idempotent & F is commutative & F is associative & B <> {} holds for x being Element of X holds F$$ ((B \/ {.x.}),f) = F . ((F $$(B,f)),(f . x)) proof end; theorem Th18: :: SETWISEO:21 for X, Y being non empty set for F being BinOp of Y for f being Function of X,Y st F is idempotent & F is commutative & F is associative holds for B1, B2 being Element of Fin X st B1 <> {} & B2 <> {} holds F$$ ((B1 \/ B2),f) = F . ((F $$(B1,f)),(F$$ (B2,f)))
proof end;

theorem :: SETWISEO:22
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 F is commutative & F is associative & F is idempotent holds
for x being Element of X st x in B holds
F . ((f . x),(F $$(B,f))) = F$$ (B,f)
proof end;

theorem :: SETWISEO:23
for X, Y being non empty set
for F being BinOp of Y
for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds
for B, C being Element of Fin X st B <> {} & B c= C holds
F . ((F $$(B,f)),(F$$ (C,f))) = F $$(C,f) proof end; theorem Th21: :: SETWISEO:24 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 <> {} & F is commutative & F is associative & F is idempotent holds 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
proof end;

theorem Th22: :: 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 F is commutative & F is associative & F is idempotent holds
for a being Element of Y st f .: B = {a} holds
F $$(B,f) = a proof end; theorem Th23: :: SETWISEO:26 for X, Y being non empty set for F being BinOp of Y st F is commutative & F is associative & F is idempotent holds 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) proof end; theorem :: SETWISEO:27 for X, Y being non empty set for F, G being BinOp of Y st F is idempotent & F is commutative & F is associative & G is_distributive_wrt F holds for B being Element of Fin X st B <> {} holds for f being Function of X,Y for a being Element of Y holds G . (a,(F$$ (B,f))) = F $$(B,(G [;] (a,f))) proof end; theorem :: SETWISEO:28 for X, Y being non empty set for F, G being BinOp of Y st F is idempotent & F is commutative & F is associative & G is_distributive_wrt F holds for B being Element of Fin X st B <> {} holds for f being Function of X,Y for a being Element of Y holds G . ((F$$ (B,f)),a) = F $$(B,(G [:] (f,a))) proof end; definition let X, Y be non empty set ; let f be Function of X,Y; let A be Element of Fin X; :: original: .: redefine func f .: A -> Element of Fin Y; coherence f .: A is Element of Fin Y by Lm1; end; theorem Th26: :: SETWISEO:29 for A, X, Y being non empty set for F being BinOp of A st F is idempotent & F is commutative & F is associative holds for B being Element of Fin X st B <> {} holds for f being Function of X,Y for g being Function of Y,A holds F$$ ((f .: B),g) = F $$(B,(g * f)) proof end; theorem Th27: :: SETWISEO:30 for X, Y being non empty set for F being BinOp of Y st F is commutative & F is associative & F is idempotent holds for Z being non empty set for G being BinOp of Z st G is commutative & G is associative & G is idempotent holds 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)) ) holds for B being Element of Fin X st B <> {} holds g . (F$$ (B,f)) = G $$(B,(g * f)) proof end; :: If F has a unity theorem Th28: :: SETWISEO:31 for X, Y being non empty set for F being BinOp of Y st F is commutative & F is associative & F is having_a_unity holds for f being Function of X,Y holds F$$ (({}. X),f) = the_unity_wrt F
proof end;

theorem Th29: :: SETWISEO:32
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 F is idempotent & F is commutative & F is associative & F is having_a_unity holds
for x being Element of X holds F $$((B \/ {.x.}),f) = F . ((F$$ (B,f)),(f . x))
proof end;

theorem :: SETWISEO:33
for X, Y being non empty set
for F being BinOp of Y
for f being Function of X,Y st F is idempotent & F is commutative & F is associative & F is having_a_unity holds
for B1, B2 being Element of Fin X holds F $$((B1 \/ B2),f) = F . ((F$$ (B1,f)),(F $$(B2,f))) proof end; theorem :: SETWISEO:34 for X, Y being non empty set for F being BinOp of Y st F is commutative & F is associative & F is idempotent & F is having_a_unity holds 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) proof end; theorem Th32: :: SETWISEO:35 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 is having_a_unity holds for B being Element of Fin X for f being Function of X,Y for g being Function of Y,A holds F$$ ((f .: B),g) = F $$(B,(g * f)) proof end; theorem :: SETWISEO:36 for X, Y being non empty set for F being BinOp of Y st F is commutative & F is associative & F is idempotent & F is having_a_unity holds for Z being non empty set for G being BinOp of Z st G is commutative & G is associative & G is idempotent & G is having_a_unity holds for f being Function of X,Y for g being Function of Y,Z st g . () = the_unity_wrt G & ( for x, y being Element of Y holds g . (F . (x,y)) = G . ((g . x),(g . y)) ) holds for B being Element of Fin X holds g . (F$$ (B,f)) = G $$(B,(g * f)) proof end; definition let A be set ; func FinUnion A -> BinOp of (Fin A) means :Def4: :: SETWISEO:def 4 for x, y being Element of Fin A holds it . (x,y) = x \/ y; existence ex b1 being BinOp of (Fin A) st for x, y being Element of Fin A holds b1 . (x,y) = x \/ y proof end; uniqueness for b1, b2 being BinOp of (Fin A) st ( for x, y being Element of Fin A holds b1 . (x,y) = x \/ y ) & ( for x, y being Element of Fin A holds b2 . (x,y) = x \/ y ) holds b1 = b2 proof end; end; :: deftheorem Def4 defines FinUnion SETWISEO:def 4 : for A being set for b2 being BinOp of (Fin A) holds ( b2 = FinUnion A iff for x, y being Element of Fin A holds b2 . (x,y) = x \/ y ); theorem Th34: :: SETWISEO:37 for A being set holds FinUnion A is idempotent proof end; theorem Th35: :: SETWISEO:38 for A being set holds FinUnion A is commutative proof end; theorem Th36: :: SETWISEO:39 for A being set holds FinUnion A is associative proof end; theorem Th37: :: SETWISEO:40 for A being set holds {}. A is_a_unity_wrt FinUnion A proof end; theorem Th38: :: SETWISEO:41 for A being set holds FinUnion A is having_a_unity proof end; theorem :: SETWISEO:42 for A being set holds the_unity_wrt () is_a_unity_wrt FinUnion A by ; theorem Th40: :: SETWISEO:43 for A being set holds the_unity_wrt () = {} proof end; definition let X be non empty set ; let 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 ()$$ (B,f);
coherence
() $$(B,f) is Element of Fin A ; end; :: deftheorem defines FinUnion SETWISEO:def 5 : for X being non empty set for A being set for B being Element of Fin X for f being Function of X,(Fin A) holds FinUnion (B,f) = ()$$ (B,f);

theorem :: SETWISEO:44
for X being non empty set
for A being set
for f being Function of X,(Fin A)
for i being Element of X holds FinUnion ({.i.},f) = f . i
proof end;

theorem :: SETWISEO:45
for X being non empty set
for A being set
for f being Function of X,(Fin A)
for i, j being Element of X holds FinUnion ({.i,j.},f) = (f . i) \/ (f . j)
proof end;

theorem :: SETWISEO:46
for X being non empty set
for A being set
for f being Function of X,(Fin A)
for i, j, k being Element of X holds FinUnion ({.i,j,k.},f) = ((f . i) \/ (f . j)) \/ (f . k)
proof end;

theorem Th44: :: SETWISEO:47
for X being non empty set
for A being set
for f being Function of X,(Fin A) holds FinUnion (({}. X),f) = {}
proof end;

theorem Th45: :: SETWISEO:48
for X being non empty set
for A being set
for f being Function of X,(Fin A)
for i being Element of X
for B being Element of Fin X holds FinUnion ((B \/ {.i.}),f) = (FinUnion (B,f)) \/ (f . i)
proof end;

theorem Th46: :: SETWISEO:49
for X being non empty set
for A being set
for f being Function of X,(Fin A)
for B being Element of Fin X holds FinUnion (B,f) = union (f .: B)
proof end;

theorem :: SETWISEO:50
for X being non empty set
for A being set
for f being Function of X,(Fin A)
for B1, B2 being Element of Fin X holds FinUnion ((B1 \/ B2),f) = (FinUnion (B1,f)) \/ (FinUnion (B2,f))
proof end;

theorem :: SETWISEO:51
for X, Y being non empty set
for A being set
for B being Element of Fin X
for f being Function of X,Y
for g being Function of Y,(Fin A) holds FinUnion ((f .: B),g) = FinUnion (B,(g * f))
proof end;

theorem Th49: :: SETWISEO:52
for A, X being non empty set
for Y being set
for G being BinOp of A st G is commutative & G is associative & G is idempotent holds
for B being Element of Fin X st B <> {} holds
for f being Function of X,(Fin Y)
for 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)) proof end; theorem Th50: :: SETWISEO:53 for X, Z being non empty set for Y being set for G being BinOp of Z st G is commutative & G is associative & G is idempotent & G is having_a_unity holds 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)) ) holds for B being Element of Fin X holds g . (FinUnion (B,f)) = G$$ (B,(g * f))
proof end;

definition
let A be set ;
func singleton A -> Function of A,(Fin A) means :Def6: :: SETWISEO:def 6
for x being object st x in A holds
it . x = {x};
existence
ex b1 being Function of A,(Fin A) st
for x being object st x in A holds
b1 . x = {x}
proof end;
uniqueness
for b1, b2 being Function of A,(Fin A) st ( for x being object st x in A holds
b1 . x = {x} ) & ( for x being object st x in A holds
b2 . x = {x} ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines singleton SETWISEO:def 6 :
for A being set
for b2 being Function of A,(Fin A) holds
( b2 = singleton A iff for x being object st x in A holds
b2 . x = {x} );

theorem Th51: :: SETWISEO:54
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} )
proof end;

theorem Th52: :: SETWISEO:55
for X being non empty set
for x being set
for y being Element of X holds
( x in () . y iff x = y )
proof end;

theorem :: SETWISEO:56
for X being non empty set
for x, y, z being Element of X st x in () . z & y in () . z holds
x = y
proof end;

Lm2: for D being non empty set
for X, P being set
for f being Function of X,D holds f .: P c= D

;

theorem Th54: :: SETWISEO:57
for X being non empty set
for A being set
for f being Function of X,(Fin A)
for B being Element of Fin X
for x being set holds
( x in FinUnion (B,f) iff ex i being Element of X st
( i in B & x in f . i ) )
proof end;

theorem :: SETWISEO:58
for X being non empty set
for B being Element of Fin X holds FinUnion (B,()) = B
proof end;

theorem :: SETWISEO:59
for X being non empty set
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) ) holds
for B being Element of Fin X holds g . (FinUnion (B,f)) = FinUnion (B,(g * f))
proof end;