:: Basic Properties of Rough Sets and Rough Membership Function
:: by Adam Grabowski
::
:: Received November 23, 2003
:: Copyright (c) 2003 Association of Mizar Users
theorem Th1: :: ROUGHS_1:1
:: deftheorem Def1 defines diagonal ROUGHS_1:def 1 :
theorem :: ROUGHS_1:2
Lm1:
for A being RelStr st A is reflexive & A is trivial holds
A is discrete
theorem :: ROUGHS_1:3
Lm2:
for A being RelStr st A is discrete holds
A is diagonal
theorem Th4: :: ROUGHS_1:4
theorem Th5: :: ROUGHS_1:5
theorem Th6: :: ROUGHS_1:6
theorem Th7: :: ROUGHS_1:7
:: 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: :: ROUGHS_1:8
theorem :: ROUGHS_1:9
theorem Th10: :: ROUGHS_1:10
theorem :: ROUGHS_1:11
theorem Th12: :: ROUGHS_1:12
theorem Th13: :: ROUGHS_1:13
theorem Th14: :: ROUGHS_1:14
theorem Th15: :: ROUGHS_1:15
theorem Th16: :: ROUGHS_1:16
theorem :: ROUGHS_1:17
theorem Th18: :: ROUGHS_1:18
theorem Th19: :: ROUGHS_1:19
theorem Th20: :: ROUGHS_1:20
theorem :: ROUGHS_1:21
theorem :: ROUGHS_1:22
theorem :: ROUGHS_1:23
theorem Th24: :: ROUGHS_1:24
theorem Th25: :: ROUGHS_1:25
theorem :: ROUGHS_1:26
theorem :: ROUGHS_1:27
theorem Th28: :: ROUGHS_1:28
theorem Th29: :: ROUGHS_1:29
theorem :: ROUGHS_1:30
theorem :: ROUGHS_1:31
theorem :: ROUGHS_1:32
theorem :: ROUGHS_1:33
theorem Th34: :: ROUGHS_1:34
theorem :: ROUGHS_1:35
theorem Th36: :: ROUGHS_1:36
theorem Th37: :: ROUGHS_1:37
:: deftheorem defines RoughSet ROUGHS_1:def 8 :
definition
let A be
finite Tolerance_Space;
let X be
Subset of
A;
func MemberFunc X,
A -> Function of the
carrier of
A,
REAL means :
Def9:
:: ROUGHS_1:def 9
for
x being
Element of
A 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 A 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 A holds b1 . x = (card (X /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x)) ) & ( for x being Element of A 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: :: ROUGHS_1:38
theorem :: ROUGHS_1:39
theorem Th40: :: ROUGHS_1:40
theorem Th41: :: ROUGHS_1:41
theorem Th42: :: ROUGHS_1:42
theorem Th43: :: ROUGHS_1:43
theorem :: ROUGHS_1:44
theorem :: ROUGHS_1:45
theorem :: ROUGHS_1:46
theorem Th47: :: ROUGHS_1:47
theorem :: ROUGHS_1:48
theorem :: ROUGHS_1:49
theorem :: ROUGHS_1:50
theorem Th51: :: ROUGHS_1:51
theorem :: ROUGHS_1:52
:: deftheorem Def10 defines FinSeqM ROUGHS_1:def 10 :
theorem Th53: :: ROUGHS_1:53
theorem Th54: :: ROUGHS_1:54
theorem :: ROUGHS_1:55
theorem :: ROUGHS_1:56
theorem :: ROUGHS_1:57
theorem :: ROUGHS_1:58
:: 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: :: ROUGHS_1:59
theorem Th60: :: ROUGHS_1:60
theorem :: ROUGHS_1:61
:: 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 :