The Mizar article:

Relations of Tolerance

by
Krzysztof Hryniewiecki

Received September 20, 1990

Copyright (c) 1990 Association of Mizar Users

MML identifier: TOLER_1
[ 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;
 definitions TARSKI, RELAT_1, RELAT_2;
 theorems TARSKI, RELAT_1, RELSET_1, RELAT_2, ZFMISC_1, WELLORD1, ENUMSET1,
      ORDERS_2, EQREL_1, ORDINAL1, XBOOLE_0, XBOOLE_1, ORDERS_1, PARTFUN1;
 schemes XBOOLE_0;

begin

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

theorem Th1:
  field {} = {}
proof
  thus field {} = {} \/ {} by RELAT_1:60,def 6
     .= {};
end;

theorem Th2:
  {} is reflexive
proof
    x in {} implies [x,x] in {};
  then {} is_reflexive_in field {} by Th1,RELAT_2:def 1;
 hence thesis by RELAT_2:def 9;
end;

theorem Th3:
  {} is symmetric
proof let x,y; assume x in field {} & y in field {} & [x,y] in {};
  hence thesis;
end;

theorem Th4:
    {} is irreflexive
proof
    {} is_irreflexive_in field {}
   proof let x; assume x in field {};
    thus not [x,x] in {};
   end;
 hence thesis by RELAT_2:def 10;
end;

theorem Th5:
    {} is antisymmetric
proof
    {} is_antisymmetric_in field {}
    proof let x,y; assume x in field {} & y in field {} &
        [x,y] in {} & [y,x] in {};
      hence x = y;
    end;
  hence thesis by RELAT_2:def 12;
end;

theorem Th6:
    {} is asymmetric
proof
    {} is_asymmetric_in field {}
    proof let x,y; assume x in field {} & y in field {} & [x,y] in {};
      thus not [y,x] in {};
    end;
  hence thesis by RELAT_2:def 13;
end;

theorem Th7:
    {} is connected
proof
    {} is_connected_in field {}
    proof let x,y; assume x in field {} & y in field {} & x <> y;
     hence [x,y] in {} or [y,x] in {} by Th1;
    end;
  hence thesis by RELAT_2:def 14;
end;

theorem Th8:
    {} is strongly_connected
proof
    {} is_strongly_connected_in field {}
    proof let x,y; assume x in field {} & y in field {};
     hence [x,y] in {} or [y,x] in {} by Th1;
    end;
  hence thesis by RELAT_2:def 15;
end;

theorem Th9:
    {} is transitive
proof
     {} is_transitive_in field {}
     proof let x,y,z; assume x in field {} & y in field {} &
       z in field {} & [x,y] in {} & [y,z] in {};
      hence [x,z] in {};
     end;
  hence thesis by RELAT_2:def 16;
end;

definition
  cluster {} -> reflexive irreflexive symmetric antisymmetric asymmetric
    connected strongly_connected transitive;
  coherence by Th2, Th3, Th4, Th5, Th6, Th7, Th8, Th9;
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;
  coherence
   proof
       R |_2 Y = R /\ [:Y,Y:] by WELLORD1:def 6;
     then R |_2 Y c= [:Y,Y:] by XBOOLE_1:17;
   hence R|_2 Y is Relation of Y,Y by RELSET_1:def 1;
   end;
end;

canceled 2;

theorem
  dom Total X = X by PARTFUN1:def 4;

theorem
  rng Total X = X
proof
    for x holds x in X iff ex y st [y,x] in Total X
    proof let x;
      thus x in X implies ex y st [y,x] in Total X
        proof assume A1: x in X; take x;
            [x,x] in [:X,X:] by A1,ZFMISC_1:106;
         hence thesis by EQREL_1:def 1;
        end;
      given y such that A2: [y,x] in Total X;
      thus thesis by A2,ZFMISC_1:106;
    end;
  hence thesis by RELAT_1:def 5;
end;

canceled;

theorem Th15:
  for x,y st x in X & y in X holds [x,y] in Total X
proof let x,y; assume x in X & y in X;
 then [x,y] in [:X,X:] by ZFMISC_1:106;
 hence thesis by EQREL_1:def 1;
end;

theorem
  for x,y st x in field Total X & y in field Total X holds
    [x,y] in Total X
proof let x,y; assume x in field Total X & y in field Total X;
  then x in X & y in X by ORDERS_1:97;
 hence thesis by Th15;
end;

canceled 2;

theorem
    Total X is strongly_connected
proof let x,y; assume x in field Total X & y in field Total X;
  then x in X & y in X by ORDERS_1:97;
  then [x,y] in [:X,X:] by ZFMISC_1:106;
 hence thesis by EQREL_1:def 1;
end;

canceled;

theorem
  Total X is connected
proof let x,y; assume x in field Total X & y in field Total X & x<>y;
  then x in X & y in X by ORDERS_1:97;
  then [x,y] in [:X,X:] by ZFMISC_1:106;
 hence thesis by EQREL_1:def 1;
end;

::  Tolerance

reserve T,R for Tolerance of X;

canceled 2;

theorem
  for T being Tolerance of X holds dom T = X by PARTFUN1:def 4;

theorem
   for T being Tolerance of X holds rng T = X
proof let T be Tolerance of X;
     for x holds x in rng T iff x in X
    proof let x;
       x in X implies x in rng T
     proof assume A1: x in X;
       field T = X by ORDERS_1:97;
       then T is_reflexive_in X by RELAT_2:def 9;
       then [x,x] in T by A1,RELAT_2:def 1;
      hence x in rng T by RELAT_1:def 5;
     end;
    hence thesis;
   end;
   hence thesis by TARSKI:2;
end;

canceled;

theorem Th27:
  for T being total reflexive Relation of X holds x in X iff [x,x] in T
proof let T be total reflexive Relation of X;
A1:     field T = X by ORDERS_1:97;
  thus x in X implies [x,x] in T by EQREL_1:11;
  assume [x,x] in T;
 hence thesis by A1,RELAT_1:30;
end;

theorem
    for T being Tolerance of X holds T is_reflexive_in X
proof let T be Tolerance of X;
 field T = X by ORDERS_1:97;
 hence thesis by RELAT_2:def 9;
end;

theorem
  for T being Tolerance of X holds T is_symmetric_in X
proof let T be Tolerance of X;
       field T = X by ORDERS_1:97;
 hence thesis by RELAT_2:def 11;
end;

Th30:
  for T being Tolerance of X holds [x,y] in T implies [y,x] in T
    by EQREL_1:12;

canceled 2;

theorem Th32:
  for R be Relation of X,Y st R is symmetric holds
    R |_2 Z is symmetric
proof let R be Relation of X,Y; assume R is symmetric;
then A1:  R is_symmetric_in field R by RELAT_2:def 11;
       now let x,y; assume A2: x in field(R|_2 Z) & y in field(R|_2 Z)
       & [x,y] in R|_2 Z;
      then A3: x in (field R) & x in Z by WELLORD1:19;
      A4: y in (field R) & y in Z by A2,WELLORD1:19;
        [x,y] in R & [x,y] in [:Z,Z:] by A2,WELLORD1:16;
      then A5: [y,x] in R by A1,A3,A4,RELAT_2:def 3;
            [y,x] in [:Z,Z:] by A2,ZFMISC_1:107;
      hence [y,x] in R|_2 Z by A5,WELLORD1:16;
     end;
   then R|_2 Z is_symmetric_in field(R|_2 Z) by RELAT_2:def 3;
 hence R|_2 Z is symmetric by RELAT_2:def 11;
end;

definition let X,T;let Y be Subset of X;
 canceled 2;
  redefine func T |_2 Y -> Tolerance of Y;
  coherence
    proof
      A1: T |_2 Y = T /\ [:Y,Y:] by WELLORD1:def 6;
           now let x; assume A2: x in Y;
           then A3: [x,x] in [:Y,Y:] by ZFMISC_1:106;
             [x,x] in T by A2,Th27;
           then [x,x] in T |_2 Y by A1,A3,XBOOLE_0:def 3;
          hence x in dom (T |_2 Y) by RELAT_1:def 4;
         end;
        then Y c= dom(T |_2 Y) by TARSKI:def 3;
      then dom(T |_2 Y) = Y by XBOOLE_0:def 10;
      hence T |_2 Y is Tolerance of Y by Th32,WELLORD1:22,PARTFUN1:def 4;
    end;
end;

theorem
    Y c= X implies T|_2 Y is Tolerance of Y
proof assume Y c= X;
  then reconsider Z = Y as Subset of X;
    T |_2 Z is Tolerance of Z;
 hence thesis;
end;

:: Set and Class of Tolerance

definition let X;let T be Tolerance of X;
  mode TolSet of T -> set means
:Def3: for x,y st x in it & y in it holds [x,y] in T;
 existence
   proof take {};
     let x,y; assume x in {} & y in {};
     hence thesis;
   end;
end;

theorem Th34:
  {} is TolSet of T
proof
  let x,y; assume x in {} & y in {};
  hence thesis;
end;

definition let X;let T be Tolerance of X;
   let IT be TolSet of T;
  attr IT is TolClass-like means
:Def4: 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;
 existence
  proof
   defpred X[set] means $1 is TolSet of T;
    consider TS being set such that A1:
       for x holds x in TS iff x in bool X & X[x] from Separation;
    A2: TS <> {}
        proof
         {} c= X by XBOOLE_1:2;
         then {} in bool X & {} is TolSet of T by Th34;
         hence TS <> {} by A1;
        end;
    A3: TS c= bool X
         proof let x; assume x in TS;
           hence x in bool X by A1;
         end;
       for Z st Z c= TS & Z is c=-linear
       ex Y st Y in TS & for X1 being set st X1 in Z holds X1 c= Y
       proof let Z such that A4: Z c= TS & Z is c=-linear;
        take union Z;
            Z c= bool X by A3,A4,XBOOLE_1:1;
          then union Z c= union bool X by ZFMISC_1:95;
          then A5: union Z c= X by ZFMISC_1:99;
                for x,y st x in union Z & y in union Z holds [x,y] in T
                proof let x,y;assume A6: x in union Z & y in union Z;
                  then consider Zx being set such that
                  A7:x in Zx & Zx in Z by TARSKI:def 4;
                  consider Zy being set such that
                  A8:y in Zy & Zy in Z by A6,TARSKI:def 4;
                  reconsider Zx as TolSet of T by A1,A4,A7;
                  reconsider Zy as TolSet of T by A1,A4,A8;
                  Zx,Zy are_c=-comparable by A4,A7,A8,ORDINAL1:def 9;
             then Zx c= Zy or Zy c= Zx by XBOOLE_0:def 9;
                   hence [x,y] in T by A7,A8,Def3;
                end;
           then union Z is TolSet of T by Def3;
         hence union Z in TS by A1,A5;
         let X1 be set;
         assume X1 in Z;
        hence X1 c= union Z by ZFMISC_1:92;
       end;
     then consider Y such that A9: Y in TS & for Z st Z in TS & Z <> Y
                               holds not Y c= Z by A2,ORDERS_2:77;
     reconsider Y as TolSet of T by A1,A9;
     take Y;
     let x such that A10: not x in Y & x in X;
     assume A11: for y st y in Y holds [x,y] in T;
     set Y1 = Y \/ {x};
       for y,z st y in Y1 & z in Y1 holds [y,z] in T
       proof let y,z; assume y in Y1 & z in Y1;
          then (y in Y or y in {x}) & (z in Y or z in {x}) by XBOOLE_0:def 2;
        then A12: (y in Y or y = x) & (z in Y or z = x) by TARSKI:def 1;
         assume A13: not [y,z] in T;
             then not [z,y] in T by Th30;
         hence contradiction by A10,A11,A12,A13,Def3,Th27;
       end;
     then A14: Y1 is TolSet of T by Def3;
          Y in bool X by A1,A9;
      then {x} c= X & Y c= X by A10,ZFMISC_1:37;
      then Y1 c= X by XBOOLE_1:8;
     then A15: Y1 in TS by A1,A14;
           Y1 <> Y
           proof assume A16: Y1 = Y;
               x in {x} by TARSKI:def 1;
            hence contradiction by A10,A16,XBOOLE_0:def 2;
           end;
        then not Y c= Y1 by A9,A15;
      hence contradiction by XBOOLE_1:7;
  end;
end;

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

canceled 3;

theorem
    for T being Tolerance of X st {} is TolClass of T holds T={}
proof let T be Tolerance of X; assume {} is TolClass of T;
  then reconsider 00 = {} as TolClass of T;
  assume T <> {};
   then consider x,y such that A1: [x,y] in T by RELAT_1:56;
      x in X by A1,ZFMISC_1:106;
    then ex z st z in 00 & not [x,z] in T by Def4;
  hence contradiction;
end;

theorem
  {} is Tolerance of {} by PARTFUN1:def 4,RELAT_1:60,RELSET_1:25;

theorem Th40:
  for x,y st [x,y] in T holds {x,y} is TolSet of T
proof let x,y; assume A1: [x,y] in T;
  then A2: x in X & y in X by ZFMISC_1:106;
        for a,b being set st a in {x,y} & b in {x,y} holds [a,b] in T
        proof let a,b be set; assume a in {x,y} & b in {x,y};
          then (a = x or a = y) & (b = x or b = y) by TARSKI:def 2;
           hence [a,b] in T by A1,A2,Th27,Th30;
        end;
    hence thesis by Def3;
end;

theorem
    for x st x in X holds {x} is TolSet of T
proof let x; assume x in X;
  then [x,x] in T by Th27;
  then {x,x} is TolSet of T by Th40;
 hence thesis by ENUMSET1:69;
end;

theorem
    for Y,Z st Y is TolSet of T & Z is TolSet of T holds Y /\ Z is TolSet of T
proof let Y,Z such that A1: Y is TolSet of T & Z is TolSet of T;
  let x,y; assume x in Y /\ Z & y in Y /\ Z;
    then x in Y & y in Y by XBOOLE_0:def 3;
  hence [x,y] in T by A1,Def3;
end;

theorem Th43:
  Y is TolSet of T implies Y c= X
proof assume A1: Y is TolSet of T;let x;
  assume x in Y;
  then [x,x] in T by A1,Def3;
 hence x in X by Th27;
end;

canceled;

theorem Th45:
  for Y being TolSet of T ex Z being TolClass of T st Y c= Z
proof let Y be TolSet of T;
   defpred X[set] means $1 is TolSet of T & ex Z st $1=Z & Y c= Z;
    consider TS being set such that A1:
       for x holds x in TS iff x in bool X & X[x] from Separation;
    A2: for x being set holds x in TS iff x in bool X & x is TolSet of T
            & Y c= x
        proof let x be set;
          thus x in TS implies x in bool X & x is TolSet of T & Y c= x
             proof assume A3: x in TS;
               hence x in bool X & x is TolSet of T by A1;
                  ex Z st x=Z & Y c= Z by A1,A3;
               hence Y c= x;
             end;
          thus thesis by A1;
        end;
    A4: TS <> {}
        proof
            Y c= X by Th43;
         hence TS <> {} by A2;
        end;
    A5: TS c= bool X
         proof let x; assume x in TS;
           hence x in bool X by A1;
         end;
       for Z st Z c= TS & Z is c=-linear
       ex Y st Y in TS & for X1 being set st X1 in Z holds X1 c= Y
       proof let Z such that A6: Z c= TS & Z is c=-linear;
       A7: Z = {} implies thesis
         proof assume A8: Z = {};
           consider Y being Element of TS;
           take Y;
           thus Y in TS by A4;
           let X1 be set; assume X1 in Z;
          hence thesis by A8;
         end;
          Z <> {} implies thesis
       proof assume A9: Z <> {};
        take union Z;
            Z c= bool X by A5,A6,XBOOLE_1:1;
          then union Z c= union bool X by ZFMISC_1:95;
          then A10: union Z c= X by ZFMISC_1:99;
                for x,y st x in union Z & y in union Z holds [x,y] in T
                proof let x,y;assume A11: x in union Z & y in union Z;
                  then consider Zx being set such that A12:
                     x in Zx & Zx in Z by TARSKI:def 4;
                  consider Zy being set such that A13:
                     y in Zy & Zy in Z by A11,TARSKI:def 4;
                      reconsider Zx as TolSet of T by A1,A6,A12;
                      reconsider Zy as TolSet of T by A1,A6,A13;
                        Zx, Zy are_c=-comparable by A6,A12,A13,ORDINAL1:def 9;
                  then Zx c= Zy or Zy c= Zx by XBOOLE_0:def 9;
                   hence [x,y] in T by A12,A13,Def3;
                end;
          then A14: union Z is TolSet of T by Def3;
                Y c= union Z
                proof let x such that A15: x in Y;
                    consider y being Element of Z;
                       y in TS by A6,A9,TARSKI:def 3;
                      then Y c= y by A2; hence x in union Z by A9,A15,TARSKI:
def 4;
                end;
         hence union Z in TS by A2,A10,A14;
         let X1 be set;
         assume X1 in Z;
        hence X1 c= union Z by ZFMISC_1:92;
        end;
      hence thesis by A7;
       end;
     then consider Z1 being set such that A16: Z1 in TS & for Z st Z in TS & Z
<>Z1
                                         holds not Z1 c= Z by A4,ORDERS_2:77;
     reconsider Z1 as TolSet of T by A1,A16;
         Z1 is TolClass of T
    proof assume not thesis;
     then consider x such that A17: not x in Z1 & x in X &
          for y st y in Z1 holds [x,y] in T by Def4;
     set Y1 = Z1 \/ {x};
       for y,z st y in Y1 & z in Y1 holds [y,z] in T
       proof let y,z; assume y in Y1 & z in Y1;
          then (y in Z1 or y in {x}) & (z in Z1 or z in {x}) by XBOOLE_0:def 2
;
        then A18: (y in Z1 or y = x) & (z in Z1 or z = x) by TARSKI:def 1;
         assume A19: not [y,z] in T;
             then not [z,y] in T by Th30;
         hence contradiction by A17,A18,A19,Def3,Th27;
       end;
     then A20: Y1 is TolSet of T by Def3;
          Z1 in bool X by A1,A16;
      then {x} c= X & Z1 c= X by A17,ZFMISC_1:37;
      then A21: Y1 c= X by XBOOLE_1:8;
           Y c= Z1 & Z1 c= Y1 by A2,A16,XBOOLE_1:7;
         then Y c= Y1 by XBOOLE_1:1;
     then A22: Y1 in TS by A2,A20,A21;
           Y1 <> Z1
           proof assume A23: Y1 = Z1;
               x in {x} by TARSKI:def 1;
            hence contradiction by A17,A23,XBOOLE_0:def 2;
           end;
         then not Z1 c= Y1 by A16,A22;
       hence contradiction by XBOOLE_1:7;
    end;
    then reconsider Z1 as TolClass of T;
    take Z1;
  thus Y c= Z1 by A2,A16;
end;

theorem Th46:
  for x,y st [x,y] in T ex Z being TolClass of T st x in Z & y in Z
proof let x,y; assume A1: [x,y] in T;
  then A2: x in X & y in X by ZFMISC_1:106;
    for a,b being set st a in {x,y} & b in {x,y} holds [a,b] in T
    proof let a,b be set; assume a in {x,y} & b in {x,y};
       then (a = x or a = y) & (b = x or b = y) by TARSKI:def 2;
      hence thesis by A1,A2,Th27,Th30;
    end;
  then reconsider PS = {x,y} as TolSet of T by Def3;
  consider Z being TolClass of T such that A3: PS c= Z by Th45;
  take Z;
    x in {x,y} by TARSKI:def 2;
 hence x in Z by A3;
    y in {x,y} by TARSKI:def 2;
 hence thesis by A3;
end;

theorem Th47:
  for x st x in X ex Z being TolClass of T st x in Z
proof let x; assume x in X;
  then [x,x] in T by Th27;
  then ex Z being TolClass of T st x in Z & x in Z by Th46;
 hence thesis;
end;

canceled;

theorem
  T c= Total X
proof let x,y; assume [x,y] in T;
  then [x,y] in [:X,X:];
 hence [x,y] in Total X by EQREL_1:def 1;
end;

theorem
  id X c= T
proof let x,y;assume [x,y] in id X;
  then x in X & x = y by RELAT_1:def 10;
 hence [x,y] in T by Th27;
end;

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
A1: for x st x in A() holds P[x,x] and
A2: for x,y st x in A() & y in A() & P[x,y] holds P[y,x]
proof
   defpred X[set] means ex y,z st $1 = [y,z] & P[y,z];
  consider T being set such that A3:
    for x holds x in T iff x in [:A(),A():] & X[x] from Separation;
    for x st x in T holds x in [:A(),A():] by A3;
  then T c= [:A(),A():] by TARSKI:def 3;
  then reconsider T as Relation of A(),A() by RELSET_1:def 1;
A4: dom T = A()
      proof
          for x st x in A() holds x in dom T
          proof let x; assume x in A();
            then [x,x] in [:A(),A():] & P[x,x] by A1,ZFMISC_1:106;
            then [x,x] in T by A3;
          hence x in dom T by RELAT_1:def 4;
          end;
        then A() c= dom T by TARSKI:def 3;
       hence dom T = A() by XBOOLE_0:def 10;
      end;
  A5: field T = A()
      proof
        A6: field T c= A() \/ A() by RELSET_1:19;
          for x st x in A() holds x in field T
          proof let x; assume x in A();
            then [x,x] in [:A(),A():] & P[x,x] by A1,ZFMISC_1:106;
            then [x,x] in T by A3;
            then x in dom T by RELAT_1:def 4;
            then x in dom T \/ rng T by XBOOLE_0:def 2;
           hence x in field T by RELAT_1:def 6;
          end;
        then A() c= field T by TARSKI:def 3;
       hence field T = A() by A6,XBOOLE_0:def 10;
      end;
A7:  T is total by A4,PARTFUN1:def 4;
        T is_reflexive_in field T
        proof
             for x st x in field T holds [x,x] in T
             proof let x; assume x in field T;
               then [x,x] in [:A(),A():] & P[x,x] by A1,A5,ZFMISC_1:106;
              hence [x,x] in T by A3;
             end;
           hence thesis by RELAT_2:def 1;
        end;
   then A8: T is reflexive by RELAT_2:def 9;
        T is_symmetric_in field T
        proof
            for x,y st x in field T & y in field T & [x,y] in T holds [y,x] in
T
            proof let x,y such that A9:
 x in field T & y in field T & [x,y] in T;
                x in A() & y in A() & P[x,y]
                proof
                   thus x in A() & y in A() by A5,A9;
                   consider a,b being set such that A10:
                       [x,y] = [a,b] & P[a,b] by A3,A9;
                     x = a & y = b by A10,ZFMISC_1:33;
                    hence P[x,y] by A10;
                end;
              then [y,x] in [:A(),A():] & P[y,x] by A2,ZFMISC_1:106;
            hence [y,x] in T by A3;
            end;
          hence thesis by RELAT_2:def 3;
        end;
   then reconsider T as Tolerance of A() by A7,A8,RELAT_2:def 11;
   take T;
   let x,y;
   assume A11: x in A() & y in A();
    thus [x,y] in T implies P[x,y]
     proof assume [x,y] in T;
       then consider a,b being set such that A12: [x,y] = [a,b] & P[a,b] by A3;
          x = a & y = b by A12,ZFMISC_1:33;
       hence P[x,y] by A12;
     end;
    assume A13: P[x,y];
      [x,y] in [:A(),A():] by A11,ZFMISC_1:106;
   hence [x,y] in T by A3,A13;
end;

theorem
    for Y ex T being Tolerance of union Y st
    for Z st Z in Y holds Z is TolSet of T
proof let Y;
   defpred X[set,set] means ex Z st Z in Y & $1 in Z & $2 in Z;
  A1: for x st x in union Y holds X[x,x]
     proof let x; assume x in union Y;
        then ex Z st x in Z & Z in Y by TARSKI:def 4;
       hence thesis;
     end;
  A2: for x,y st x in union Y & y in union Y & X[x,y] holds X[y,x];
  consider T being Tolerance of union Y such that A3:
   for x,y st x in union Y & y in union Y holds
     [x,y] in T iff X[x,y]  from ToleranceEx(A1,A2);
  take T;
  let Z such that A4: Z in Y;
    for x,y st x in Z & y in Z holds [x,y] in T
   proof let x,y; assume A5: x in Z & y in Z;
     then x in union Y & y in union Y by A4,TARSKI:def 4;
    hence [x,y] in T by A3,A4,A5;
   end;
 hence Z is TolSet of T by Def3;
end;

theorem
    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
proof let Y be set;let T,R be Tolerance of union Y such that A1:
    (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);
    for x,y holds [x,y] in T iff [x,y] in R
    proof let x,y;
      thus [x,y] in T implies [x,y] in R
        proof assume [x,y] in T;
          then ex Z st Z in Y & x in Z & y in Z by A1;
         hence [x,y] in R by A1;
        end;
      assume [x,y] in R;
        then ex Z st Z in Y & x in Z & y in Z by A1;
       hence [x,y] in T by A1;
    end;
  hence T = R by RELAT_1:def 2;
end;

theorem Th53:
  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
proof let T,R be Tolerance of X;
  assume A1: for Z holds Z is TolClass of T iff Z is TolClass of R;
    for x,y holds [x,y] in T iff [x,y] in R
    proof let x,y;
      thus [x,y] in T implies [x,y] in R
        proof assume [x,y] in T;
         then consider Z being TolClass of T such that
A2: x in Z & y in Z by Th46;
         reconsider Z as TolClass of R by A1;
         Z is TolSet of R;
         hence [x,y] in R by A2,Def3;
        end;
     assume [x,y] in R;
     then consider Z being TolClass of R such that A3: x in Z & y in Z by Th46;
     reconsider Z as TolClass of T by A1;
       Z is TolSet of T;
    hence [x,y] in T by A3,Def3;
    end;
  hence T = R by RELAT_1:def 2;
end;

:: 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 Th54:
  for y being set holds y in neighbourhood(x,T) iff [x,y] in T
  proof
    let y be set;
    hereby assume y in neighbourhood(x,T); then
      [y,x] in T by EQREL_1:27;
      hence [x,y] in T by EQREL_1:12;
    end;
    assume [x,y] in T; then
    [y,x] in T by EQREL_1:12;
    hence thesis by EQREL_1:27;
  end;

Th56:
  x in X implies x in neighbourhood(x,T) by EQREL_1:28;

canceled 3;

theorem
  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
proof let Y such that A1: for Z being set holds
                          Z in Y iff x in Z & Z is TolClass of T;
    for y holds y in neighbourhood(x,T) iff y in union Y
    proof let y;
      thus y in neighbourhood(x,T) implies y in union Y
       proof assume y in neighbourhood(x,T);
         then [x,y] in T by Th54;
         then consider Z being TolClass of T such that
A2: x in Z & y in Z by Th46;
        Z in Y by A1,A2;
        hence y in union Y by A2,TARSKI:def 4;
       end;
       assume y in union Y;
       then consider Z such that A3: y in Z & Z in Y by TARSKI:def 4;
       reconsider Z as TolClass of T by A1,A3;
         x in Z by A1,A3;
       then [x,y] in T by A3,Def3;
      hence y in neighbourhood(x,T) by Th54;
    end;
  hence thesis by TARSKI:2;
end;

theorem
    for Y st for Z holds Z in Y iff x in Z & Z is TolSet of T holds
    neighbourhood(x,T) = union Y
proof let Y such that A1: for Z holds Z in Y iff x in Z & Z is TolSet of T;
    for y holds y in neighbourhood(x,T) iff y in union Y
    proof let y;
      thus y in neighbourhood(x,T) implies y in union Y
       proof assume y in neighbourhood(x,T);
         then [x,y] in T by Th54;
         then consider Z being TolClass of T such that
A2: x in Z & y in Z by Th46;
           Z in Y by A1,A2;
        hence y in union Y by A2,TARSKI:def 4;
       end;
       assume y in union Y;
       then consider Z such that A3: y in Z & Z in Y by TARSKI:def 4;
       reconsider Z as TolSet of T by A1,A3;
       x in Z by A1,A3;
      then [x,y] in T by A3,Def3;
      hence y in neighbourhood(x,T) by Th54;
    end;
  hence thesis by TARSKI:2;
end;

:::::::::::::::::::::::::::::::::::::::::::::
:: Family of sets and classes of proximity ::
:::::::::::::::::::::::::::::::::::::::::::::
definition let X; let T be Tolerance of X;
  func TolSets T -> set means
:Def6: for Y holds Y in it iff Y is TolSet of T;
  existence
    proof
   defpred X[set] means $1 is TolSet of T;
      consider Z being set such that A1:
        x in Z iff x in bool X & X[x] from Separation;
      take Z;
      let Y;
      thus Y in Z implies Y is TolSet of T by A1;
      assume A2: Y is TolSet of T;
        for x holds x in Y implies x in X
        proof let x;assume x in Y;
          then [x,x] in T by A2,Def3;
         hence x in X by ZFMISC_1:106;
        end;
      then Y c= X by TARSKI:def 3;
    hence Y in Z by A1,A2;
    end;
  uniqueness
    proof
      defpred P[set] means $1 is TolSet of T;
      let Z1,Z2 be set such that
      A3: for Y holds Y in Z1 iff P[Y] and
      A4: for Y holds Y in Z2 iff P[Y];
      Z1 = Z2 from Extensionality (A3, A4);
      hence thesis;
    end;

  func TolClasses T -> set means
:Def7: for Y holds Y in it iff Y is TolClass of T;
   existence
    proof
   defpred X[set] means $1 is TolClass of T;
      consider Z being set such that A5:
        x in Z iff x in bool X & X[x] from Separation;
      take Z;
      let Y;
      thus Y in Z implies Y is TolClass of T by A5;
      assume A6: Y is TolClass of T;
        for x holds x in Y implies x in X
        proof let x;assume x in Y;
          then [x,x] in T by A6,Def3;
         hence x in X by ZFMISC_1:106;
        end;
      then Y c= X by TARSKI:def 3;
     hence Y in Z by A5,A6;
   end;
   uniqueness
     proof
      defpred P[set] means $1 is TolClass of T;
      let C1,C2 be set such that
      A7: for Y holds Y in C1 iff P[Y] and
      A8: for Y holds Y in C2 iff P[Y];
      C1 = C2 from Extensionality (A7, A8);
      hence thesis;
     end;
end;

canceled 4;

theorem
    TolClasses R c= TolClasses T implies R c= T
proof assume A1: TolClasses R c= TolClasses T;
  let x,y; assume [x,y] in R;
  then consider Z being TolClass of R such that A2: x in Z & y in Z by Th46;
    Z in TolClasses R by Def7;
  then Z is TolSet of T by A1,Def7;
 hence [x,y] in T by A2,Def3;
end;

theorem
     for T,R being Tolerance of X st TolClasses T = TolClasses R
     holds T = R
proof let T,R be Tolerance of X;
  assume A1: TolClasses T = TolClasses R;
    for Z holds Z is TolClass of T iff Z is TolClass of R
    proof let Z;
        Z is TolClass of T iff Z in TolClasses R by A1,Def7;
     hence thesis by Def7;
    end;
  hence thesis by Th53;
end;

theorem
    union TolClasses T = X
proof
    for x holds x in union TolClasses T iff x in X
    proof let x;
      thus x in union TolClasses T implies x in X
        proof assume x in union TolClasses T;
          then consider Z such that A1: x in Z & Z in TolClasses T by TARSKI:
def 4;
            Z is TolSet of T by A1,Def7;
          then Z c= X by Th43;
         hence x in X by A1;
        end;
      assume x in X;
      then consider Z being TolClass of T such that A2: x in Z by Th47;
        Z in TolClasses T by Def7;
    hence x in union TolClasses T by A2,TARSKI:def 4;
    end;
  hence thesis by TARSKI:2;
end;

theorem
    union TolSets T = X
proof
    for x holds x in union TolSets T iff x in X
   proof let x;
      thus x in union TolSets T implies x in X
         proof assume x in union TolSets T;
           then consider Z such that A1: x in Z & Z in TolSets T by TARSKI:def
4;
             Z is TolSet of T by A1,Def6;
           then Z c= X by Th43;
          hence x in X by A1;
         end;
      assume x in X;
      then consider Z being TolClass of T such that A2: x in Z by Th47;
        Z in TolSets T by Def6;
    hence x in union TolSets T by A2,TARSKI:def 4;
   end;
 hence thesis by TARSKI:2;
end;

theorem
    (for x st x in X holds neighbourhood(x,T) is TolSet of T)
   implies T is transitive
proof
A1:     field T = X by ORDERS_1:97;
  assume A2: for x st x in X holds neighbourhood(x,T) is TolSet of T;
    for x,y,z st x in field T & y in field T & z in field T &
    [x,y] in T & [y,z] in T holds [x,z] in T
  proof let x,y,z; assume A3: x in field T & y in field T & z in field T &
                                   [x,y] in T & [y,z] in T;
    then reconsider N = neighbourhood(y,T) as TolSet of T by A1,A2;
    A4: z in N by A3,Th54;
          [y,x] in T by A3,Th30;
        then x in N by Th54;
     hence [x,z] in T by A4,Def3;
  end;
  then T is_transitive_in field T by RELAT_2:def 8;
 hence T is transitive by RELAT_2:def 16;
end;

theorem
    T is transitive implies
  (for x st x in X holds neighbourhood(x,T) is TolClass of T)
proof
A1:     field T = X by ORDERS_1:97;
 assume T is transitive;
  then A2: T is_transitive_in X by A1,RELAT_2:def 16;
  let x;
  assume A3: x in X;
  set N = neighbourhood(x,T);
    for y,z st y in N & z in N holds [y,z] in T
    proof let y,z such that A4: y in N & z in N;
      A6: [x,z] in T by A4,Th54;
       [x,y] in T by A4,Th54;
       then [y,x] in T by Th30;
     hence [y,z] in T by A2,A3,A4,A6,RELAT_2:def 8;
    end;
  then reconsider Z = N as TolSet of T by Def3;
    for x st not x in Z & x in X ex y st y in Z & not [x,y] in T
    proof let y such that A7: not y in Z & y in X;
      assume A8: for z st z in Z holds [y,z] in T;
        x in Z by A3,Th56;
      then [y,x] in T by A8;
      then [x,y] in T by Th30;
     hence contradiction by A7,Th54;
    end;
 hence thesis by Def4;
end;

theorem
    for x for Y being TolClass of T st x in Y holds
     Y c= neighbourhood(x,T)
proof let x;let Y be TolClass of T such that A1: x in Y;
    for y st y in Y holds y in neighbourhood(x,T)
    proof let y; assume y in Y;
      then [x,y] in T by A1,Def3;
     hence thesis by Th54;
    end;
  hence thesis by TARSKI:def 3;
end;

theorem
    TolSets R c= TolSets T iff R c= T
proof
  thus TolSets R c= TolSets T implies R c= T
    proof assume A1: TolSets R c= TolSets T;
      let x,y; assume [x,y] in R;
      then consider Z being TolClass of R such that A2: x in Z & y in Z by Th46
;
        Z in TolSets R by Def6;
      then Z is TolSet of T by A1,Def6;
     hence [x,y] in T by A2,Def3;
    end;
  assume A3: R c= T;
   let x; assume x in TolSets R;
   then reconsider Z = x as TolSet of R by Def6;
     for x,y st x in Z & y in Z holds [x,y] in T
     proof let x,y;assume x in Z & y in Z;
       then [x,y] in R by Def3;
      hence [x,y] in T by A3;
     end;
   then Z is TolSet of T by Def3;
  hence x in TolSets T by Def6;
end;

theorem
    TolClasses T c= TolSets T
proof let x; assume x in TolClasses T;
   then x is TolSet of T by Def7;
  hence thesis by Def6;
end;

theorem
    (for x st x in X holds neighbourhood(x,R) c= neighbourhood(x,T))
    implies R c= T
proof
  assume A1: for x st x in X holds neighbourhood(x,R) c= neighbourhood(x,T);
  let x,y; assume A2: [x,y] in R;
  then A3: y in neighbourhood(x,R) by Th54;
    x in X by A2,ZFMISC_1:106;
  then neighbourhood(x,R) c= neighbourhood(x,T) by A1; hence [x,y] in T by A3,
Th54;
end;

theorem
    T c= T*T
proof let x,y; assume A1: [x,y] in T;
  then y in X by ZFMISC_1:106;
  then [y,y] in T by Th27;
 hence [x,y] in T*T by A1,RELAT_1:def 8;
end;

Back to top