:: Some Basic Properties of Many Sorted Sets
:: by Artur Korni{\l}owicz
::
:: Received September 29, 1995
:: Copyright (c) 1995 Association of Mizar Users
theorem Th1: :: PZFMISC1:1
theorem :: PZFMISC1:2
theorem :: PZFMISC1:3
:: deftheorem Def1 defines { PZFMISC1:def 1 :
definition
let I be
set ;
let A,
B be
ManySortedSet of
I;
func {A,B} -> ManySortedSet of
I means :
Def2:
:: PZFMISC1:def 2
for
i being
set st
i in I holds
it . i = {(A . i),(B . i)};
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = {(A . i),(B . i)}
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = {(A . i),(B . i)} ) & ( for i being set st i in I holds
b2 . i = {(A . i),(B . i)} ) holds
b1 = b2
commutativity
for b1, A, B being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = {(A . i),(B . i)} ) holds
for i being set st i in I holds
b1 . i = {(B . i),(A . i)}
;
end;
:: deftheorem Def2 defines { PZFMISC1:def 2 :
theorem :: PZFMISC1:4
theorem :: PZFMISC1:5
theorem :: PZFMISC1:6
theorem :: PZFMISC1:7
canceled;
theorem :: PZFMISC1:8
theorem :: PZFMISC1:9
theorem :: PZFMISC1:10
theorem :: PZFMISC1:11
theorem :: PZFMISC1:12
theorem :: PZFMISC1:13
canceled;
theorem :: PZFMISC1:14
theorem :: PZFMISC1:15
theorem :: PZFMISC1:16
theorem :: PZFMISC1:17
theorem :: PZFMISC1:18
theorem :: PZFMISC1:19
theorem :: PZFMISC1:20
theorem :: PZFMISC1:21
canceled;
theorem :: PZFMISC1:22
theorem :: PZFMISC1:23
theorem :: PZFMISC1:24
theorem :: PZFMISC1:25
theorem :: PZFMISC1:26
theorem :: PZFMISC1:27
theorem :: PZFMISC1:28
theorem :: PZFMISC1:29
theorem :: PZFMISC1:30
theorem :: PZFMISC1:31
theorem :: PZFMISC1:32
theorem :: PZFMISC1:33
theorem :: PZFMISC1:34
theorem :: PZFMISC1:35
theorem :: PZFMISC1:36
theorem :: PZFMISC1:37
theorem :: PZFMISC1:38
theorem :: PZFMISC1:39
theorem :: PZFMISC1:40
theorem :: PZFMISC1:41
theorem :: PZFMISC1:42
theorem :: PZFMISC1:43
theorem :: PZFMISC1:44
theorem :: PZFMISC1:45
theorem :: PZFMISC1:46
theorem :: PZFMISC1:47
theorem :: PZFMISC1:48
theorem :: PZFMISC1:49
theorem :: PZFMISC1:50
theorem :: PZFMISC1:51
theorem :: PZFMISC1:52
theorem :: PZFMISC1:53
theorem :: PZFMISC1:54
theorem :: PZFMISC1:55
theorem :: PZFMISC1:56
theorem :: PZFMISC1:57
canceled;
theorem :: PZFMISC1:58
theorem :: PZFMISC1:59
theorem :: PZFMISC1:60
theorem :: PZFMISC1:61
theorem :: PZFMISC1:62
theorem :: PZFMISC1:63
theorem :: PZFMISC1:64
theorem :: PZFMISC1:65
theorem :: PZFMISC1:66
theorem :: PZFMISC1:67
theorem :: PZFMISC1:68
theorem :: PZFMISC1:69
theorem :: PZFMISC1:70
theorem :: PZFMISC1:71
theorem :: PZFMISC1:72
theorem :: PZFMISC1:73
theorem :: PZFMISC1:74
theorem :: PZFMISC1:75
theorem :: PZFMISC1:76
for
I being
set for
x,
y,
X being
ManySortedSet of
I holds
(
[|{x,y},X|] = [|{x},X|] \/ [|{y},X|] &
[|X,{x,y}|] = [|X,{x}|] \/ [|X,{y}|] )
theorem :: PZFMISC1:77
theorem :: PZFMISC1:78
theorem :: PZFMISC1:79
theorem :: PZFMISC1:80
theorem :: PZFMISC1:81
theorem :: PZFMISC1:82
theorem :: PZFMISC1:83
theorem :: PZFMISC1:84
:: deftheorem defines is_transformable_to PZFMISC1:def 3 :