:: TOLER_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem :: TOLER_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
field {} = {} ;

theorem Th2: :: TOLER_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{} is reflexive
proof end;

theorem Th3: :: TOLER_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{} is symmetric
proof end;

theorem Th4: :: TOLER_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{} is irreflexive
proof end;

theorem Th5: :: TOLER_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{} is antisymmetric
proof end;

theorem Th6: :: TOLER_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{} is asymmetric
proof end;

theorem Th7: :: TOLER_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{} is connected
proof end;

theorem Th8: :: TOLER_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{} is strongly_connected
proof end;

theorem Th9: :: TOLER_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{} is transitive
proof end;

registration
cluster {} -> reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive ;
coherence
( {} is reflexive & {} is irreflexive & {} is symmetric & {} is antisymmetric & {} is asymmetric & {} is connected & {} is strongly_connected & {} is transitive ) by Th2, Th3, Th4, Th5, Th6, Th7, Th8, Th9;
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
proof end;
end;

theorem :: TOLER_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOLER_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOLER_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOLER_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds rng (Total X) = X
proof end;

theorem :: TOLER_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th15: :: TOLER_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOLER_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOLER_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds Total X is strongly_connected
proof end;

theorem :: TOLER_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOLER_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds Total X is connected
proof end;

theorem :: TOLER_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOLER_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOLER_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOLER_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for T being Tolerance of X holds rng T = X
proof end;

theorem :: TOLER_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th27: :: TOLER_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for T being Tolerance of X holds T is_reflexive_in X
proof end;

theorem :: TOLER_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for T being Tolerance of X holds T is_symmetric_in X
proof end;

theorem :: TOLER_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOLER_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th32: :: TOLER_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 b1 being set st
for x, y being set st x in b1 & y in b1 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 b3 being set holds
( b3 is TolSet of T iff for x, y being set st x in b3 & y in b3 holds
[x,y] in T );

theorem Th34: :: TOLER_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 b1 being TolSet of T st b1 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOLER_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOLER_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOLER_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for T being Tolerance of X st {} is TolClass of T holds
T = {}
proof end;

theorem :: TOLER_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{} is Tolerance of {} by PARTFUN1:def 4, RELAT_1:60, RELSET_1:25;

theorem Th40: :: TOLER_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for T being Tolerance of X
for Y, Z being set st Y is TolSet of T & Z is TolSet of T holds
Y /\ Z is TolSet of T
proof end;

theorem Th43: :: TOLER_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th45: :: TOLER_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOLER_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for T being Tolerance of X holds T c= Total X
proof end;

theorem :: TOLER_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for T being Tolerance of X holds id X c= T
proof end;

scheme :: TOLER_1:sch 1
ToleranceEx{ F1() -> set , P1[ set , set ] } :
ex T being Tolerance of F1() st
for x, y being set st x in F1() & y in F1() holds
( [x,y] in T iff P1[x,y] )
provided
A1: for x being set st x in F1() holds
P1[x,x] and
A2: for x, y being set st x in F1() & y in F1() & P1[x,y] holds
P1[y,x]
proof end;

theorem :: TOLER_1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 be set ;
let T be Tolerance of X;
let x be set ;
synonym neighbourhood x,T for Class T,x;
end;

theorem Th54: :: TOLER_1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, x being set
for T being Tolerance of X
for y being set holds
( y in neighbourhood x,T iff [x,y] in T )
proof end;

theorem :: TOLER_1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOLER_1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOLER_1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOLER_1:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 x,T = union Y
proof end;

theorem :: TOLER_1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 x,T = 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 b1 being set st
for Y being set holds
( Y in b1 iff Y is TolSet of T )
proof end;
uniqueness
for b1, b2 being set st ( for Y being set holds
( Y in b1 iff Y is TolSet of T ) ) & ( for Y being set holds
( Y in b2 iff Y is TolSet of T ) ) holds
b1 = b2
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 b1 being set st
for Y being set holds
( Y in b1 iff Y is TolClass of T )
proof end;
uniqueness
for b1, b2 being set st ( for Y being set holds
( Y in b1 iff Y is TolClass of T ) ) & ( for Y being set holds
( Y in b2 iff Y is TolClass of T ) ) holds
b1 = b2
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 b3 being set holds
( b3 = TolSets T iff for Y being set holds
( Y in b3 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 b3 being set holds
( b3 = TolClasses T iff for Y being set holds
( Y in b3 iff Y is TolClass of T ) );

theorem :: TOLER_1:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOLER_1:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOLER_1:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOLER_1:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOLER_1:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for T being Tolerance of X holds union (TolClasses T) = X
proof end;

theorem :: TOLER_1:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for T being Tolerance of X holds union (TolSets T) = X
proof end;

theorem :: TOLER_1:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for T being Tolerance of X st ( for x being set st x in X holds
neighbourhood x,T is TolSet of T ) holds
T is transitive
proof end;

theorem :: TOLER_1:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 x,T is TolClass of T
proof end;

theorem :: TOLER_1:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 x,T
proof end;

theorem :: TOLER_1:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for T being Tolerance of X holds TolClasses T c= TolSets T
proof end;

theorem :: TOLER_1:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for R, T being Tolerance of X st ( for x being set st x in X holds
neighbourhood x,R c= neighbourhood x,T ) holds
R c= T
proof end;

theorem :: TOLER_1:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for T being Tolerance of X holds T c= T * T
proof end;