:: TOLER_1 semantic presentation

theorem Th1: :: TOLER_1:1
field {} = {} ;

theorem Th2: :: TOLER_1:2
{} is reflexive
proof end;

theorem Th3: :: TOLER_1:3
{} is symmetric
proof end;

theorem Th4: :: TOLER_1:4
{} is irreflexive
proof end;

theorem Th5: :: TOLER_1:5
{} is antisymmetric
proof end;

theorem Th6: :: TOLER_1:6
{} is asymmetric
proof end;

theorem Th7: :: TOLER_1:7
{} is connected
proof end;

theorem Th8: :: TOLER_1:8
{} is strongly_connected
proof end;

theorem Th9: :: TOLER_1:9
{} 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 c1 be set ;
synonym Total c1 for nabla c1;
end;

definition
let c1 be Relation;
let c2 be set ;
redefine func |_2 as c1 |_2 c2 -> Relation of a2,a2;
coherence
c1 |_2 c2 is Relation of c2,c2
proof end;
end;

theorem Th10: :: TOLER_1:10
canceled;

theorem Th11: :: TOLER_1:11
canceled;

theorem Th12: :: TOLER_1:12
canceled;

theorem Th13: :: TOLER_1:13
for b1 being set holds rng (Total b1) = b1
proof end;

theorem Th14: :: TOLER_1:14
canceled;

theorem Th15: :: TOLER_1:15
for b1, b2, b3 being set st b2 in b1 & b3 in b1 holds
[b2,b3] in Total b1
proof end;

theorem Th16: :: TOLER_1:16
for b1, b2, b3 being set st b2 in field (Total b1) & b3 in field (Total b1) holds
[b2,b3] in Total b1
proof end;

theorem Th17: :: TOLER_1:17
canceled;

theorem Th18: :: TOLER_1:18
canceled;

theorem Th19: :: TOLER_1:19
for b1 being set holds Total b1 is strongly_connected
proof end;

theorem Th20: :: TOLER_1:20
canceled;

theorem Th21: :: TOLER_1:21
for b1 being set holds Total b1 is connected
proof end;

theorem Th22: :: TOLER_1:22
canceled;

theorem Th23: :: TOLER_1:23
canceled;

theorem Th24: :: TOLER_1:24
canceled;

theorem Th25: :: TOLER_1:25
for b1 being set
for b2 being Tolerance of b1 holds rng b2 = b1
proof end;

theorem Th26: :: TOLER_1:26
canceled;

theorem Th27: :: TOLER_1:27
for b1, b2 being set
for b3 being reflexive total Relation of b1 holds
( b2 in b1 iff [b2,b2] in b3 )
proof end;

theorem Th28: :: TOLER_1:28
for b1 being set
for b2 being Tolerance of b1 holds b2 is_reflexive_in b1
proof end;

theorem Th29: :: TOLER_1:29
for b1 being set
for b2 being Tolerance of b1 holds b2 is_symmetric_in b1
proof end;

theorem Th30: :: TOLER_1:30
canceled;

theorem Th31: :: TOLER_1:31
canceled;

theorem Th32: :: TOLER_1:32
for b1, b2, b3 being set
for b4 being Relation of b1,b2 st b4 is symmetric holds
b4 |_2 b3 is symmetric
proof end;

definition
let c1 be set ;
let c2 be Tolerance of c1;
let c3 be Subset of c1;
redefine func |_2 as c2 |_2 c3 -> Tolerance of a3;
coherence
c2 |_2 c3 is Tolerance of c3
proof end;
end;

theorem Th33: :: TOLER_1:33
for b1, b2 being set
for b3 being Tolerance of b2 st b1 c= b2 holds
b3 |_2 b1 is Tolerance of b1
proof end;

definition
let c1 be set ;
let c2 be Tolerance of c1;
canceled;
canceled;
mode TolSet of c2 -> set means :Def3: :: TOLER_1:def 3
for b1, b2 being set st b1 in a3 & b2 in a3 holds
[b1,b2] in a2;
existence
ex b1 being set st
for b2, b3 being set st b2 in b1 & b3 in b1 holds
[b2,b3] in c2
proof end;
end;

:: deftheorem Def1 TOLER_1:def 1 :
canceled;

:: deftheorem Def2 TOLER_1:def 2 :
canceled;

:: deftheorem Def3 defines TolSet TOLER_1:def 3 :
for b1 being set
for b2 being Tolerance of b1
for b3 being set holds
( b3 is TolSet of b2 iff for b4, b5 being set st b4 in b3 & b5 in b3 holds
[b4,b5] in b2 );

theorem Th34: :: TOLER_1:34
for b1 being set
for b2 being Tolerance of b1 holds {} is TolSet of b2
proof end;

