begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem Th15:
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem Th27:
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem Th32:
theorem
:: deftheorem TOLER_1:def 1 :
canceled;
:: deftheorem TOLER_1:def 2 :
canceled;
:: deftheorem Def3 defines TolSet TOLER_1:def 3 :
theorem Th34:
:: deftheorem Def4 defines TolClass-like TOLER_1:def 4 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem Th40:
theorem
theorem
theorem Th43:
theorem
canceled;
theorem Th45:
theorem Th46:
theorem Th47:
theorem
canceled;
theorem
theorem
scheme
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]
theorem
theorem
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
theorem Th53:
theorem Th54:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
:: deftheorem TOLER_1:def 5 :
canceled;
:: deftheorem Def6 defines TolSets TOLER_1:def 6 :
:: deftheorem Def7 defines TolClasses TOLER_1:def 7 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem