:: Relations of Tolerance
:: by Krzysztof Hryniewiecki
::
:: Received September 20, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

registration
cluster Relation-like empty  ->  reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive for set ;
coherence
 for b1 being Relation st b1 is empty holds
( b1 is reflexive & b1 is irreflexive & b1 is symmetric & b1 is antisymmetric & b1 is asymmetric & b1 is connected & b1 is strongly_connected & b1 is transitive )
proofend;
end;

notation
let X be set ;
synonym  Total X for  nabla X;
end;

definition
let R be Relation;
let Y be set ;
:: original:|_2
redefine funcR |_2 Y ->  Relation of Y,Y;
coherence
 R |_2 Y is Relation of Y,Y by XBOOLE_1:17;
end;

theorem :: TOLER_1:1
for X being set holds rng (Total X) = X
proofend;

theorem Th2: :: TOLER_1:2
for X, x, y being set st x in X & y in X holds
[x,y] in Total X
proofend;

theorem :: TOLER_1:3
for X, x, y being set st x in field (Total X) & y in field (Total X) holds
[x,y] in Total X
proofend;

theorem :: TOLER_1:4
for X being set holds Total X is strongly_connected
proofend;

theorem :: TOLER_1:5
for X being set holds Total X is connected
proofend;

theorem :: TOLER_1:6
for X being set
for T being Tolerance of X holds rng T = X
proofend;

theorem Th7: :: TOLER_1:7
for X, x being set
for T being reflexive total Relation of X holds
( x in X iff [x,x] in T )
proofend;

theorem :: TOLER_1:8
for X being set
for T being Tolerance of X holds T is_reflexive_in X
proofend;

theorem :: TOLER_1:9
for X being set
for T being Tolerance of X holds T is_symmetric_in X
proofend;

theorem Th10: :: TOLER_1:10
for X, Y, Z being set
for R being Relation of X,Y st R is symmetric holds
R |_2 Z is symmetric
proofend;

definition
let X be set ;
let T be Tolerance of X;
let Y be Subset of X;
:: original:|_2
redefine funcT |_2 Y ->  Tolerance of Y;
coherence
 T |_2 Y is Tolerance of Y
proofend;
end;

theorem :: TOLER_1:11
for Y, X being set
for T being Tolerance of X st Y c= X holds
T |_2 Y is Tolerance of Y
proofend;

:: Set and Class of Tolerance
definition
let X be set ;
let T be Tolerance of X;
mode TolSet of T ->  set  means :Def1: :: TOLER_1:def 1
 for x, y being set st x in it & y in it holds
[x,y] in T;
existence
 ex b1 being set st
for x, y being set st x in b1 & y in b1 holds
[x,y] in T
proofend;
end;

:: deftheorem Def1 defines TolSet TOLER_1:def_1_:_
 for X being set
for T being Tolerance of X
for b3 being set holds
( b3 is TolSet of T iff for x, y being set st x in b3 & y in b3 holds
[x,y] in T );

theorem Th12: :: TOLER_1:12
for X being set
for T being Tolerance of X holds {} is TolSet of T
proofend;

definition
let X be set ;
let T be Tolerance of X;
let IT be TolSet of T;
attrIT is TolClass-like  means :Def2: :: TOLER_1:def 2
 for x being set st not x in IT & x in X holds
ex y being set st
( y in IT & not [x,y] in T );
end;

:: deftheorem Def2 defines TolClass-like TOLER_1:def_2_:_
 for X being set
for T being Tolerance of X
for IT being TolSet of T holds
( IT is TolClass-like iff for x being set st not x in IT & x in X holds
ex y being set st
( y in IT & not [x,y] in T ) );

registration
let X be set ;
let T be Tolerance of X;
cluster TolClass-like for TolSet of T;
existence
 ex b1 being TolSet of T st b1 is TolClass-like
proofend;
end;

definition
let X be set ;
let T be Tolerance of X;
mode TolClass of T is TolClass-like TolSet of T;
end;

theorem :: TOLER_1:13
for X being set
for T being Tolerance of X st {} is TolClass of T holds
T = {}
proofend;

theorem :: TOLER_1:14
{} is Tolerance of {} by RELSET_1:12;

theorem Th15: :: TOLER_1:15
for X being set
for T being Tolerance of X
for x, y being set st [x,y] in T holds
{x,y} is TolSet of T
proofend;

theorem :: TOLER_1:16
for X being set
for T being Tolerance of X
for x being set st x in X holds
{x} is TolSet of T
proofend;

theorem :: TOLER_1:17
for X being set
for T being Tolerance of X
for Y, Z being set st Y is TolSet of T holds
Y /\ Z is TolSet of T
proofend;

theorem Th18: :: TOLER_1:18
for Y, X being set
for T being Tolerance of X st Y is TolSet of T holds
Y c= X
proofend;

theorem Th19: :: TOLER_1:19
for X being set
for T being Tolerance of X
for Y being TolSet of T ex Z being TolClass of T st Y c= Z
proofend;

theorem Th20: :: TOLER_1:20
for X being set
for T being Tolerance of X
for x, y being set st [x,y] in T holds
ex Z being TolClass of T st
( x in Z & y in Z )
proofend;

theorem Th21: :: TOLER_1:21
for X being set
for T being Tolerance of X
for x being set st x in X holds
ex Z being TolClass of T st x in Z
proofend;

