:: Properties of Binary Relations
:: by Edmund Woronowicz and Anna Zalewska
::
:: Received March 15, 1989
:: Copyright (c) 1990 Association of Mizar Users
definition
let R be
Relation;
let X be
set ;
pred R is_reflexive_in X means :
Def1:
:: RELAT_2:def 1
for
x being
set st
x in X holds
[x,x] in R;
pred R is_irreflexive_in X means :
Def2:
:: RELAT_2:def 2
for
x being
set st
x in X holds
not
[x,x] in R;
pred R is_symmetric_in X means :
Def3:
:: RELAT_2:def 3
for
x,
y being
set st
x in X &
y in X &
[x,y] in R holds
[y,x] in R;
pred R is_antisymmetric_in X means :
Def4:
:: RELAT_2:def 4
for
x,
y being
set st
x in X &
y in X &
[x,y] in R &
[y,x] in R holds
x = y;
pred R is_asymmetric_in X means :
Def5:
:: RELAT_2:def 5
for
x,
y being
set st
x in X &
y in X &
[x,y] in R holds
not
[y,x] in R;
pred R is_connected_in X means :
Def6:
:: RELAT_2:def 6
for
x,
y being
set st
x in X &
y in X &
x <> y & not
[x,y] in R holds
[y,x] in R;
pred R is_strongly_connected_in X means :
Def7:
:: RELAT_2:def 7
for
x,
y being
set st
x in X &
y in X & not
[x,y] in R holds
[y,x] in R;
pred R is_transitive_in X means :
Def8:
:: RELAT_2:def 8
for
x,
y,
z being
set st
x in X &
y in X &
z in X &
[x,y] in R &
[y,z] in R holds
[x,z] in R;
end;
:: deftheorem Def1 defines is_reflexive_in RELAT_2:def 1 :
:: deftheorem Def2 defines is_irreflexive_in RELAT_2:def 2 :
:: deftheorem Def3 defines is_symmetric_in RELAT_2:def 3 :
:: deftheorem Def4 defines is_antisymmetric_in RELAT_2:def 4 :
:: deftheorem Def5 defines is_asymmetric_in RELAT_2:def 5 :
:: deftheorem Def6 defines is_connected_in RELAT_2:def 6 :
:: deftheorem Def7 defines is_strongly_connected_in RELAT_2:def 7 :
:: deftheorem Def8 defines is_transitive_in RELAT_2:def 8 :
:: deftheorem Def9 defines reflexive RELAT_2:def 9 :
:: deftheorem Def10 defines irreflexive RELAT_2:def 10 :
:: deftheorem Def11 defines symmetric RELAT_2:def 11 :
:: deftheorem Def12 defines antisymmetric RELAT_2:def 12 :
:: deftheorem Def13 defines asymmetric RELAT_2:def 13 :
:: deftheorem Def14 defines connected RELAT_2:def 14 :
:: deftheorem Def15 defines strongly_connected RELAT_2:def 15 :
:: deftheorem Def16 defines transitive RELAT_2:def 16 :
theorem :: RELAT_2:1
canceled;
theorem :: RELAT_2:2
canceled;
theorem :: RELAT_2:3
canceled;
theorem :: RELAT_2:4
canceled;
theorem :: RELAT_2:5
canceled;
theorem :: RELAT_2:6
canceled;
theorem :: RELAT_2:7
canceled;
theorem :: RELAT_2:8
canceled;
theorem :: RELAT_2:9
canceled;
theorem :: RELAT_2:10
canceled;
theorem :: RELAT_2:11
canceled;
theorem :: RELAT_2:12
canceled;
theorem :: RELAT_2:13
canceled;
theorem :: RELAT_2:14
canceled;
theorem :: RELAT_2:15
canceled;
theorem :: RELAT_2:16
canceled;
theorem :: RELAT_2:17
theorem :: RELAT_2:18
theorem :: RELAT_2:19
theorem :: RELAT_2:20
theorem :: RELAT_2:21
canceled;
theorem Th22: :: RELAT_2:22
theorem Th23: :: RELAT_2:23
theorem :: RELAT_2:24
theorem :: RELAT_2:25
theorem :: RELAT_2:26
theorem Th27: :: RELAT_2:27
theorem :: RELAT_2:28
theorem :: RELAT_2:29
theorem Th30: :: RELAT_2:30
theorem :: RELAT_2:31
theorem :: RELAT_2:32
theorem :: RELAT_2:33
theorem :: RELAT_2:34
theorem :: RELAT_2:35
theorem :: RELAT_2:36
theorem :: RELAT_2:37
theorem :: RELAT_2:38
theorem :: RELAT_2:39
theorem :: RELAT_2:40
theorem :: RELAT_2:41
theorem :: RELAT_2:42
theorem :: RELAT_2:43
theorem :: RELAT_2:44
theorem :: RELAT_2:45
theorem :: RELAT_2:46
theorem :: RELAT_2:47
theorem :: RELAT_2:48