:: Relations of Tolerance
:: by Krzysztof Hryniewiecki
::
:: Received September 20, 1990
:: Copyright (c) 1990-2017 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;