:: Relations of Tolerance
:: by Krzysztof Hryniewiecki
::
:: Received September 20, 1990
:: Copyright (c) 1990 Association of Mizar Users

begin

registration

cluster Relation-like empty -> reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive set ;
coherence
for b₁ being Relation st b₁ is empty holds
( b₁ is reflexive & b₁ is irreflexive & b₁ is symmetric & b₁ is antisymmetric & b₁ is asymmetric & b₁ is connected & b₁ is strongly_connected & b₁ is transitive )

proof end;

end;

notation

let X be set ;
synonym Total X for nabla X;

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;

theorem :: TOLER_1:1

canceled;

theorem :: TOLER_1:2

canceled;

theorem :: TOLER_1:3

canceled;

theorem :: TOLER_1:4

canceled;

theorem :: TOLER_1:5

canceled;

theorem :: TOLER_1:6

canceled;

theorem :: TOLER_1:7

canceled;

theorem :: TOLER_1:8

canceled;

theorem :: TOLER_1:9

canceled;

theorem :: TOLER_1:10

canceled;

theorem :: TOLER_1:11

canceled;

theorem :: TOLER_1:12

canceled;

theorem :: TOLER_1:13

for X being set holds rng (Total X) = X

proof end;

theorem :: TOLER_1:14

canceled;

theorem Th15: :: TOLER_1:15

for X, x, y being set st x in X & y in X holds
[x,y] in Total X

proof end;

theorem :: TOLER_1:16

for X, x, y being set st x in field (Total X) & y in field (Total X) holds
[x,y] in Total X

proof end;

theorem :: TOLER_1:17

canceled;

theorem :: TOLER_1:18

canceled;

theorem :: TOLER_1:19

for X being set holds Total X is strongly_connected

proof end;

theorem :: TOLER_1:20

canceled;

theorem :: TOLER_1:21

for X being set holds Total X is connected

proof end;

theorem :: TOLER_1:22

canceled;

theorem :: TOLER_1:23

canceled;

theorem :: TOLER_1:24

canceled;

theorem :: TOLER_1:25

for X being set
for T being Tolerance of X holds rng T = X

proof end;

theorem :: TOLER_1:26

canceled;

theorem Th27: :: TOLER_1:27

for X, x being set
for T being reflexive total Relation of X holds
( x in X iff [x,x] in T )

proof end;

theorem :: TOLER_1:28

for X being set
for T being Tolerance of X holds T is_reflexive_in X

proof end;

theorem :: TOLER_1:29

for X being set
for T being Tolerance of X holds T is_symmetric_in X

proof end;

theorem :: TOLER_1:30

canceled;

theorem :: TOLER_1:31

canceled;

theorem Th32: :: TOLER_1:32

for X, Y, Z being set
for R being Relation of X,Y st R is symmetric holds
R |_2 Z is symmetric

proof end;

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

proof end;

end;

theorem :: TOLER_1:33

for Y, X being set
for T being Tolerance of X st Y c= X holds
T |_2 Y is Tolerance of Y

proof end;

definition

let X be set ;
let T be Tolerance of X;
canceled;
canceled;
mode TolSet of T -> set means :Def3: :: TOLER_1:def 3
for x, y being set st x in it & y in it holds
[x,y] in T;
existence
ex b₁ being set st
for x, y being set st x in b₁ & y in b₁ holds
[x,y] in T

proof end;

end;

:: deftheorem TOLER_1:def 1 :
canceled;

:: deftheorem TOLER_1:def 2 :
canceled;

:: deftheorem Def3 defines TolSet TOLER_1:def 3 :
for X being set
for T being Tolerance of X
for b₃ being set holds
( b₃ is TolSet of T iff for x, y being set st x in b₃ & y in b₃ holds
[x,y] in T );

theorem Th34: :: TOLER_1:34

for X being set
for T being Tolerance of X holds {} is TolSet of T

proof end;

definition

let X be set ;
let T be Tolerance of X;
let IT be TolSet of T;
attr IT is TolClass-like means :Def4: :: TOLER_1:def 4
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 );

end;

:: deftheorem Def4 defines TolClass-like TOLER_1:def 4 :
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;
cluster TolClass-like TolSet of T;
existence
ex b₁ being TolSet of T st b₁ is TolClass-like

proof end;

end;

definition

let X be set ;
let T be Tolerance of X;
mode TolClass of T is TolClass-like TolSet of T;

end;

theorem :: TOLER_1:35

canceled;

theorem :: TOLER_1:36

canceled;

theorem :: TOLER_1:37

canceled;

theorem :: TOLER_1:38

for X being set
for T being Tolerance of X st {} is TolClass of T holds
T = {}

proof end;

theorem :: TOLER_1:39

{} is Tolerance of {} by RELSET_1:25;

theorem Th40: :: TOLER_1:40

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

proof end;

