:: Relations of Tolerance
:: by Krzysztof Hryniewiecki
::
:: Received September 20, 1990
:: Copyright (c) 1990 Association of Mizar Users
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
theorem :: TOLER_1:14
canceled;
theorem Th15: :: TOLER_1:15
theorem :: TOLER_1:16
theorem :: TOLER_1:17
canceled;
theorem :: TOLER_1:18
canceled;
theorem :: TOLER_1:19
theorem :: TOLER_1:20
canceled;
theorem :: TOLER_1:21
theorem :: TOLER_1:22
canceled;
theorem :: TOLER_1:23
canceled;
theorem :: TOLER_1:24
canceled;
theorem :: TOLER_1:25
theorem :: TOLER_1:26
canceled;
theorem Th27: :: TOLER_1:27
theorem :: TOLER_1:28
theorem :: TOLER_1:29
theorem :: TOLER_1:30
canceled;
theorem :: TOLER_1:31
canceled;
theorem Th32: :: TOLER_1:32
theorem :: TOLER_1:33
:: deftheorem TOLER_1:def 1 :
canceled;
:: deftheorem TOLER_1:def 2 :
canceled;
:: deftheorem Def3 defines TolSet TOLER_1:def 3 :
theorem Th34: :: TOLER_1:34
:: deftheorem Def4 defines TolClass-like TOLER_1:def 4 :
theorem :: TOLER_1:35
canceled;
theorem :: TOLER_1:36
canceled;
theorem :: TOLER_1:37
canceled;
theorem :: TOLER_1:38
theorem :: TOLER_1:39
theorem Th40: :: TOLER_1:40
theorem :: TOLER_1:41
theorem :: TOLER_1:42
theorem Th43: :: TOLER_1:43
theorem :: TOLER_1:44
canceled;
theorem Th45: :: TOLER_1:45
theorem Th46: :: TOLER_1:46
theorem Th47: :: TOLER_1:47
theorem :: TOLER_1:48
canceled;
theorem :: TOLER_1:49
theorem :: TOLER_1:50
theorem :: TOLER_1:51
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
theorem Th53: :: TOLER_1:53
theorem Th54: :: TOLER_1:54
theorem :: TOLER_1:55
canceled;
theorem :: TOLER_1:56
canceled;
theorem :: TOLER_1:57
canceled;
theorem :: TOLER_1:58
theorem :: TOLER_1:59
:: deftheorem TOLER_1:def 5 :
canceled;
:: deftheorem Def6 defines TolSets TOLER_1:def 6 :
:: deftheorem Def7 defines TolClasses TOLER_1:def 7 :
theorem :: TOLER_1:60
canceled;
theorem :: TOLER_1:61
canceled;
theorem :: TOLER_1:62
canceled;
theorem :: TOLER_1:63
canceled;
theorem :: TOLER_1:64
theorem :: TOLER_1:65
theorem :: TOLER_1:66
theorem :: TOLER_1:67
theorem :: TOLER_1:68
theorem :: TOLER_1:69
theorem :: TOLER_1:70
theorem :: TOLER_1:71
theorem :: TOLER_1:72
theorem :: TOLER_1:73
theorem :: TOLER_1:74