:: RELAT_2 semantic presentation
definition
let c1 be
Relation;
let c2 be
set ;
pred c1 is_reflexive_in c2 means :
Def1:
:: RELAT_2:def 1
for
b1 being
set st
b1 in a2 holds
[b1,b1] in a1;
pred c1 is_irreflexive_in c2 means :
Def2:
:: RELAT_2:def 2
for
b1 being
set st
b1 in a2 holds
not
[b1,b1] in a1;
pred c1 is_symmetric_in c2 means :
Def3:
:: RELAT_2:def 3
for
b1,
b2 being
set st
b1 in a2 &
b2 in a2 &
[b1,b2] in a1 holds
[b2,b1] in a1;
pred c1 is_antisymmetric_in c2 means :
Def4:
:: RELAT_2:def 4
for
b1,
b2 being
set st
b1 in a2 &
b2 in a2 &
[b1,b2] in a1 &
[b2,b1] in a1 holds
b1 = b2;
pred c1 is_asymmetric_in c2 means :
Def5:
:: RELAT_2:def 5
for
b1,
b2 being
set st
b1 in a2 &
b2 in a2 &
[b1,b2] in a1 holds
not
[b2,b1] in a1;
pred c1 is_connected_in c2 means :
Def6:
:: RELAT_2:def 6
for
b1,
b2 being
set st
b1 in a2 &
b2 in a2 &
b1 <> b2 & not
[b1,b2] in a1 holds
[b2,b1] in a1;
pred c1 is_strongly_connected_in c2 means :
Def7:
:: RELAT_2:def 7
for
b1,
b2 being
set st
b1 in a2 &
b2 in a2 & not
[b1,b2] in a1 holds
[b2,b1] in a1;
pred c1 is_transitive_in c2 means :
Def8:
:: RELAT_2:def 8
for
b1,
b2,
b3 being
set st
b1 in a2 &
b2 in a2 &
b3 in a2 &
[b1,b2] in a1 &
[b2,b3] in a1 holds
[b1,b3] in a1;
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 Th1: :: RELAT_2:1
canceled;
theorem Th2: :: RELAT_2:2
canceled;
theorem Th3: :: RELAT_2:3
canceled;
theorem Th4: :: RELAT_2:4
canceled;
theorem Th5: :: RELAT_2:5
canceled;
theorem Th6: :: RELAT_2:6
canceled;
theorem Th7: :: RELAT_2:7
canceled;
theorem Th8: :: RELAT_2:8
canceled;
theorem Th9: :: RELAT_2:9
canceled;
theorem Th10: :: RELAT_2:10
canceled;
theorem Th11: :: RELAT_2:11
canceled;
theorem Th12: :: RELAT_2:12
canceled;
theorem Th13: :: RELAT_2:13
canceled;
theorem Th14: :: RELAT_2:14
canceled;
theorem Th15: :: RELAT_2:15
canceled;
theorem Th16: :: RELAT_2:16
canceled;
theorem Th17: :: RELAT_2:17
theorem Th18: :: RELAT_2:18
theorem Th19: :: RELAT_2:19
theorem Th20: :: RELAT_2:20
theorem Th21: :: RELAT_2:21
canceled;
theorem Th22: :: RELAT_2:22
theorem Th23: :: RELAT_2:23
theorem Th24: :: RELAT_2:24
theorem Th25: :: RELAT_2:25
theorem Th26: :: RELAT_2:26
theorem Th27: :: RELAT_2:27
theorem Th28: :: RELAT_2:28
theorem Th29: :: RELAT_2:29
theorem Th30: :: RELAT_2:30
theorem Th31: :: RELAT_2:31
theorem Th32: :: RELAT_2:32
theorem Th33: :: RELAT_2:33
theorem Th34: :: RELAT_2:34
theorem Th35: :: RELAT_2:35
theorem Th36: :: RELAT_2:36
theorem Th37: :: RELAT_2:37
theorem Th38: :: RELAT_2:38
theorem Th39: :: RELAT_2:39
theorem Th40: :: RELAT_2:40
theorem Th41: :: RELAT_2:41
theorem Th42: :: RELAT_2:42
theorem Th43: :: RELAT_2:43
theorem Th44: :: RELAT_2:44
theorem Th45: :: RELAT_2:45
theorem Th46: :: RELAT_2:46
theorem Th47: :: RELAT_2:47