definition
let c1 be set ;
let c2 be Tolerance of c1;
let c3 be TolSet of c2;
attr a3 is TolClass-like means :Def4: :: TOLER_1:def 4
for b1 being set st not b1 in a3 & b1 in a1 holds
ex b2 being set st
( b2 in a3 & not [b1,b2] in a2 );
end;

:: deftheorem Def4 defines TolClass-like TOLER_1:def 4 :
for b1 being set
for b2 being Tolerance of b1
for b3 being TolSet of b2 holds
( b3 is TolClass-like iff for b4 being set st not b4 in b3 & b4 in b1 holds
ex b5 being set st
( b5 in b3 & not [b4,b5] in b2 ) );

registration
let c1 be set ;
let c2 be Tolerance of c1;
cluster TolClass-like TolSet of a2;
existence
ex b1 being TolSet of c2 st b1 is TolClass-like
proof end;
end;

definition
let c1 be set ;
let c2 be Tolerance of c1;
mode TolClass of a2 is TolClass-like TolSet of a2;
end;

theorem Th35: :: TOLER_1:35
canceled;

theorem Th36: :: TOLER_1:36
canceled;

theorem Th37: :: TOLER_1:37
canceled;

theorem Th38: :: TOLER_1:38
for b1 being set
for b2 being Tolerance of b1 st {} is TolClass of b2 holds
b2 = {}
proof end;

theorem Th39: :: TOLER_1:39
{} is Tolerance of {} by PARTFUN1:def 4, RELAT_1:60, RELSET_1:25;

theorem Th40: :: TOLER_1:40
for b1 being set
for b2 being Tolerance of b1
for b3, b4 being set st [b3,b4] in b2 holds
{b3,b4} is TolSet of b2
proof end;

theorem Th41: :: TOLER_1:41
for b1 being set
for b2 being Tolerance of b1
for b3 being set st b3 in b1 holds
{b3} is TolSet of b2
proof end;

theorem Th42: :: TOLER_1:42
for b1 being set
for b2 being Tolerance of b1
for b3, b4 being set st b3 is TolSet of b2 & b4 is TolSet of b2 holds
b3 /\ b4 is TolSet of b2
proof end;

theorem Th43: :: TOLER_1:43
for b1, b2 being set
for b3 being Tolerance of b2 st b1 is TolSet of b3 holds
b1 c= b2
proof end;

theorem Th44: :: TOLER_1:44
canceled;

theorem Th45: :: TOLER_1:45
for b1 being set
for b2 being Tolerance of b1
for b3 being TolSet of b2 ex b4 being TolClass of b2 st b3 c= b4
proof end;

theorem Th46: :: TOLER_1:46
for b1 being set
for b2 being Tolerance of b1
for b3, b4 being set st [b3,b4] in b2 holds
ex b5 being TolClass of b2 st
( b3 in b5 & b4 in b5 )
proof end;

theorem Th47: :: TOLER_1:47
for b1 being set
for b2 being Tolerance of b1
for b3 being set st b3 in b1 holds
ex b4 being TolClass of b2 st b3 in b4
proof end;

theorem Th48: :: TOLER_1:48
canceled;

theorem Th49: :: TOLER_1:49
for b1 being set
for b2 being Tolerance of b1 holds b2 c= Total b1
proof end;

theorem Th50: :: TOLER_1:50
for b1 being set
for b2 being Tolerance of b1 holds id b1 c= b2
proof end;

scheme :: TOLER_1:sch 1
s1{ F1() -> set , P1[ set , set ] } :
ex b1 being Tolerance of F1() st
for b2, b3 being set st b2 in F1() & b3 in F1() holds
( [b2,b3] in b1 iff P1[b2,b3] )
provided
E20: for b1 being set st b1 in F1() holds
P1[b1,b1] and
E21: for b1, b2 being set st b1 in F1() & b2 in F1() & P1[b1,b2] holds
P1[b2,b1]
proof end;

theorem Th51: :: TOLER_1:51
for b1 being set ex b2 being Tolerance of union b1 st
for b3 being set st b3 in b1 holds
b3 is TolSet of b2
proof end;

theorem Th52: :: TOLER_1:52
for b1 being set
for b2, b3 being Tolerance of union b1 st ( for b4, b5 being set holds
( [b4,b5] in b2 iff ex b6 being set st
( b6 in b1 & b4 in b6 & b5 in b6 ) ) ) & ( for b4, b5 being set holds
( [b4,b5] in b3 iff ex b6 being set st
( b6 in b1 & b4 in b6 & b5 in b6 ) ) ) holds
b2 = b3
proof end;

theorem Th53: :: TOLER_1:53
for b1 being set
for b2, b3 being Tolerance of b1 st ( for b4 being set holds
( b4 is TolClass of b2 iff b4 is TolClass of b3 ) ) holds
b2 = b3
proof end;

notation
let c1 be set ;
let c2 be Tolerance of c1;
let c3 be set ;
synonym neighbourhood c3,c2 for Class c2,c3;
end;

