:: Equivalence Relations and Classes of Abstraction
:: by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received November 16, 1989
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem defines nabla EQREL_1:def 1 :
theorem :: EQREL_1:1
theorem :: EQREL_1:2
canceled;
theorem :: EQREL_1:3
canceled;
theorem :: EQREL_1:4
theorem :: EQREL_1:5
canceled;
theorem :: EQREL_1:6
theorem Th7: :: EQREL_1:7
Lm1:
for x, y, X being set
for R being Relation of X st [x,y] in R holds
( x in X & y in X )
theorem :: EQREL_1:8
canceled;
theorem :: EQREL_1:9
canceled;
theorem :: EQREL_1:10
canceled;
theorem Th11: :: EQREL_1:11
theorem Th12: :: EQREL_1:12
theorem Th13: :: EQREL_1:13
theorem :: EQREL_1:14
theorem :: EQREL_1:15
canceled;
theorem Th16: :: EQREL_1:16
theorem :: EQREL_1:17
theorem :: EQREL_1:18
canceled;
theorem Th19: :: EQREL_1:19
theorem Th20: :: EQREL_1:20
:: deftheorem EQREL_1:def 2 :
canceled;
:: deftheorem Def3 defines "\/" EQREL_1:def 3 :
theorem :: EQREL_1:21
theorem :: EQREL_1:22
theorem :: EQREL_1:23
theorem :: EQREL_1:24
theorem :: EQREL_1:25
scheme :: EQREL_1:sch 1
ExEqRel{
F1()
-> set ,
P1[
set ,
set ] } :
provided
A1:
for
x being
set st
x in F1() holds
P1[
x,
x]
and A2:
for
x,
y being
set st
P1[
x,
y] holds
P1[
y,
x]
and A3:
for
x,
y,
z being
set st
P1[
x,
y] &
P1[
y,
z] holds
P1[
x,
z]
:: deftheorem EQREL_1:def 4 :
canceled;
theorem :: EQREL_1:26
theorem Th27: :: EQREL_1:27
theorem Th28: :: EQREL_1:28
theorem :: EQREL_1:29
theorem :: EQREL_1:30
Lm2:
for X, y being set
for EqR being Equivalence_Relation of X
for x being set st x in X holds
( [x,y] in EqR iff Class EqR,x = Class EqR,y )
theorem Th31: :: EQREL_1:31
theorem Th32: :: EQREL_1:32
theorem Th33: :: EQREL_1:33
theorem Th34: :: EQREL_1:34
theorem Th35: :: EQREL_1:35
theorem :: EQREL_1:36
theorem Th37: :: EQREL_1:37
theorem :: EQREL_1:38
:: deftheorem Def5 defines Class EQREL_1:def 5 :
theorem :: EQREL_1:39
canceled;
theorem Th40: :: EQREL_1:40
:: deftheorem Def6 defines a_partition EQREL_1:def 6 :
theorem Th41: :: EQREL_1:41
theorem Th42: :: EQREL_1:42
theorem Th43: :: EQREL_1:43
theorem :: EQREL_1:44
theorem :: EQREL_1:45
:: deftheorem defines SmallestPartition EQREL_1:def 7 :
theorem :: EQREL_1:46
:: deftheorem Def8 defines EqClass EQREL_1:def 8 :
theorem Th47: :: EQREL_1:47
theorem Th48: :: EQREL_1:48
Lm3:
for X being set holds {} is Family-Class of X
by XBOOLE_1:2;
:: deftheorem EQREL_1:def 9 :
canceled;
:: deftheorem Def10 defines partition-membered EQREL_1:def 10 :
theorem Th49: :: EQREL_1:49
theorem Th50: :: EQREL_1:50
Lm4:
for X being non empty set
for x being Element of X
for F being Part-Family of X
for A being set st A in { (EqClass x,S) where S is a_partition of X : S in F } holds
ex T being a_partition of X st
( T in F & A = EqClass x,T )
theorem :: EQREL_1:51
:: deftheorem defines Intersection EQREL_1:def 11 :
theorem Th52: :: EQREL_1:52
theorem :: EQREL_1:53
theorem :: EQREL_1:54