The abstract of the Mizar article:

Relations of Tolerance

by

Krzysztof Hryniewiecki

Received September 20, 1990

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;