:: A theory of partitions, { I }
:: by Shunichi Kobayashi and Kui Jia
::
:: Received October 5, 1998
:: Copyright (c) 1998 Association of Mizar Users
theorem Th1: :: PARTIT1:1
theorem :: PARTIT1:2
canceled;
theorem Th3: :: PARTIT1:3
theorem Th4: :: PARTIT1:4
theorem Th5: :: PARTIT1:5
theorem :: PARTIT1:6
canceled;
theorem Th7: :: PARTIT1:7
:: deftheorem Def1 defines is_a_dependent_set_of PARTIT1:def 1 :
:: deftheorem Def2 defines is_min_depend PARTIT1:def 2 :
theorem Th8: :: PARTIT1:8
theorem Th9: :: PARTIT1:9
theorem Th10: :: PARTIT1:10
theorem Th11: :: PARTIT1:11
theorem Th12: :: PARTIT1:12
theorem Th13: :: PARTIT1:13
theorem :: PARTIT1:14
:: deftheorem Def3 defines PARTITIONS PARTIT1:def 3 :
:: deftheorem defines '/\' PARTIT1:def 4 :
theorem :: PARTIT1:15
theorem :: PARTIT1:16
theorem Th17: :: PARTIT1:17
definition
let Y be non
empty set ;
let PA,
PB be
a_partition of
Y;
func PA '\/' PB -> a_partition of
Y means :
Def5:
:: PARTIT1:def 5
for
d being
set holds
(
d in it iff
d is_min_depend PA,
PB );
existence
ex b1 being a_partition of Y st
for d being set holds
( d in b1 iff d is_min_depend PA,PB )
uniqueness
for b1, b2 being a_partition of Y st ( for d being set holds
( d in b1 iff d is_min_depend PA,PB ) ) & ( for d being set holds
( d in b2 iff d is_min_depend PA,PB ) ) holds
b1 = b2
commutativity
for b1, PA, PB being a_partition of Y st ( for d being set holds
( d in b1 iff d is_min_depend PA,PB ) ) holds
for d being set holds
( d in b1 iff d is_min_depend PB,PA )
end;
:: deftheorem Def5 defines '\/' PARTIT1:def 5 :
theorem :: PARTIT1:18
canceled;
theorem Th19: :: PARTIT1:19
theorem :: PARTIT1:20
theorem Th21: :: PARTIT1:21
theorem :: PARTIT1:22
theorem Th23: :: PARTIT1:23
:: deftheorem Def6 defines ERl PARTIT1:def 6 :
:: deftheorem defines Rel PARTIT1:def 7 :
theorem Th24: :: PARTIT1:24
theorem Th25: :: PARTIT1:25
theorem Th26: :: PARTIT1:26
theorem Th27: :: PARTIT1:27
theorem Th28: :: PARTIT1:28
theorem Th29: :: PARTIT1:29
theorem :: PARTIT1:30
theorem :: PARTIT1:31
theorem :: PARTIT1:32
theorem Th33: :: PARTIT1:33
theorem :: PARTIT1:34
:: deftheorem PARTIT1:def 8 :
canceled;
:: deftheorem defines %O PARTIT1:def 9 :
theorem :: PARTIT1:35
theorem Th36: :: PARTIT1:36
theorem Th37: :: PARTIT1:37
theorem Th38: :: PARTIT1:38
theorem :: PARTIT1:39
theorem :: PARTIT1:40
theorem :: PARTIT1:41