theorem :: TOLER_1:22
for X being set
for T being Tolerance of X holds T c= Total X
proofend;

theorem :: TOLER_1:23
for X being set
for T being Tolerance of X holds id X c= T
proofend;

scheme :: TOLER_1:sch 1
ToleranceEx{ F1() ->  set , P1[ set , set ] } :
 ex T being Tolerance of F1() st
for x, y being set st x in F1() & y in F1() holds
( [x,y] in T iff P1[x,y] )
provided
A1: for x being set st x in F1() holds
P1[x,x] and
A2: for x, y being set st x in F1() & y in F1() & P1[x,y] holds
P1[y,x]
proofend;

theorem :: TOLER_1:24
for Y being set ex T being Tolerance of (union Y) st
for Z being set st Z in Y holds
Z is TolSet of T
proofend;

theorem :: TOLER_1:25
for Y being set
for T, R being Tolerance of (union Y) st ( for x, y being set holds
( [x,y] in T iff ex Z being set st
( Z in Y & x in Z & y in Z ) ) ) & ( for x, y being set holds
( [x,y] in R iff ex Z being set st
( Z in Y & x in Z & y in Z ) ) ) holds
T = R
proofend;

theorem Th26: :: TOLER_1:26
for X being set
for T, R being Tolerance of X st ( for Z being set holds
( Z is TolClass of T iff Z is TolClass of R ) ) holds
T = R
proofend;

notation
let X, Y be set ;
let T be Relation of X,Y;
let x be set ;
synonym  neighbourhood (x,T) for  Class (X,Y);
end;

theorem Th27: :: TOLER_1:27
for X, x being set
for T being Tolerance of X
for y being set holds
( y in neighbourhood (,) iff [x,y] in T )
proofend;

theorem :: TOLER_1:28
for X, x being set
for T being Tolerance of X
for Y being set st ( for Z being set holds
( Z in Y iff ( x in Z & Z is TolClass of T ) ) ) holds
neighbourhood (,) = union Y
proofend;

theorem :: TOLER_1:29
for X, x being set
for T being Tolerance of X
for Y being set st ( for Z being set holds
( Z in Y iff ( x in Z & Z is TolSet of T ) ) ) holds
neighbourhood (,) = union Y
proofend;

:: Family of sets and classes of proximity
definition
let X be set ;
let T be Tolerance of X;
func TolSets T ->  set  means :Def3: :: TOLER_1:def 3
 for Y being set holds
( Y in it iff Y is TolSet of T );
existence
 ex b1 being set st
for Y being set holds
( Y in b1 iff Y is TolSet of T )
proofend;
uniqueness
 for b1, b2 being set st ( for Y being set holds
( Y in b1 iff Y is TolSet of T ) ) & ( for Y being set holds
( Y in b2 iff Y is TolSet of T ) ) holds
b1 = b2
proofend;
func TolClasses T ->  set  means :Def4: :: TOLER_1:def 4
 for Y being set holds
( Y in it iff Y is TolClass of T );
existence
 ex b1 being set st
for Y being set holds
( Y in b1 iff Y is TolClass of T )
proofend;
uniqueness
 for b1, b2 being set st ( for Y being set holds
( Y in b1 iff Y is TolClass of T ) ) & ( for Y being set holds
( Y in b2 iff Y is TolClass of T ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines TolSets TOLER_1:def_3_:_
 for X being set
for T being Tolerance of X
for b3 being set holds
( b3 = TolSets T iff for Y being set holds
( Y in b3 iff Y is TolSet of T ) );

:: deftheorem Def4 defines TolClasses TOLER_1:def_4_:_
 for X being set
for T being Tolerance of X
for b3 being set holds
( b3 = TolClasses T iff for Y being set holds
( Y in b3 iff Y is TolClass of T ) );

theorem :: TOLER_1:30
for X being set
for R, T being Tolerance of X st TolClasses R c= TolClasses T holds
R c= T
proofend;

theorem :: TOLER_1:31
for X being set
for T, R being Tolerance of X st TolClasses T = TolClasses R holds
T = R
proofend;

theorem :: TOLER_1:32
for X being set
for T being Tolerance of X holds union (TolClasses T) = X
proofend;

theorem :: TOLER_1:33
for X being set
for T being Tolerance of X holds union (TolSets T) = X
proofend;

theorem :: TOLER_1:34
for X being set
for T being Tolerance of X st ( for x being set st x in X holds
neighbourhood (,) is TolSet of T ) holds
T is transitive
proofend;

theorem :: TOLER_1:35
for X being set
for T being Tolerance of X st T is transitive holds
for x being set st x in X holds
neighbourhood (,) is TolClass of T
proofend;

theorem :: TOLER_1:36
for X being set
for T being Tolerance of X
for x being set
for Y being TolClass of T st x in Y holds
Y c= neighbourhood (,)
proofend;

theorem :: TOLER_1:37
for X being set
for R, T being Tolerance of X holds
( TolSets R c= TolSets T iff R c= T )
proofend;

theorem :: TOLER_1:38
for X being set
for T being Tolerance of X holds TolClasses T c= TolSets T
proofend;

theorem :: TOLER_1:39
for X being set
for R, T being Tolerance of X st ( for x being set st x in X holds
neighbourhood (,) c= neighbourhood (,) ) holds
R c= T
proofend;

theorem :: TOLER_1:40
for X being set
for T being Tolerance of X holds T c= T * T
proofend;