Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### 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;

Back to top