:: Relations of Tolerance :: by Krzysztof Hryniewiecki :: :: Received September 20, 1990 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, RELAT_2, RELAT_1, EQREL_1, WELLORD1, ZFMISC_1, PARTFUN1, SUBSET_1, TARSKI, ORDINAL1, TOLER_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, RELAT_2, PARTFUN1, ORDINAL1, WELLORD1, EQREL_1; constructors ORDINAL1, WELLORD1, EQREL_1, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELAT_1, PARTFUN1, EQREL_1, RELSET_1; requirements SUBSET, BOOLE; begin reserve X,Y,Z,x,y,z for set; registration cluster empty -> reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive for Relation; end; :: Total relation notation let X; synonym Total X for nabla X; end; definition let R be Relation, Y be set; redefine func R |_2 Y -> Relation of Y,Y; end; theorem :: TOLER_1:1 rng Total X = X; theorem :: TOLER_1:2 for x,y st x in X & y in X holds [x,y] in Total X; theorem :: TOLER_1:3 for x,y st x in field Total X & y in field Total X holds [x,y] in Total X; theorem :: TOLER_1:4 Total X is strongly_connected; theorem :: TOLER_1:5 Total X is connected; :: Tolerance reserve T,R for Tolerance of X; theorem :: TOLER_1:6 for T being Tolerance of X holds rng T = X; theorem :: TOLER_1:7 for x being object holds for T being total reflexive Relation of X holds x in X iff [x,x] in T; theorem :: TOLER_1:8 for T being Tolerance of X holds T is_reflexive_in X; theorem :: TOLER_1:9 for T being Tolerance of X holds T is_symmetric_in X; theorem :: TOLER_1:10 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; redefine func T |_2 Y -> Tolerance of Y; end; theorem :: TOLER_1:11 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 1 for x,y st x in it & y in it holds [x,y ] in T; end; theorem :: TOLER_1:12 {} 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 2 for x st not x in IT & x in X ex y st y in IT & not [x,y] in T; end; registration let X; let T be Tolerance of X; cluster TolClass-like for TolSet of T; end; definition let X; let T be Tolerance of X; mode TolClass of T is TolClass-like TolSet of T; end; theorem :: TOLER_1:13 for T being Tolerance of X st {} is TolClass of T holds T={}; theorem :: TOLER_1:14 {} is Tolerance of {}; theorem :: TOLER_1:15 for x,y st [x,y] in T holds {x,y} is TolSet of T; theorem :: TOLER_1:16 for x st x in X holds {x} is TolSet of T; theorem :: TOLER_1:17 for Y,Z st Y is TolSet of T holds Y /\ Z is TolSet of T; theorem :: TOLER_1:18 Y is TolSet of T implies Y c= X; theorem :: TOLER_1:19 for Y being TolSet of T ex Z being TolClass of T st Y c= Z; theorem :: TOLER_1:20 for x,y being object st [x,y] in T ex Z being TolClass of T st x in Z & y in Z; theorem :: TOLER_1:21 for x st x in X ex Z being TolClass of T st x in Z; theorem :: TOLER_1:22 T c= Total X; theorem :: TOLER_1:23 id X c= T; scheme :: TOLER_1:sch 1 ToleranceEx{A() -> set,P[object,object]}: 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:24 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:25 for Y being set for T,R being Tolerance of union Y st (for x,y being object holds [x,y] in T iff ex Z st Z in Y & x in Z & y in Z) & (for x,y being object holds [x,y] in R iff ex Z st Z in Y & x in Z & y in Z) holds T = R; theorem :: TOLER_1:26 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 notation let X, Y; let T be Relation of X, Y; let x be object; synonym neighbourhood (x, T) for Class (T,x); end; theorem :: TOLER_1:27 for x,y being object holds y in neighbourhood(x,T) iff [x,y] in T; theorem :: TOLER_1:28 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:29 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 3 for Y holds Y in it iff Y is TolSet of T; func TolClasses T -> set means :: TOLER_1:def 4 for Y holds Y in it iff Y is TolClass of T; end; theorem :: TOLER_1:30 TolClasses R c= TolClasses T implies R c= T; theorem :: TOLER_1:31 for T,R being Tolerance of X st TolClasses T = TolClasses R holds T = R; theorem :: TOLER_1:32 union TolClasses T = X; theorem :: TOLER_1:33 union TolSets T = X; theorem :: TOLER_1:34 (for x st x in X holds neighbourhood(x,T) is TolSet of T) implies T is transitive; theorem :: TOLER_1:35 T is transitive implies for x st x in X holds neighbourhood(x,T) is TolClass of T; theorem :: TOLER_1:36 for x for Y being TolClass of T st x in Y holds Y c= neighbourhood(x,T ); theorem :: TOLER_1:37 TolSets R c= TolSets T iff R c= T; theorem :: TOLER_1:38 TolClasses T c= TolSets T; theorem :: TOLER_1:39 (for x st x in X holds neighbourhood(x,R) c= neighbourhood(x,T)) implies R c= T; theorem :: TOLER_1:40 T c= T*T;