begin
theorem Th1:
:: deftheorem Def1 defines diagonal ROUGHS_1:def 1 :
theorem
Lm1:
for A being RelStr st A is reflexive & A is trivial holds
A is discrete
theorem
Lm2:
for A being RelStr st A is discrete holds
A is diagonal
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
begin
:: deftheorem Def2 defines with_equivalence ROUGHS_1:def 2 :
:: deftheorem Def3 defines with_tolerance ROUGHS_1:def 3 :
:: deftheorem defines LAp ROUGHS_1:def 4 :
:: deftheorem defines UAp ROUGHS_1:def 5 :
:: deftheorem defines BndAp ROUGHS_1:def 6 :
:: deftheorem Def7 defines rough ROUGHS_1:def 7 :
theorem Th8:
theorem
theorem Th10:
theorem
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem
theorem
theorem Th24:
theorem Th25:
theorem
theorem
theorem Th28:
theorem Th29:
theorem
theorem
theorem
theorem
theorem Th34:
theorem
theorem Th36:
theorem Th37:
:: deftheorem defines RoughSet ROUGHS_1:def 8 :
begin
definition
let A be
finite Tolerance_Space;
let X be
Subset of ;
func MemberFunc X,
A -> Function of the
carrier of
A,
REAL means :
Def9:
for
x being
Element of holds
it . x = (card (X /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x));
existence
ex b1 being Function of the carrier of A, REAL st
for x being Element of holds b1 . x = (card (X /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x))
uniqueness
for b1, b2 being Function of the carrier of A, REAL st ( for x being Element of holds b1 . x = (card (X /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x)) ) & ( for x being Element of holds b2 . x = (card (X /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x)) ) holds
b1 = b2
end;
:: deftheorem Def9 defines MemberFunc ROUGHS_1:def 9 :
theorem Th38:
theorem
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem
theorem
theorem
theorem Th47:
theorem
theorem
theorem
theorem Th51:
theorem
:: deftheorem Def10 defines FinSeqM ROUGHS_1:def 10 :
theorem Th53:
theorem Th54:
theorem
theorem
theorem
theorem
begin
:: deftheorem Def11 defines _c= ROUGHS_1:def 11 :
:: deftheorem Def12 defines c=^ ROUGHS_1:def 12 :
:: deftheorem Def13 defines _c=^ ROUGHS_1:def 13 :
theorem Th59:
theorem Th60:
theorem
begin
:: deftheorem Def14 defines _= ROUGHS_1:def 14 :
:: deftheorem Def15 defines =^ ROUGHS_1:def 15 :
:: deftheorem Def16 defines _=^ ROUGHS_1:def 16 :
:: deftheorem defines _= ROUGHS_1:def 17 :
:: deftheorem defines =^ ROUGHS_1:def 18 :
:: deftheorem defines _=^ ROUGHS_1:def 19 :