:: by Krzysztof Hryniewiecki

::

:: Received September 20, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

registration

for b_{1} being Relation st b_{1} is empty holds

( b_{1} is reflexive & b_{1} is irreflexive & b_{1} is symmetric & b_{1} is antisymmetric & b_{1} is asymmetric & b_{1} is connected & b_{1} is strongly_connected & b_{1} is transitive )
end;

cluster Relation-like empty -> reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive for set ;

coherence for b

( b

proof end;

definition

let R be Relation;

let Y be set ;

:: original: |_2

redefine func R |_2 Y -> Relation of Y,Y;

coherence

R |_2 Y is Relation of Y,Y by XBOOLE_1:17;

end;
let Y be set ;

:: original: |_2

redefine func R |_2 Y -> Relation of Y,Y;

coherence

R |_2 Y is Relation of Y,Y by XBOOLE_1:17;

definition

let X be set ;

let T be Tolerance of X;

let Y be Subset of X;

:: original: |_2

redefine func T |_2 Y -> Tolerance of Y;

coherence

T |_2 Y is Tolerance of Y

end;
let T be Tolerance of X;

let Y be Subset of X;

:: original: |_2

redefine func T |_2 Y -> Tolerance of Y;

coherence

T |_2 Y is Tolerance of Y

proof end;

:: Set and Class of Tolerance

definition

let X be set ;

let T be Tolerance of X;

ex b_{1} being set st

for x, y being set st x in b_{1} & y in b_{1} holds

[x,y] in T

end;
let T be Tolerance of X;

mode TolSet of T -> set means :Def1: :: TOLER_1:def 1

for x, y being set st x in it & y in it holds

[x,y] in T;

existence for x, y being set st x in it & y in it holds

[x,y] in T;

ex b

for x, y being set st x in b

[x,y] in T

proof end;

:: deftheorem Def1 defines TolSet TOLER_1:def 1 :

for X being set

for T being Tolerance of X

for b_{3} being set holds

( b_{3} is TolSet of T iff for x, y being set st x in b_{3} & y in b_{3} holds

[x,y] in T );

for X being set

for T being Tolerance of X

for b

( b

[x,y] in T );

:: deftheorem Def2 defines TolClass-like TOLER_1:def 2 :

for X being set

for T being Tolerance of X

for IT being TolSet of T holds

( IT is TolClass-like iff for x being set st not x in IT & x in X holds

ex y being set st

( y in IT & not [x,y] in T ) );

for X being set

for T being Tolerance of X

for IT being TolSet of T holds

( IT is TolClass-like iff for x being set st not x in IT & x in X holds

ex y being set st

( y in IT & not [x,y] in T ) );

registration

let X be set ;

let T be Tolerance of X;

existence

ex b_{1} being TolSet of T st b_{1} is TolClass-like

end;
let T be Tolerance of X;

existence

ex b

proof end;

definition
end;

theorem Th15: :: TOLER_1:15

for X being set

for T being Tolerance of X

for x, y being set st [x,y] in T holds

{x,y} is TolSet of T

for T being Tolerance of X

for x, y being set st [x,y] in T holds

{x,y} is TolSet of T

proof end;

theorem :: TOLER_1:17

for X being set

for T being Tolerance of X

for Y, Z being set st Y is TolSet of T holds

Y /\ Z is TolSet of T

for T being Tolerance of X

for Y, Z being set st Y is TolSet of T holds

Y /\ Z is TolSet of T

proof end;

theorem Th19: :: TOLER_1:19

for X being set

for T being Tolerance of X

for Y being TolSet of T ex Z being TolClass of T st Y c= Z

for T being Tolerance of X

for Y being TolSet of T ex Z being TolClass of T st Y c= Z

proof end;

theorem Th20: :: TOLER_1:20

for X being set

for T being Tolerance of X

for x, y being set st [x,y] in T holds

ex Z being TolClass of T st

( x in Z & y in Z )

for T being Tolerance of X

for x, y being set st [x,y] in T holds

ex Z being TolClass of T st

( x in Z & y in Z )

proof end;

theorem Th21: :: TOLER_1:21

for X being set

for T being Tolerance of X

for x being set st x in X holds

ex Z being TolClass of T st x in Z

for T being Tolerance of X

for x being set st x in X holds

ex Z being TolClass of T st x in Z

proof end;

scheme :: TOLER_1:sch 1

ToleranceEx{ F_{1}() -> set , P_{1}[ set , set ] } :

ToleranceEx{ F

ex T being Tolerance of F_{1}() st

for x, y being set st x in F_{1}() & y in F_{1}() holds

( [x,y] in T iff P_{1}[x,y] )

providedfor x, y being set st x in F

( [x,y] in T iff P

A1:
for x being set st x in F_{1}() holds

P_{1}[x,x]
and

A2: for x, y being set st x in F_{1}() & y in F_{1}() & P_{1}[x,y] holds

P_{1}[y,x]

P

A2: for x, y being set st x in F

P

proof end;

theorem :: TOLER_1:24

for Y being set ex T being Tolerance of (union Y) st

for Z being set st Z in Y holds

Z is TolSet of T

for Z being set st Z in Y holds

Z is TolSet of T

proof end;

theorem :: TOLER_1:25

for Y being set

for T, R being Tolerance of (union Y) st ( for x, y being set holds

( [x,y] in T iff ex Z being set st

( Z in Y & x in Z & y in Z ) ) ) & ( for x, y being set holds

( [x,y] in R iff ex Z being set st

( Z in Y & x in Z & y in Z ) ) ) holds

T = R

for T, R being Tolerance of (union Y) st ( for x, y being set holds

( [x,y] in T iff ex Z being set st

( Z in Y & x in Z & y in Z ) ) ) & ( for x, y being set holds

( [x,y] in R iff ex Z being set st

( Z in Y & x in Z & y in Z ) ) ) holds

T = R

proof end;

theorem Th26: :: TOLER_1:26

for X being set

for T, R being Tolerance of X st ( for Z being set holds

( Z is TolClass of T iff Z is TolClass of R ) ) holds

T = R

for T, R being Tolerance of X st ( for Z being set holds

( Z is TolClass of T iff Z is TolClass of R ) ) holds

T = R

proof end;

notation

let X, Y be set ;

let T be Relation of X,Y;

let x be set ;

synonym neighbourhood (x,T) for Class (X,Y);

end;
let T be Relation of X,Y;

let x be set ;

synonym neighbourhood (x,T) for Class (X,Y);

theorem Th27: :: TOLER_1:27

for X, x being set

for T being Tolerance of X

for y being set holds

( y in neighbourhood (,) iff [x,y] in T )

for T being Tolerance of X

for y being set holds

( y in neighbourhood (,) iff [x,y] in T )

proof end;

theorem :: TOLER_1:28

for X, x being set

for T being Tolerance of X

for Y being set st ( for Z being set holds

( Z in Y iff ( x in Z & Z is TolClass of T ) ) ) holds

neighbourhood (,) = union Y

for T being Tolerance of X

for Y being set st ( for Z being set holds

( Z in Y iff ( x in Z & Z is TolClass of T ) ) ) holds

neighbourhood (,) = union Y

proof end;

theorem :: TOLER_1:29

for X, x being set

for T being Tolerance of X

for Y being set st ( for Z being set holds

( Z in Y iff ( x in Z & Z is TolSet of T ) ) ) holds

neighbourhood (,) = union Y

for T being Tolerance of X

for Y being set st ( for Z being set holds

( Z in Y iff ( x in Z & Z is TolSet of T ) ) ) holds

neighbourhood (,) = union Y

proof end;

:: Family of sets and classes of proximity

definition

let X be set ;

let T be Tolerance of X;

ex b_{1} being set st

for Y being set holds

( Y in b_{1} iff Y is TolSet of T )

for b_{1}, b_{2} being set st ( for Y being set holds

( Y in b_{1} iff Y is TolSet of T ) ) & ( for Y being set holds

( Y in b_{2} iff Y is TolSet of T ) ) holds

b_{1} = b_{2}

ex b_{1} being set st

for Y being set holds

( Y in b_{1} iff Y is TolClass of T )

for b_{1}, b_{2} being set st ( for Y being set holds

( Y in b_{1} iff Y is TolClass of T ) ) & ( for Y being set holds

( Y in b_{2} iff Y is TolClass of T ) ) holds

b_{1} = b_{2}

end;
let T be Tolerance of X;

func TolSets T -> set means :Def3: :: TOLER_1:def 3

for Y being set holds

( Y in it iff Y is TolSet of T );

existence for Y being set holds

( Y in it iff Y is TolSet of T );

ex b

for Y being set holds

( Y in b

proof end;

uniqueness for b

( Y in b

( Y in b

b

proof end;

func TolClasses T -> set means :Def4: :: TOLER_1:def 4

for Y being set holds

( Y in it iff Y is TolClass of T );

existence for Y being set holds

( Y in it iff Y is TolClass of T );

ex b

for Y being set holds

( Y in b

proof end;

uniqueness for b

( Y in b

( Y in b

b

proof end;

:: deftheorem Def3 defines TolSets TOLER_1:def 3 :

for X being set

for T being Tolerance of X

for b_{3} being set holds

( b_{3} = TolSets T iff for Y being set holds

( Y in b_{3} iff Y is TolSet of T ) );

for X being set

for T being Tolerance of X

for b

( b

( Y in b

:: deftheorem Def4 defines TolClasses TOLER_1:def 4 :

for X being set

for T being Tolerance of X

for b_{3} being set holds

( b_{3} = TolClasses T iff for Y being set holds

( Y in b_{3} iff Y is TolClass of T ) );

for X being set

for T being Tolerance of X

for b

( b

( Y in b

theorem :: TOLER_1:34

for X being set

for T being Tolerance of X st ( for x being set st x in X holds

neighbourhood (,) is TolSet of T ) holds

T is transitive

for T being Tolerance of X st ( for x being set st x in X holds

neighbourhood (,) is TolSet of T ) holds

T is transitive

proof end;

theorem :: TOLER_1:35

for X being set

for T being Tolerance of X st T is transitive holds

for x being set st x in X holds

neighbourhood (,) is TolClass of T

for T being Tolerance of X st T is transitive holds

for x being set st x in X holds

neighbourhood (,) is TolClass of T

proof end;

theorem :: TOLER_1:36

for X being set

for T being Tolerance of X

for x being set

for Y being TolClass of T st x in Y holds

Y c= neighbourhood (,)

for T being Tolerance of X

for x being set

for Y being TolClass of T st x in Y holds

Y c= neighbourhood (,)

proof end;

theorem :: TOLER_1:39

for X being set

for R, T being Tolerance of X st ( for x being set st x in X holds

neighbourhood (,) c= neighbourhood (,) ) holds

R c= T

for R, T being Tolerance of X st ( for x being set st x in X holds

neighbourhood (,) c= neighbourhood (,) ) holds

R c= T

proof end;