theorem Th54: :: TOLER_1:54
for b1, b2 being set
for b3 being Tolerance of b1
for b4 being set holds
( b4 in neighbourhood b2,b3 iff [b2,b4] in b3 )
proof end;

theorem Th55: :: TOLER_1:55
canceled;

theorem Th56: :: TOLER_1:56
canceled;

theorem Th57: :: TOLER_1:57
canceled;

theorem Th58: :: TOLER_1:58
for b1, b2 being set
for b3 being Tolerance of b1
for b4 being set st ( for b5 being set holds
( b5 in b4 iff ( b2 in b5 & b5 is TolClass of b3 ) ) ) holds
neighbourhood b2,b3 = union b4
proof end;

theorem Th59: :: TOLER_1:59
for b1, b2 being set
for b3 being Tolerance of b1
for b4 being set st ( for b5 being set holds
( b5 in b4 iff ( b2 in b5 & b5 is TolSet of b3 ) ) ) holds
neighbourhood b2,b3 = union b4
proof end;

definition
let c1 be set ;
let c2 be Tolerance of c1;
canceled;
func TolSets c2 -> set means :Def6: :: TOLER_1:def 6
for b1 being set holds
( b1 in a3 iff b1 is TolSet of a2 );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff b2 is TolSet of c2 )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff b3 is TolSet of c2 ) ) & ( for b3 being set holds
( b3 in b2 iff b3 is TolSet of c2 ) ) holds
b1 = b2
proof end;
func TolClasses c2 -> set means :Def7: :: TOLER_1:def 7
for b1 being set holds
( b1 in a3 iff b1 is TolClass of a2 );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff b2 is TolClass of c2 )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff b3 is TolClass of c2 ) ) & ( for b3 being set holds
( b3 in b2 iff b3 is TolClass of c2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 TOLER_1:def 5 :
canceled;

:: deftheorem Def6 defines TolSets TOLER_1:def 6 :
for b1 being set
for b2 being Tolerance of b1
for b3 being set holds
( b3 = TolSets b2 iff for b4 being set holds
( b4 in b3 iff b4 is TolSet of b2 ) );

:: deftheorem Def7 defines TolClasses TOLER_1:def 7 :
for b1 being set
for b2 being Tolerance of b1
for b3 being set holds
( b3 = TolClasses b2 iff for b4 being set holds
( b4 in b3 iff b4 is TolClass of b2 ) );

theorem Th60: :: TOLER_1:60
canceled;

theorem Th61: :: TOLER_1:61
canceled;

theorem Th62: :: TOLER_1:62
canceled;

theorem Th63: :: TOLER_1:63
canceled;

theorem Th64: :: TOLER_1:64
for b1 being set
for b2, b3 being Tolerance of b1 st TolClasses b2 c= TolClasses b3 holds
b2 c= b3
proof end;

theorem Th65: :: TOLER_1:65
for b1 being set
for b2, b3 being Tolerance of b1 st TolClasses b2 = TolClasses b3 holds
b2 = b3
proof end;

theorem Th66: :: TOLER_1:66
for b1 being set
for b2 being Tolerance of b1 holds union (TolClasses b2) = b1
proof end;

theorem Th67: :: TOLER_1:67
for b1 being set
for b2 being Tolerance of b1 holds union (TolSets b2) = b1
proof end;

theorem Th68: :: TOLER_1:68
for b1 being set
for b2 being Tolerance of b1 st ( for b3 being set st b3 in b1 holds
neighbourhood b3,b2 is TolSet of b2 ) holds
b2 is transitive
proof end;

theorem Th69: :: TOLER_1:69
for b1 being set
for b2 being Tolerance of b1 st b2 is transitive holds
for b3 being set st b3 in b1 holds
neighbourhood b3,b2 is TolClass of b2
proof end;

theorem Th70: :: TOLER_1:70
for b1 being set
for b2 being Tolerance of b1
for b3 being set
for b4 being TolClass of b2 st b3 in b4 holds
b4 c= neighbourhood b3,b2
proof end;

theorem Th71: :: TOLER_1:71
for b1 being set
for b2, b3 being Tolerance of b1 holds
( TolSets b2 c= TolSets b3 iff b2 c= b3 )
proof end;

theorem Th72: :: TOLER_1:72
for b1 being set
for b2 being Tolerance of b1 holds TolClasses b2 c= TolSets b2
proof end;

theorem Th73: :: TOLER_1:73
for b1 being set
for b2, b3 being Tolerance of b1 st ( for b4 being set st b4 in b1 holds
neighbourhood b4,b2 c= neighbourhood b4,b3 ) holds
b2 c= b3
proof end;

theorem Th74: :: TOLER_1:74
for b1 being set
for b2 being Tolerance of b1 holds b2 c= b2 * b2
proof end;