theorem :: TOLER_1:41

for X being set
for T being Tolerance of X
for x being set st x in X holds
{x} is TolSet of T

proof end;

theorem :: TOLER_1:42

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

proof end;

theorem Th43: :: TOLER_1:43

for Y, X being set
for T being Tolerance of X st Y is TolSet of T holds
Y c= X

proof end;

theorem :: TOLER_1:44

canceled;

theorem Th45: :: TOLER_1:45

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

proof end;

theorem Th46: :: TOLER_1:46

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 )

proof end;

theorem Th47: :: TOLER_1:47

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

proof end;

theorem :: TOLER_1:48

canceled;

theorem :: TOLER_1:49

for X being set
for T being Tolerance of X holds T c= Total X

proof end;

theorem :: TOLER_1:50

for X being set
for T being Tolerance of X holds id X c= T

proof end;

scheme :: TOLER_1:sch 1
ToleranceEx{ F₁() -> set , P₁[ set , set ] } :

ex T being Tolerance of F₁() st
for x, y being set st x in F₁() & y in F₁() holds
( [x,y] in T iff P₁[x,y] )

provided

A1: for x being set st x in F₁() holds
P₁[x,x] and
A2: for x, y being set st x in F₁() & y in F₁() & P₁[x,y] holds
P₁[y,x]

proof end;

theorem :: TOLER_1:51

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

proof end;

theorem :: TOLER_1:52

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

proof end;

theorem Th53: :: TOLER_1:53

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

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;

theorem Th54: :: TOLER_1:54

for X, x being set
for T being Tolerance of X
for y being set holds
( y in neighbourhood (,) iff [x,y] in T )

proof end;

theorem :: TOLER_1:55

canceled;

theorem :: TOLER_1:56

canceled;

theorem :: TOLER_1:57

canceled;

theorem :: TOLER_1:58

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

proof end;

theorem :: TOLER_1:59

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

proof end;

definition

let X be set ;
let T be Tolerance of X;
canceled;
func TolSets T -> set means :Def6: :: TOLER_1:def 6
for Y being set holds
( Y in it iff Y is TolSet of T );
existence
ex b₁ being set st
for Y being set holds
( Y in b₁ iff Y is TolSet of T )

proof end;

uniqueness
for b₁, b₂ being set st ( for Y being set holds
( Y in b₁ iff Y is TolSet of T ) ) & ( for Y being set holds
( Y in b₂ iff Y is TolSet of T ) ) holds
b₁ = b₂

proof end;

func TolClasses T -> set means :Def7: :: TOLER_1:def 7
for Y being set holds
( Y in it iff Y is TolClass of T );
existence
ex b₁ being set st
for Y being set holds
( Y in b₁ iff Y is TolClass of T )

proof end;

uniqueness
for b₁, b₂ being set st ( for Y being set holds
( Y in b₁ iff Y is TolClass of T ) ) & ( for Y being set holds
( Y in b₂ iff Y is TolClass of T ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem TOLER_1:def 5 :
canceled;

:: deftheorem Def6 defines TolSets TOLER_1:def 6 :
for X being set
for T being Tolerance of X
for b₃ being set holds
( b₃ = TolSets T iff for Y being set holds
( Y in b₃ iff Y is TolSet of T ) );

:: deftheorem Def7 defines TolClasses TOLER_1:def 7 :
for X being set
for T being Tolerance of X
for b₃ being set holds
( b₃ = TolClasses T iff for Y being set holds
( Y in b₃ iff Y is TolClass of T ) );

theorem :: TOLER_1:60

canceled;

theorem :: TOLER_1:61

canceled;

theorem :: TOLER_1:62

canceled;

theorem :: TOLER_1:63

canceled;

theorem :: TOLER_1:64

for X being set
for R, T being Tolerance of X st TolClasses R c= TolClasses T holds
R c= T

proof end;

theorem :: TOLER_1:65

for X being set
for T, R being Tolerance of X st TolClasses T = TolClasses R holds
T = R

proof end;

theorem :: TOLER_1:66

for X being set
for T being Tolerance of X holds union (TolClasses T) = X

proof end;

theorem :: TOLER_1:67

for X being set
for T being Tolerance of X holds union (TolSets T) = X

proof end;

theorem :: TOLER_1:68

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

proof end;

theorem :: TOLER_1:69

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

proof end;

theorem :: TOLER_1:70

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 (,)

proof end;

theorem :: TOLER_1:71

for X being set
for R, T being Tolerance of X holds
( TolSets R c= TolSets T iff R c= T )

proof end;

theorem :: TOLER_1:72

for X being set
for T being Tolerance of X holds TolClasses T c= TolSets T

proof end;

theorem :: TOLER_1:73

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

proof end;

theorem :: TOLER_1:74

for X being set
for T being Tolerance of X holds T c= T * T

proof end;