Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Relations of Tolerance

by
Krzysztof Hryniewiecki

MML identifier: TOLER_1
[ Mizar article, MML identifier index ]

```environ

vocabulary RELAT_1, BOOLE, RELAT_2, EQREL_1, WELLORD1, ZFMISC_1, TARSKI,
TOLER_1, HAHNBAN, PARTFUN1, FUNCT_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, RELAT_2,
PARTFUN1, ORDINAL1, WELLORD1, EQREL_1;
constructors RELAT_2, WELLORD1, EQREL_1, ORDINAL1, PARTFUN1, XBOOLE_0;
clusters RELAT_1, RELSET_1, SUBSET_1, ZFMISC_1, PARTFUN1, XBOOLE_0, EQREL_1;
requirements SUBSET, BOOLE;

begin

reserve X,Y,Z,x,y,z for set;

theorem :: TOLER_1:1
field {} = {};

theorem :: TOLER_1:2
{} is reflexive;

theorem :: TOLER_1:3
{} is symmetric;

theorem :: TOLER_1:4
{} is irreflexive;

theorem :: TOLER_1:5
{} is antisymmetric;

theorem :: TOLER_1:6
{} is asymmetric;

theorem :: TOLER_1:7
{} is connected;

theorem :: TOLER_1:8
{} is strongly_connected;

theorem :: TOLER_1:9
{} is transitive;

definition
cluster {} -> reflexive irreflexive symmetric antisymmetric asymmetric
connected strongly_connected transitive;
end;

::::::::::::::::::::
:: Total relation ::
::::::::::::::::::::

definition let X;
redefine func nabla X;
synonym Total X;
end;

definition let R be Relation, Y be set;
redefine func R |_2 Y -> Relation of Y,Y;
end;

canceled 2;

theorem :: TOLER_1:12
dom Total X = X;

theorem :: TOLER_1:13
rng Total X = X;

canceled;

theorem :: TOLER_1:15
for x,y st x in X & y in X holds [x,y] in Total X;

theorem :: TOLER_1:16
for x,y st x in field Total X & y in field Total X holds
[x,y] in Total X;

canceled 2;

theorem :: TOLER_1:19
Total X is strongly_connected;

canceled;

theorem :: TOLER_1:21
Total X is connected;

::  Tolerance

reserve T,R for Tolerance of X;

canceled 2;

theorem :: TOLER_1:24
for T being Tolerance of X holds dom T = X;

theorem :: TOLER_1:25
for T being Tolerance of X holds rng T = X;

canceled;

theorem :: TOLER_1:27
for T being total reflexive Relation of X holds x in X iff [x,x] in T;

theorem :: TOLER_1:28
for T being Tolerance of X holds T is_reflexive_in X;

theorem :: TOLER_1:29
for T being Tolerance of X holds T is_symmetric_in X;

canceled 2;

theorem :: TOLER_1:32
for R be Relation of X,Y st R is symmetric holds
R |_2 Z is symmetric;

definition let X,T;let Y be Subset of X;
canceled 2;
redefine func T |_2 Y -> Tolerance of Y;
end;

theorem :: TOLER_1:33
Y c= X implies T|_2 Y is Tolerance of Y;

:: Set and Class of Tolerance

definition let X;let T be Tolerance of X;
mode TolSet of T -> set means
:: TOLER_1:def 3
for x,y st x in it & y in it holds [x,y] in T;
end;

theorem :: TOLER_1:34
{} is TolSet of T;

definition let X;let T be Tolerance of X;
let IT be TolSet of T;
attr IT is TolClass-like means
:: TOLER_1:def 4
for x st not x in IT & x in X ex y st y in IT & not [x,y] in T;
end;

definition let X;let T be Tolerance of X;
cluster TolClass-like TolSet of T;
end;

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

canceled 3;

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

theorem :: TOLER_1:39
{} is Tolerance of {};

theorem :: TOLER_1:40
for x,y st [x,y] in T holds {x,y} is TolSet of T;

theorem :: TOLER_1:41
for x st x in X holds {x} is TolSet of T;

theorem :: TOLER_1:42
for Y,Z st Y is TolSet of T & Z is TolSet of T holds Y /\ Z is TolSet of T;

theorem :: TOLER_1:43
Y is TolSet of T implies Y c= X;

canceled;

theorem :: TOLER_1:45
for Y being TolSet of T ex Z being TolClass of T st Y c= Z;

theorem :: TOLER_1:46
for x,y st [x,y] in T ex Z being TolClass of T st x in Z & y in Z;

theorem :: TOLER_1:47
for x st x in X ex Z being TolClass of T st x in Z;

canceled;

theorem :: TOLER_1:49
T c= Total X;

theorem :: TOLER_1:50
id X c= T;

scheme ToleranceEx{A() -> set,P[set,set]}:
ex T being Tolerance of A() st
for x,y st x in A() & y in A() holds [x,y] in T iff P[x,y]
provided
for x st x in A() holds P[x,x] and
for x,y st x in A() & y in A() & P[x,y] holds P[y,x];

theorem :: TOLER_1:51
for Y ex T being Tolerance of union Y st
for Z st Z in Y holds Z is TolSet of T;

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

theorem :: TOLER_1:53
for T,R being Tolerance of X st
for Z holds Z is TolClass of T iff Z is TolClass of R
holds T = R;

:: Tolerance neighbourhood

definition let X; let T be Tolerance of X; let x;
canceled;
redefine func Class (T,x);
synonym neighbourhood (x, T);
end;

theorem :: TOLER_1:54
for y being set holds y in neighbourhood(x,T) iff [x,y] in T;

canceled 3;

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

theorem :: TOLER_1:59
for Y st for Z holds Z in Y iff x in Z & Z is TolSet of T holds
neighbourhood(x,T) = union Y;

:::::::::::::::::::::::::::::::::::::::::::::
:: Family of sets and classes of proximity ::
:::::::::::::::::::::::::::::::::::::::::::::
definition let X; let T be Tolerance of X;
func TolSets T -> set means
:: TOLER_1:def 6
for Y holds Y in it iff Y is TolSet of T;

func TolClasses T -> set means
:: TOLER_1:def 7
for Y holds Y in it iff Y is TolClass of T;
end;

canceled 4;

theorem :: TOLER_1:64
TolClasses R c= TolClasses T implies R c= T;

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

theorem :: TOLER_1:66
union TolClasses T = X;

theorem :: TOLER_1:67
union TolSets T = X;

theorem :: TOLER_1:68
(for x st x in X holds neighbourhood(x,T) is TolSet of T)
implies T is transitive;

theorem :: TOLER_1:69
T is transitive implies
(for x st x in X holds neighbourhood(x,T) is TolClass of T);

theorem :: TOLER_1:70
for x for Y being TolClass of T st x in Y holds
Y c= neighbourhood(x,T);

theorem :: TOLER_1:71
TolSets R c= TolSets T iff R c= T;

theorem :: TOLER_1:72
TolClasses T c= TolSets T;

theorem :: TOLER_1:73
(for x st x in X holds neighbourhood(x,R) c= neighbourhood(x,T))
implies R c= T;

theorem :: TOLER_1:74
T c= T*T;
```