:: 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;
definitions TARSKI, RELAT_1, RELAT_2;
equalities RELAT_1, WELLORD1;
expansions TARSKI, RELAT_1, RELAT_2;
theorems TARSKI, RELAT_1, RELSET_1, RELAT_2, ZFMISC_1, WELLORD1, ENUMSET1,
ORDERS_1, EQREL_1, ORDINAL1, XBOOLE_0, XBOOLE_1, PARTFUN1, XTUPLE_0;
schemes XBOOLE_0, XFAMILY;
begin
reserve X,Y,Z,x,y,z for set;
registration
cluster empty -> reflexive irreflexive symmetric antisymmetric asymmetric
connected strongly_connected transitive for Relation;
coherence
proof
let R be Relation such that
A1: R is empty;
{} is_reflexive_in field {};
hence R is reflexive by A1;
{} is_irreflexive_in field {};
hence R is irreflexive by A1;
thus R is symmetric
proof
let x,y be object;
assume that
x in field R and
y in field R and
A2: [x,y] in R;
thus thesis by A1,A2;
end;
{} is_antisymmetric_in field {};
hence R is antisymmetric by A1;
{} is_asymmetric_in field {};
hence R is asymmetric by A1;
{} is_connected_in field {};
hence R is connected by A1;
{} is_strongly_connected_in field {};
hence R is strongly_connected by A1;
{} is_transitive_in field {};
hence R is transitive by A1;
end;
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;
coherence by XBOOLE_1:17;
end;
theorem
rng Total X = X
proof
for x being object holds x in X iff ex y being object st [y,x] in Total X
proof
let x be object;
thus x in X implies ex y being object st [y,x] in Total X
proof
assume
A1: x in X;
take x;
[x,x] in [:X,X:] by A1,ZFMISC_1:87;
hence thesis by EQREL_1:def 1;
end;
thus thesis by ZFMISC_1:87;
end;
hence thesis by XTUPLE_0:def 13;
end;
theorem Th2:
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:87;
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:12;
hence thesis by Th2;
end;
theorem
Total X is strongly_connected
proof
let x,y be object;
assume x in field Total X & y in field Total X;
then x in X & y in X by ORDERS_1:12;
then [x,y] in [:X,X:] by ZFMISC_1:87;
hence thesis by EQREL_1:def 1;
end;
theorem
Total X is connected
proof
let x,y be object;
assume that
A1: x in field Total X & y in field Total X and
x<>y;
x in X & y in X by A1,ORDERS_1:12;
then [x,y] in [:X,X:] by ZFMISC_1:87;
hence thesis by EQREL_1:def 1;
end;
:: Tolerance
reserve T,R for Tolerance of X;
theorem
for T being Tolerance of X holds rng T = X
proof
let T be Tolerance of X;
for x being object holds x in rng T iff x in X
proof
let x be object;
x in X implies x in rng T
proof
field T = X by ORDERS_1:12;
then
A1: T is_reflexive_in X by RELAT_2:def 9;
assume x in X;
then [x,x] in T by A1;
hence thesis by XTUPLE_0:def 13;
end;
hence thesis;
end;
hence thesis by TARSKI:2;
end;
theorem Th7:
for x being object holds
for T being total reflexive Relation of X holds x in X iff [x,x] in T
proof let x be object;
let T be total reflexive Relation of X;
thus x in X implies [x,x] in T by EQREL_1:5;
assume
A1: [x,x] in T;
field T = X by ORDERS_1:12;
hence thesis by A1,RELAT_1:15;
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:12;
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:12;
hence thesis by RELAT_2:def 11;
end;
theorem Th10:
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;
now
let x,y be object;
assume that
A2: x in field(R|_2 Z) & y in field(R|_2 Z) and
A3: [x,y] in R|_2 Z;
A4: [x,y] in R by A3,XBOOLE_0:def 4;
A5: [y,x] in [:Z,Z:] by A3,ZFMISC_1:88;
x in field R & y in field R by A2,WELLORD1:12;
then [y,x] in R by A1,A4;
hence [y,x] in R|_2 Z by A5,XBOOLE_0:def 4;
end;
then R|_2 Z is_symmetric_in field(R|_2 Z);
hence thesis;
end;
definition
let X,T;
let Y be Subset of X;
redefine func T |_2 Y -> Tolerance of Y;
coherence
proof
now
let x be object;
assume x in Y;
then [x,x] in [:Y,Y:] & [x,x] in T by Th7,ZFMISC_1:87;
then [x,x] in T |_2 Y by XBOOLE_0:def 4;
hence x in dom (T |_2 Y) by XTUPLE_0:def 12;
end;
then Y c= dom(T |_2 Y);
then dom(T |_2 Y) = Y by XBOOLE_0:def 10;
hence T |_2 Y is Tolerance of Y by Th10,PARTFUN1:def 2,WELLORD1:15;
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
:Def1:
for x,y st x in it & y in it holds [x,y ] in T;
existence
proof
take {};
let x,y;
assume that
A1: x in {} and
y in {};
thus thesis by A1;
end;
end;
theorem Th12:
{} is TolSet of T
proof
let x,y;
assume that
A1: x in {} and
y in {};
thus thesis by A1;
end;
definition
let X;
let T be Tolerance of X;
let IT be TolSet of T;
attr IT is TolClass-like means
:Def2:
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;
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 XFAMILY:sch 1;
A2: TS c= bool X
by A1;
A3: 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 and
A5: Z is c=-linear;
for x,y st x in union Z & y in union Z holds [x,y] in T
proof
let x,y;
assume that
A6: x in union Z and
A7: y in union Z;
consider Zy being set such that
A8: y in Zy and
A9: Zy in Z by A7,TARSKI:def 4;
reconsider Zy as TolSet of T by A1,A4,A9;
consider Zx being set such that
A10: x in Zx and
A11: Zx in Z by A6,TARSKI:def 4;
reconsider Zx as TolSet of T by A1,A4,A11;
Zx,Zy are_c=-comparable by A5,A11,A9,ORDINAL1:def 8;
then Zx c= Zy or Zy c= Zx by XBOOLE_0:def 9;
hence thesis by A10,A8,Def1;
end;
then
A12: union Z is TolSet of T by Def1;
take union Z;
Z c= bool X by A2,A4;
then union Z c= union bool X by ZFMISC_1:77;
then union Z c= X by ZFMISC_1:81;
hence union Z in TS by A1,A12;
let X1 be set;
assume X1 in Z;
hence thesis by ZFMISC_1:74;
end;
{} c= X & {} is TolSet of T by Th12;
then TS <> {} by A1;
then consider Y such that
A13: Y in TS and
A14: for Z st Z in TS & Z <> Y holds not Y c= Z by A3,ORDERS_1:65;
reconsider Y as TolSet of T by A1,A13;
take Y;
let x such that
A15: not x in Y and
A16: x in X;
set Y1 = Y \/ {x};
A17: {x} c= X by A16,ZFMISC_1:31;
assume
A18: for y st y in Y holds [x,y] in T;
for y,z st y in Y1 & z in Y1 holds [y,z] in T
proof
let y,z;
assume that
A19: y in Y1 and
A20: z in Y1;
y in Y or y in {x} by A19,XBOOLE_0:def 3;
then
A21: y in Y or y = x by TARSKI:def 1;
z in Y or z in {x} by A20,XBOOLE_0:def 3;
then
A22: z in Y or z = x by TARSKI:def 1;
assume
A23: not [y,z] in T;
then not [z,y] in T by EQREL_1:6;
hence contradiction by A16,A18,A21,A22,A23,Def1,Th7;
end;
then
A24: Y1 is TolSet of T by Def1;
A25: Y1 <> Y
proof
A26: x in {x} by TARSKI:def 1;
assume Y1 = Y;
hence contradiction by A15,A26,XBOOLE_0:def 3;
end;
Y in bool X by A1,A13;
then Y1 c= X by A17,XBOOLE_1:8;
then Y1 in TS by A1,A24;
hence contradiction by A14,A25,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;
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 being object such that
A1: [x,y] in T;
x in X by A1,ZFMISC_1:87;
then ex z st z in 00 & not [x,z] in T by Def2;
hence contradiction;
end;
theorem
{} is Tolerance of {} by RELSET_1:12;
theorem Th15:
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:87;
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 that
A3: a in {x,y} and
A4: b in {x,y};
A5: b = x or b = y by A4,TARSKI:def 2;
a = x or a = y by A3,TARSKI:def 2;
hence thesis by A1,A2,A5,Th7,EQREL_1:6;
end;
hence thesis by Def1;
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 Th7;
then {x,x} is TolSet of T by Th15;
hence thesis by ENUMSET1:29;
end;
theorem
for Y,Z st Y is TolSet of T holds Y /\ Z is TolSet of T
proof
let Y,Z such that
A1: Y 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 4;
hence thesis by A1,Def1;
end;
theorem Th18:
Y is TolSet of T implies Y c= X
proof
assume
A1: Y is TolSet of T;
let x be object;
assume x in Y;
then [x,x] in T by A1,Def1;
hence thesis by Th7;
end;
theorem Th19:
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 XFAMILY:sch 1;
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 thesis;
end;
thus thesis by A1;
end;
Y c= X by Th18;
then
A4: TS <> {} by A2;
A5: TS c= bool X
by A1;
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 and
A7: Z is c=-linear;
A8: for x,y st x in union Z & y in union Z holds [x,y] in T
proof
let x,y;
assume that
A9: x in union Z and
A10: y in union Z;
consider Zy being set such that
A11: y in Zy and
A12: Zy in Z by A10,TARSKI:def 4;
reconsider Zy as TolSet of T by A1,A6,A12;
consider Zx being set such that
A13: x in Zx and
A14: Zx in Z by A9,TARSKI:def 4;
reconsider Zx as TolSet of T by A1,A6,A14;
Zx, Zy are_c=-comparable by A7,A14,A12,ORDINAL1:def 8;
then Zx c= Zy or Zy c= Zx by XBOOLE_0:def 9;
hence thesis by A13,A11,Def1;
end;
A15: Z <> {} implies thesis
proof
assume
A16: Z <> {};
A17: Y c= union Z
proof
set y = the Element of Z;
y in TS by A6,A16;
then
A18: Y c= y by A2;
let x be object;
assume x in Y;
hence thesis by A16,A18,TARSKI:def 4;
end;
Z c= bool X by A5,A6;
then union Z c= union bool X by ZFMISC_1:77;
then
A19: union Z c= X by ZFMISC_1:81;
take union Z;
union Z is TolSet of T by A8,Def1;
hence union Z in TS by A2,A19,A17;
let X1 be set;
assume X1 in Z;
hence thesis by ZFMISC_1:74;
end;
Z = {} implies thesis
proof
set Y = the Element of TS;
assume
A20: Z = {};
take Y;
thus Y in TS by A4;
let X1 be set;
assume X1 in Z;
hence thesis by A20;
end;
hence thesis by A15;
end;
then consider Z1 being set such that
A21: Z1 in TS and
A22: for Z st Z in TS & Z<>Z1 holds not Z1 c= Z by A4,ORDERS_1:65;
reconsider Z1 as TolSet of T by A1,A21;
Z1 is TolClass of T
proof
assume not thesis;
then consider x such that
A23: not x in Z1 and
A24: x in X and
A25: for y st y in Z1 holds [x,y] in T by Def2;
set Y1 = Z1 \/ {x};
A26: {x} c= X by A24,ZFMISC_1:31;
for y,z st y in Y1 & z in Y1 holds [y,z] in T
proof
let y,z;
assume that
A27: y in Y1 and
A28: z in Y1;
y in Z1 or y in {x} by A27,XBOOLE_0:def 3;
then
A29: y in Z1 or y = x by TARSKI:def 1;
z in Z1 or z in {x} by A28,XBOOLE_0:def 3;
then
A30: z in Z1 or z = x by TARSKI:def 1;
assume
A31: not [y,z] in T;
then not [z,y] in T by EQREL_1:6;
hence contradiction by A24,A25,A29,A30,A31,Def1,Th7;
end;
then
A32: Y1 is TolSet of T by Def1;
Y c= Z1 & Z1 c= Y1 by A2,A21,XBOOLE_1:7;
then
A33: Y c= Y1;
A34: Y1 <> Z1
proof
A35: x in {x} by TARSKI:def 1;
assume Y1 = Z1;
hence contradiction by A23,A35,XBOOLE_0:def 3;
end;
Z1 in bool X by A1,A21;
then Y1 c= X by A26,XBOOLE_1:8;
then Y1 in TS by A2,A32,A33;
hence contradiction by A22,A34,XBOOLE_1:7;
end;
then reconsider Z1 as TolClass of T;
take Z1;
thus thesis by A2,A21;
end;
theorem Th20:
for x,y being object st [x,y] in T
ex Z being TolClass of T st x in Z & y in Z
proof
let x,y be object;
assume
A1: [x,y] in T;
then
A2: x in X & y in X by ZFMISC_1:87;
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 that
A3: a in {x,y} and
A4: b in {x,y};
A5: b = x or b = y by A4,TARSKI:def 2;
a = x or a = y by A3,TARSKI:def 2;
hence thesis by A1,A2,A5,Th7,EQREL_1:6;
end;
then reconsider PS = {x,y} as TolSet of T by Def1;
consider Z being TolClass of T such that
A6: PS c= Z by Th19;
take Z;
x in {x,y} by TARSKI:def 2;
hence x in Z by A6;
y in {x,y} by TARSKI:def 2;
hence thesis by A6;
end;
theorem Th21:
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 Th7;
then ex Z being TolClass of T st x in Z & x in Z by Th20;
hence thesis;
end;
theorem
T c= Total X
proof
let x,y be object;
assume [x,y] in T;
then [x,y] in [:X,X:];
hence thesis by EQREL_1:def 1;
end;
theorem
id X c= T
proof
let x,y be object;
assume [x,y] in id X;
then x in X & x = y by RELAT_1:def 10;
hence thesis by Th7;
end;
scheme
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
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[object] means ex y,z being object st $1 = [y,z] & P[y,z];
consider T being set such that
A3: for x being object holds x in T iff x in [:A(),A():] & X[x]
from XBOOLE_0:sch 1;
for x being object st x in T holds x in [:A(),A():] by A3;
then reconsider T as Relation of A(),A() by TARSKI:def 3;
A4: field T c= A() \/ A() by RELSET_1:8;
for x being object st x in field T holds [x,x] in T
proof
let x be object;
assume x in field T;
then [x,x] in [:A(),A():] & P[x,x] by A1,A4,ZFMISC_1:87;
hence thesis by A3;
end;
then
A5: T is_reflexive_in field T;
for x,y being object st x in field T & y in field T & [x,y] in T
holds [y,x] in T
proof
let x,y being object such that
A6: x in field T & y in field T and
A7: [x,y] in T;
x in A() & y in A() & P[x,y]
proof
thus x in A() & y in A() by A4,A6;
consider a,b being object such that
A8: [x,y] = [a,b] and
A9: P[a,b] by A3,A7;
x = a by A8,XTUPLE_0:1;
hence thesis by A8,A9,XTUPLE_0:1;
end;
then [y,x] in [:A(),A():] & P[y,x] by A2,ZFMISC_1:87;
hence thesis by A3;
end;
then
A10: T is_symmetric_in field T;
for x being object st x in A() holds x in dom T
proof
let x be object;
assume x in A();
then [x,x] in [:A(),A():] & P[x,x] by A1,ZFMISC_1:87;
then [x,x] in T by A3;
hence thesis by XTUPLE_0:def 12;
end;
then A() c= dom T;
then dom T = A() by XBOOLE_0:def 10;
then reconsider T as Tolerance of A() by A5,A10,PARTFUN1:def 2,RELAT_2:def 9
,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 object such that
A12: [x,y] = [a,b] and
A13: P[a,b] by A3;
x = a by A12,XTUPLE_0:1;
hence thesis by A12,A13,XTUPLE_0:1;
end;
assume
A14: P[x,y];
[x,y] in [:A(),A():] by A11,ZFMISC_1:87;
hence thesis by A3,A14;
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 thesis by A3,A4,A5;
end;
hence thesis by Def1;
end;
theorem
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
proof
let Y be set;
let T,R be Tolerance of union Y such that
A1: for x,y being object holds [x,y] in T iff
ex Z st Z in Y & x in Z & y in Z and
A2: for x,y being object holds [x,y] in R iff
ex Z st Z in Y & x in Z & y in Z;
for x,y being object holds [x,y] in T iff [x,y] in R
proof
let x,y be object;
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 thesis by A2;
end;
assume [x,y] in R;
then ex Z st Z in Y & x in Z & y in Z by A2;
hence thesis by A1;
end;
hence thesis;
end;
theorem Th26:
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 being object holds [x,y] in T iff [x,y] in R
proof
let x,y be object;
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 Th20;
reconsider Z as TolClass of R by A1;
Z is TolSet of R;
hence thesis by A2,Def1;
end;
assume [x,y] in R;
then consider Z being TolClass of R such that
A3: x in Z & y in Z by Th20;
reconsider Z as TolClass of T by A1;
Z is TolSet of T;
hence thesis by A3,Def1;
end;
hence thesis;
end;
:: 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 Th27:
for x,y being object holds y in neighbourhood(x,T) iff [x,y] in T
proof
let x,y be object;
hereby
assume y in neighbourhood(x,T);
then [y,x] in T by EQREL_1:19;
hence [x,y] in T by EQREL_1:6;
end;
assume [x,y] in T;
then [y,x] in T by EQREL_1:6;
hence thesis by EQREL_1:19;
end;
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 being object holds y in neighbourhood(x,T) iff y in union Y
proof
let y be object;
thus y in neighbourhood(x,T) implies y in union Y
proof
assume y in neighbourhood(x,T);
then [x,y] in T by Th27;
then consider Z being TolClass of T such that
A2: x in Z and
A3: y in Z by Th20;
Z in Y by A1,A2;
hence thesis by A3,TARSKI:def 4;
end;
assume y in union Y;
then consider Z such that
A4: y in Z and
A5: Z in Y by TARSKI:def 4;
reconsider Z as TolClass of T by A1,A5;
x in Z by A1,A5;
then [x,y] in T by A4,Def1;
hence thesis by Th27;
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 being object holds y in neighbourhood(x,T) iff y in union Y
proof
let y be object;
thus y in neighbourhood(x,T) implies y in union Y
proof
assume y in neighbourhood(x,T);
then [x,y] in T by Th27;
then consider Z being TolClass of T such that
A2: x in Z and
A3: y in Z by Th20;
Z in Y by A1,A2;
hence thesis by A3,TARSKI:def 4;
end;
assume y in union Y;
then consider Z such that
A4: y in Z and
A5: Z in Y by TARSKI:def 4;
reconsider Z as TolSet of T by A1,A5;
x in Z by A1,A5;
then [x,y] in T by A4,Def1;
hence thesis by Th27;
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
:Def3:
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 XFAMILY:sch 1;
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 being object holds x in Y implies x in X
proof
let x be object;
assume x in Y;
then [x,x] in T by A2,Def1;
hence thesis by ZFMISC_1:87;
end;
then Y c= X;
hence thesis 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 XFAMILY:sch 2 (A3, A4);
hence thesis;
end;
func TolClasses T -> set means
:Def4:
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 XFAMILY:sch 1;
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 being object holds x in Y implies x in X
proof
let x be object;
assume x in Y;
then [x,x] in T by A6,Def1;
hence thesis by ZFMISC_1:87;
end;
then Y c= X;
hence thesis 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 XFAMILY:sch 2 (A7, A8);
hence thesis;
end;
end;
theorem
TolClasses R c= TolClasses T implies R c= T
proof
assume
A1: TolClasses R c= TolClasses T;
let x,y be object;
assume [x,y] in R;
then consider Z being TolClass of R such that
A2: x in Z & y in Z by Th20;
Z in TolClasses R by Def4;
then Z is TolSet of T by A1,Def4;
hence thesis by A2,Def1;
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,Def4;
hence thesis by Def4;
end;
hence thesis by Th26;
end;
theorem
union TolClasses T = X
proof
for x being object holds x in union TolClasses T iff x in X
proof
let x be object;
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 and
A2: Z in TolClasses T by TARSKI:def 4;
Z is TolSet of T by A2,Def4;
then Z c= X by Th18;
hence thesis by A1;
end;
assume x in X;
then consider Z being TolClass of T such that
A3: x in Z by Th21;
Z in TolClasses T by Def4;
hence thesis by A3,TARSKI:def 4;
end;
hence thesis by TARSKI:2;
end;
theorem
union TolSets T = X
proof
for x being object holds x in union TolSets T iff x in X
proof
let x be object;
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 and
A2: Z in TolSets T by TARSKI:def 4;
Z is TolSet of T by A2,Def3;
then Z c= X by Th18;
hence thesis by A1;
end;
assume x in X;
then consider Z being TolClass of T such that
A3: x in Z by Th21;
Z in TolSets T by Def3;
hence thesis by A3,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
assume
A1: for x st x in X holds neighbourhood(x,T) is TolSet of T;
A2: field T = X by ORDERS_1:12;
for x,y,z being object
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 be object;
assume that
x in field T and
A3: y in field T and
z in field T and
A4: [x,y] in T and
A5: [y,z] in T;
reconsider N = neighbourhood(y,T) as TolSet of T by A2,A1,A3;
[y,x] in T by A4,EQREL_1:6;
then
A6: x in N by Th27;
z in N by A5,Th27;
hence thesis by A6,Def1;
end;
then T is_transitive_in field T;
hence thesis;
end;
theorem
T is transitive implies for x st x in X holds neighbourhood(x,T) is
TolClass of T
proof
assume
A1: T is transitive;
let x;
assume
A2: x in X;
set N = Class(T,x);
field T = X by ORDERS_1:12;
then
A3: T is_transitive_in X by A1;
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 and
A5: z in N;
[x,y] in T by A4,Th27;
then
A6: [y,x] in T by EQREL_1:6;
[x,z] in T by A5,Th27;
hence thesis by A3,A2,A4,A5,A6;
end;
then reconsider Z = N as TolSet of T by Def1;
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 and
y in X;
A8: x in Z by A2,EQREL_1:20;
assume for z st z in Z holds [y,z] in T;
then [y,x] in T by A8;
then [x,y] in T by EQREL_1:6;
hence contradiction by A7,Th27;
end;
hence thesis by Def2;
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 being object st y in Y holds y in neighbourhood(x,T)
proof
let y be object;
assume y in Y;
then [x,y] in T by A1,Def1;
hence thesis by Th27;
end;
hence thesis;
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 be object;
assume [x,y] in R;
then consider Z being TolClass of R such that
A2: x in Z & y in Z by Th20;
Z in TolSets R by Def3;
then Z is TolSet of T by A1,Def3;
hence thesis by A2,Def1;
end;
assume
A3: R c= T;
let x be object;
assume x in TolSets R;
then reconsider Z = x as TolSet of R by Def3;
for x,y st x in Z & y in Z holds [x,y] in T
by Def1,A3;
then Z is TolSet of T by Def1;
hence thesis by Def3;
end;
theorem
TolClasses T c= TolSets T
proof
let x be object;
assume x in TolClasses T;
then x is TolSet of T by Def4;
hence thesis by Def3;
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 be object;
assume
A2: [x,y] in R;
then x in X by ZFMISC_1:87;
then
A3: neighbourhood(x,R) c= neighbourhood(x,T) by A1;
y in neighbourhood(x,R) by A2,Th27;
hence thesis by A3,Th27;
end;
theorem
T c= T*T
proof
let x,y be object;
assume
A1: [x,y] in T;
then y in X by ZFMISC_1:87;
then [y,y] in T by Th7;
hence thesis by A1,RELAT_1:def 8;
end;