:: Basic Properties of Rough Sets and Rough Membership Function
:: by Adam Grabowski
::
:: Received November 23, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ORDERS_2, RELAT_1, NATTRA_1, TOLER_1, TARSKI, ZFMISC_1,
MATRIX_1, STRUCT_0, RELAT_2, XBOOLE_0, PARTFUN1, SUBSET_1, FINSEQ_1,
CARD_3, ORDINAL4, FUNCT_1, PROB_2, FINSEQ_2, NAT_1, FINSET_1, EQREL_1,
CARD_1, ARYTM_3, XXREAL_0, XXREAL_1, FUNCT_3, ARYTM_1, ROUGHS_1, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, XXREAL_0, FINSET_1, RELAT_1, RELAT_2, FUNCT_1, FINSEQ_1,
RVSUM_1, FINSEQ_2, RELSET_1, PARTFUN1, CARD_3, PROB_2, FUNCT_2, FUNCT_3,
DOMAIN_1, STRUCT_0, ORDERS_2, EQREL_1, RCOMP_1, TOLER_1, ORDERS_3;
constructors EQREL_1, PROB_2, RCOMP_1, RVSUM_1, FUNCT_6, REALSET2, ORDERS_3,
RELSET_1, BINOP_2, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, PARTFUN1, FINSET_1, NUMBERS,
XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, EQREL_1, STRUCT_0,
ORDERS_2, VALUED_0, CARD_1, RELSET_1;
requirements BOOLE, SUBSET, NUMERALS, REAL;
definitions TARSKI, XBOOLE_0, PROB_2;
equalities FINSEQ_2, SUBSET_1, CARD_3, STRUCT_0, ORDINAL1;
expansions TARSKI, XBOOLE_0, PROB_2;
theorems EQREL_1, XBOOLE_0, XBOOLE_1, SUBSET_1, XCMPLX_1, CARD_2, TOLER_1,
NAT_1, TARSKI, ZFMISC_1, RELAT_1, RELAT_2, ORDERS_3, CHAIN_1, FUNCT_2,
FUNCT_3, RVSUM_1, FINSEQ_1, FINSEQ_3, FUNCT_1, GRFUNC_1, FINSEQ_6,
FINSEQ_2, ORDERS_2, SYSREL, FUNCOP_1, ORDERS_1, XREAL_0, ORDINAL1,
XXREAL_1, XREAL_1, XXREAL_0, PARTFUN1, RELSET_1, FUNCT_4;
schemes FUNCT_2, BINOP_2, FINSEQ_2;
begin :: Preliminaries
registration
let A be set;
cluster RelStr (# A, id A #) -> discrete;
coherence by ORDERS_3:def 1;
end;
theorem Th1:
for X being set st Total X c= id X holds X is trivial
proof
let X be set;
assume
A1: Total X c= id X;
assume X is non trivial;
then consider x, y being object such that
A2: x in X & y in X and
A3: x <> y by ZFMISC_1:def 10;
[x,y] in Total X by A2,TOLER_1:2;
hence thesis by A1,A3,RELAT_1:def 10;
end;
definition
let A be RelStr;
attr A is diagonal means
:Def1:
the InternalRel of A c= id the carrier of A;
end;
registration
let A be non trivial set;
cluster RelStr (# A, Total A #) -> non diagonal;
coherence by Th1;
end;
theorem
for L being reflexive RelStr holds
id the carrier of L c= the InternalRel of L
proof
let L be reflexive RelStr;
for a,b being object st [a,b] in id the carrier of L holds [a,b] in the
InternalRel of L
proof
let a,b be object;
assume [a,b] in id the carrier of L;
then
A1: a = b & a in the carrier of L by RELAT_1:def 10;
the InternalRel of L is_reflexive_in the carrier of L by ORDERS_2:def 2;
hence thesis by A1,RELAT_2:def 1;
end;
hence thesis by RELAT_1:def 3;
end;
Lm1: for A being RelStr st A is reflexive trivial holds A is discrete
proof
let A be RelStr;
assume
A1: A is reflexive trivial;
per cases by A1,ZFMISC_1:131;
suppose
A2: the carrier of A is empty;
then the InternalRel of A = {};
hence thesis by A2,ORDERS_3:def 1,RELAT_1:55;
end;
suppose
ex x being object st the carrier of A = {x};
then consider x being object such that
A3: the carrier of A = {x};
the InternalRel of A c= [:{x}, {x}:] by A3;
then the InternalRel of A c= { [x, x] } by ZFMISC_1:29;
then
A4: the InternalRel of A = { [x, x] } or the InternalRel of A = {}
by ZFMISC_1:33;
A5: the InternalRel of A is_reflexive_in the carrier of A by A1,ORDERS_2:def 2;
x in the carrier of A by A3,TARSKI:def 1;
then the InternalRel of A = id {x} by A4,A5,RELAT_2:def 1,SYSREL:13;
hence thesis by A3,ORDERS_3:def 1;
end;
end;
registration
cluster non discrete -> non trivial for reflexive RelStr;
coherence by Lm1;
cluster reflexive trivial -> discrete for RelStr;
coherence;
end;
theorem
for X being set, R being Relation of X
holds R is total reflexive iff id X c= R
proof
let X be set, R be Relation of X;
hereby
assume R is total reflexive;
then A1: dom R = X & id field R c= R by PARTFUN1:def 2, RELAT_2:1;
then field R = X \/ rng R by RELAT_1:def 6;
hence id X c= R by A1, XBOOLE_1:12;
end;
assume A2: id X c= R;
field R c= X \/ X by RELSET_1:8;
then id field R c= id X by FUNCT_4:3;
then A3: id field R c= R by A2;
dom id X c= dom R by A2, RELAT_1:11;
hence thesis by A3, XBOOLE_0:def 10, RELAT_2:1, PARTFUN1:def 2;
end;
Lm2: for A being RelStr st A is discrete holds A is diagonal
by ORDERS_3:def 1;
registration
cluster discrete -> diagonal for RelStr;
coherence by Lm2;
cluster non diagonal -> non discrete for RelStr;
coherence;
end;
registration
cluster non diagonal non empty for RelStr;
existence
proof
set A = the non trivial set;
take RelStr (# A, Total A #);
thus thesis;
end;
end;
theorem Th4:
for A being non diagonal non empty RelStr ex x, y being Element of A st
x <> y & [x,y] in the InternalRel of A
proof
let A be non diagonal non empty RelStr;
now
assume
A1: for x,y being Element of A st [x,y] in the InternalRel of A holds x = y;
for a,b being object st [a,b] in the InternalRel of A holds [a,b] in id
the carrier of A
proof
let a,b be object;
assume
A2: [a,b] in the InternalRel of A;
then
A3: a is Element of A by ZFMISC_1:87;
b is Element of A by A2,ZFMISC_1:87;
then a = b by A1,A2,A3;
hence thesis by A3,RELAT_1:def 10;
end;
then the InternalRel of A c= id the carrier of A by RELAT_1:def 3;
hence thesis by Def1;
end;
hence thesis;
end;
theorem Th5:
for D being set, p, q being FinSequence of D holds
Union (p^q) = Union p \/ Union q
proof
let D be set, p, q be FinSequence of D;
union rng(p^q) = union (rng p \/ rng q) by FINSEQ_1:31
.= Union p \/ Union q by ZFMISC_1:78;
hence thesis;
end;
theorem Th6:
for p, q being Function st q is disjoint_valued & p c= q holds
p is disjoint_valued
proof
let p, q be Function;
assume that
A1: q is disjoint_valued and
A2: p c= q;
for x, y being object st x <> y holds p.x misses p.y
proof
let x, y be object;
assume
A3: x <> y;
assume
A4: p.x meets p.y;
x in dom p & y in dom p
proof
assume not x in dom p or not y in dom p;
then p.x = {} or p.y = {} by FUNCT_1:def 2;
hence thesis by A4;
end;
then p.x = q.x & p.y = q.y by A2,GRFUNC_1:2;
hence thesis by A1,A3,A4;
end;
hence thesis;
end;
registration
cluster empty -> disjoint_valued for Function;
coherence
proof
let X be Function;
assume
A1: X is empty;
let x, y be object;
assume x <> y;
X.x = {} by A1,FUNCT_1:def 2,RELAT_1:38;
hence thesis;
end;
end;
registration
let A be set;
cluster disjoint_valued for FinSequence of A;
existence
proof
set X = <*>A;
X is disjoint_valued;
hence thesis;
end;
end;
registration
let A be non empty set;
cluster non empty disjoint_valued for FinSequence of A;
existence
proof
set a = the Element of A;
reconsider X = 1 |-> a as FinSequence of A;
A1: X is disjoint_valued
proof
let x, y be object;
assume
A2: x <> y;
per cases;
suppose
A3: x in dom X & y in dom X;
then x in Seg 1 by FUNCOP_1:13;
then
A4: x = 1 by FINSEQ_1:2,TARSKI:def 1;
y in Seg 1 by A3,FUNCOP_1:13;
hence thesis by A2,A4,FINSEQ_1:2,TARSKI:def 1;
end;
suppose
not x in dom X or not y in dom X;
then X.x = {} or X.y = {} by FUNCT_1:def 2;
hence thesis;
end;
end;
X is non empty by FUNCOP_1:13,RELAT_1:38;
hence thesis by A1;
end;
end;
definition
let A be set;
let X be FinSequence of bool A;
let n be Nat;
redefine func X.n -> Subset of A; :: redefines . (FUNCT_1, definition)
coherence
proof
per cases;
suppose
not n in dom X;
then X.n = {} by FUNCT_1:def 2;
hence thesis by XBOOLE_1:2;
end;
suppose
n in dom X;
hence thesis by FINSEQ_2:11;
end;
end;
end;
definition
let A be set;
let X be FinSequence of bool A;
redefine func Union X -> Subset of A; :: redefines Union (CARD_3, definition)
coherence
proof
union rng X c= A
proof
let x be object;
assume x in union rng X;
then ex Y being set st x in Y & Y in rng X by TARSKI:def 4;
hence thesis;
end;
hence thesis;
end;
end;
registration
let A be finite set;
let R be Relation of A;
cluster RelStr (# A, R #) -> finite;
coherence;
end;
theorem Th7:
for X being set, x, y being object, T being Tolerance of X
st x in Class (T, y) holds y in Class (T, x)
proof
let X be set, x, y be object, T be Tolerance of X;
assume x in Class (T, y);
then [x,y] in T by EQREL_1:19;
then [y,x] in T by EQREL_1:6;
hence thesis by EQREL_1:19;
end;
begin :: Tolerance and Approximation Spaces
definition
let P be RelStr;
attr P is with_equivalence means :Def2:
the InternalRel of P is Equivalence_Relation of the carrier of P;
attr P is with_tolerance means :Def3:
the InternalRel of P is Tolerance of the carrier of P;
end;
registration
cluster with_equivalence -> with_tolerance for RelStr;
coherence;
end;
registration
let A be set;
cluster RelStr (# A, id A #) -> with_equivalence;
coherence;
end;
registration
cluster discrete finite with_equivalence non empty for RelStr;
existence
proof
set E = RelStr (# {{}}, id {{}} #);
E is discrete;
hence thesis;
end;
cluster non diagonal finite with_equivalence non empty for RelStr;
existence
proof
set C = {0,1};
set R = Total C;
set E = RelStr (# C, R #);
reconsider E as non empty RelStr;
E is with_equivalence & C is non trivial by CHAIN_1:3;
hence thesis;
end;
end;
definition
mode Approximation_Space is with_equivalence non empty RelStr;
mode Tolerance_Space is with_tolerance non empty RelStr;
end;
registration
let A be Tolerance_Space;
cluster the InternalRel of A -> total reflexive symmetric;
coherence by Def3;
end;
registration
let A be Approximation_Space;
cluster the InternalRel of A -> transitive;
coherence by Def2;
end;
definition
let A be non empty RelStr;
let X be Subset of A;
func LAp X -> Subset of A equals
{ x where x is Element of A : Class (the InternalRel of A, x) c= X };
coherence
proof
{ x where x is Element of A : Class (the InternalRel of A, x) c= X }
c= the carrier of A
proof
let y be object;
assume y in { x where x is Element of A : Class (the InternalRel of A,
x) c= X };
then
ex x being Element of A st y = x & Class (the InternalRel of A, x) c= X;
hence thesis;
end;
hence thesis;
end;
func UAp X -> Subset of A equals
{ x where x is Element of A : Class (the InternalRel of A, x) meets X };
coherence
proof
{ x where x is Element of A : Class (the InternalRel of A, x) meets X }
c= the carrier of A
proof
let y be object;
assume y in { x where x is Element of A : Class (the InternalRel of A,
x) meets X };
then ex x being Element of A st y = x & Class (the InternalRel of A, x)
meets X;
hence thesis;
end;
hence thesis;
end;
end;
definition
let A be non empty RelStr;
let X be Subset of A;
func BndAp X -> Subset of A equals
UAp X \ LAp X;
coherence;
end;
definition
let A be non empty RelStr;
let X be Subset of A;
attr X is rough means
BndAp X <> {};
end;
notation
let A be non empty RelStr;
let X be Subset of A;
antonym X is exact for X is rough;
end;
reserve A for Tolerance_Space,
X, Y for Subset of A;
theorem Th8:
for x being object st x in LAp X holds Class (the InternalRel of A, x) c= X
proof
let x be object;
assume x in LAp X;
then
ex x1 being Element of A st x = x1 & Class (the InternalRel of A, x1) c= X;
hence thesis;
end;
theorem
for x being Element of A st Class (the InternalRel of A, x) c= X holds
x in LAp X;
theorem Th10:
for x being set st x in UAp X holds Class (the InternalRel of A, x) meets X
proof
let x be set;
assume x in UAp X;
then ex x1 being Element of A st x = x1 & Class (the InternalRel of A, x1)
meets X;
hence thesis;
end;
theorem
for x being Element of A st Class (the InternalRel of A, x) meets X
holds x in UAp X;
theorem Th12:
LAp X c= X
proof
let x be object;
assume x in LAp X;
then consider y being Element of A such that
A1: y = x & Class (the InternalRel of A, y) c= X;
y in Class (the InternalRel of A, y) by EQREL_1:20;
hence thesis by A1;
end;
theorem Th13:
X c= UAp X
proof
let x be object;
assume
A1: x in X;
then reconsider x9 = x as Element of A;
x9 in Class (the InternalRel of A, x9) by EQREL_1:20;
then Class (the InternalRel of A, x9) meets X by A1,XBOOLE_0:3;
hence thesis;
end;
theorem Th14:
LAp X c= UAp X
proof
LAp X c= X & X c= UAp X by Th12,Th13;
hence thesis;
end;
theorem Th15:
X is exact iff LAp X = X
proof
A1: LAp X c= UAp X by Th14;
hereby
assume X is exact;
then BndAp X = {};
then UAp X c= LAp X by XBOOLE_1:37;
then UAp X = LAp X by A1;
then
A2: X c= LAp X by Th13;
LAp X c= X by Th12;
hence LAp X = X by A2;
end;
assume
A3: LAp X = X;
UAp X c= X
proof
let y be object;
assume y in UAp X;
then Class (the InternalRel of A, y) meets X by Th10;
then consider z being object such that
A4: z in Class (the InternalRel of A, y) & z in LAp X by A3,XBOOLE_0:3;
Class (the InternalRel of A, z) c= X & y in Class (the InternalRel of
A, z) by A4,Th7,Th8;
hence thesis;
end;
then BndAp X = {} by A3,XBOOLE_1:37;
hence thesis;
end;
theorem Th16:
X is exact iff UAp X = X
proof
hereby
assume X is exact;
then BndAp X = {};
then
A1: UAp X c= LAp X by XBOOLE_1:37;
A2: X c= UAp X by Th13;
LAp X c= X by Th12;
then UAp X c= X by A1;
hence UAp X = X by A2;
end;
assume
A3: UAp X = X;
X c= LAp X
proof
let x be object;
assume
A4: x in X;
Class (the InternalRel of A, x) c= X
proof
let y be object;
assume
A5: y in Class (the InternalRel of A, x);
then [y,x] in the InternalRel of A by EQREL_1:19;
then [x,y] in the InternalRel of A by EQREL_1:6;
then x in Class (the InternalRel of A, y) by EQREL_1:19;
then Class (the InternalRel of A, y) meets X by A4,XBOOLE_0:3;
hence thesis by A3,A5;
end;
hence thesis by A4;
end;
then BndAp X = {} by A3,XBOOLE_1:37;
hence thesis;
end;
theorem
X = LAp X iff X = UAp X
by Th15,Th16;
theorem Th18:
LAp {}A = {}
proof
assume LAp {}A <> {};
then consider x being object such that
A1: x in LAp {}A by XBOOLE_0:def 1;
ex y being Element of A st y = x & Class (the InternalRel of A, y) c= {}A
by A1;
hence thesis by EQREL_1:20;
end;
theorem Th19:
UAp {}A = {}
proof
assume UAp {}A <> {};
then consider x being object such that
A1: x in UAp {}A by XBOOLE_0:def 1;
ex y being Element of A st y = x & Class (the InternalRel of A, y) meets
{}A by A1;
hence thesis;
end;
theorem Th20:
LAp [#]A = [#]A
proof
thus LAp [#]A c= [#]A;
let x be object;
A1: Class (the InternalRel of A, x) c= [#]A;
assume x in [#]A;
hence thesis by A1;
end;
theorem
UAp [#]A = [#]A
proof
LAp [#]A c= UAp [#]A by Th14;
then [#]A c= UAp [#]A by Th20;
hence thesis;
end;
theorem
LAp (X /\ Y) = LAp X /\ LAp Y
proof
thus LAp (X /\ Y) c= LAp X /\ LAp Y
proof
let x be object;
assume
A1: x in LAp (X /\ Y);
then Class (the InternalRel of A, x) c= Y by Th8,XBOOLE_1:18;
then
A2: x in LAp Y by A1;
Class (the InternalRel of A, x) c= X by A1,Th8,XBOOLE_1:18;
then x in LAp X by A1;
hence thesis by A2,XBOOLE_0:def 4;
end;
let x be object;
assume
A3: x in LAp X /\ LAp Y;
then x in LAp Y by XBOOLE_0:def 4;
then
A4: Class (the InternalRel of A, x) c= Y by Th8;
x in LAp X by A3,XBOOLE_0:def 4;
then Class (the InternalRel of A, x) c= X by Th8;
then Class (the InternalRel of A, x) c= X /\ Y by A4,XBOOLE_1:19;
hence thesis by A3;
end;
theorem
UAp (X \/ Y) = UAp X \/ UAp Y
proof
thus UAp (X \/ Y) c= UAp X \/ UAp Y
proof
let x be object;
assume
A1: x in UAp (X \/ Y);
then Class (the InternalRel of A, x) meets (X \/ Y) by Th10; then
Class (the InternalRel of A, x) meets X or
Class (the InternalRel of A, x) meets Y by XBOOLE_1:70;
then x in UAp X or x in UAp Y by A1;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume
A2: x in UAp X \/ UAp Y;
then x in UAp X or x in UAp Y by XBOOLE_0:def 3;
then
Class (the InternalRel of A, x) meets X or Class (the InternalRel of A,
x) meets Y by Th10;
then Class (the InternalRel of A, x) meets (X \/ Y) by XBOOLE_1:70;
hence thesis by A2;
end;
theorem Th24:
X c= Y implies LAp X c= LAp Y
proof
assume
A1: X c= Y;
let x be object;
assume
A2: x in LAp X;
then Class (the InternalRel of A, x) c= X by Th8;
then Class (the InternalRel of A, x) c= Y by A1;
hence thesis by A2;
end;
theorem Th25:
X c= Y implies UAp X c= UAp Y
proof
assume
A1: X c= Y;
let x be object;
assume
A2: x in UAp X;
then Class (the InternalRel of A, x) meets X by Th10;
then Class (the InternalRel of A, x) meets Y by A1,XBOOLE_1:63;
hence thesis by A2;
end;
theorem
LAp X \/ LAp Y c= LAp (X \/ Y)
proof
let x be object;
assume
A1: x in LAp X \/ LAp Y;
per cases by A1,XBOOLE_0:def 3;
suppose
x in LAp X;
then Class (the InternalRel of A, x) c= X \/ Y by Th8,XBOOLE_1:10;
hence thesis by A1;
end;
suppose
x in LAp Y;
then Class (the InternalRel of A, x) c= X \/ Y by Th8,XBOOLE_1:10;
hence thesis by A1;
end;
end;
theorem
UAp (X /\ Y) c= UAp X /\ UAp Y
proof
let x be object;
assume
A1: x in UAp (X /\ Y);
then Class (the InternalRel of A, x) meets Y by Th10,XBOOLE_1:74;
then
A2: x in UAp Y by A1;
Class (the InternalRel of A, x) meets X by A1,Th10,XBOOLE_1:74;
then x in UAp X by A1;
hence thesis by A2,XBOOLE_0:def 4;
end;
theorem Th28:
LAp X` = (UAp X)`
proof
LAp X` misses UAp X
proof
assume LAp X` meets UAp X;
then consider x being object such that
A1: x in LAp X` & x in UAp X by XBOOLE_0:3;
Class (the InternalRel of A, x) meets X & Class (the InternalRel of A,
x) c= X` by A1,Th8,Th10;
hence thesis by XBOOLE_1:63,79;
end;
hence LAp X` c= (UAp X)` by SUBSET_1:23;
let x be object;
assume
A2: x in (UAp X)`;
then not x in UAp X by XBOOLE_0:def 5;
then Class (the InternalRel of A, x) misses X by A2;
then Class (the InternalRel of A, x) c= X` by SUBSET_1:23;
hence thesis by A2;
end;
theorem Th29:
UAp X` = (LAp X)`
proof
(UAp X`)`` = (LAp X``)` by Th28;
hence thesis;
end;
theorem
UAp LAp UAp X = UAp X
proof
thus UAp LAp UAp X c= UAp X
proof
let x be object;
assume x in UAp LAp UAp X;
then Class (the InternalRel of A, x) meets LAp UAp X by Th10;
then consider y being object such that
A1: y in Class (the InternalRel of A, x) and
A2: y in LAp UAp X by XBOOLE_0:3;
[y, x] in the InternalRel of A by A1,EQREL_1:19;
then [x, y] in the InternalRel of A by EQREL_1:6;
then
A3: x in Class (the InternalRel of A, y) by EQREL_1:19;
Class (the InternalRel of A, y) c= UAp X by A2,Th8;
hence thesis by A3;
end;
X c= LAp UAp X
proof
let x be object;
assume
A4: x in X;
Class (the InternalRel of A, x) c= UAp X
proof
let y be object;
assume
A5: y in Class (the InternalRel of A, x);
then [y,x] in the InternalRel of A by EQREL_1:19;
then [x,y] in the InternalRel of A by EQREL_1:6;
then x in Class (the InternalRel of A, y) by EQREL_1:19;
then Class (the InternalRel of A, y) meets X by A4,XBOOLE_0:3;
hence thesis by A5;
end;
hence thesis by A4;
end;
hence UAp X c= UAp LAp UAp X by Th25;
end;
theorem
LAp UAp LAp X = LAp X
proof
UAp LAp X c= X
proof
let y be object;
assume y in UAp LAp X;
then Class (the InternalRel of A, y) meets LAp X by Th10;
then consider z being object such that
A1: z in Class (the InternalRel of A, y) and
A2: z in LAp X by XBOOLE_0:3;
[z,y] in the InternalRel of A by A1,EQREL_1:19;
then [y,z] in the InternalRel of A by EQREL_1:6;
then
A3: y in Class (the InternalRel of A, z) by EQREL_1:19;
Class (the InternalRel of A, z) c= X by A2,Th8;
hence thesis by A3;
end;
hence LAp UAp LAp X c= LAp X by Th24;
thus LAp X c= LAp UAp LAp X
proof
let x be object;
assume
A4: x in LAp X;
Class (the InternalRel of A, x) c= UAp LAp X
proof
let y be object;
assume
A5: y in Class (the InternalRel of A, x);
then [y,x] in the InternalRel of A by EQREL_1:19;
then [x,y] in the InternalRel of A by EQREL_1:6;
then x in Class (the InternalRel of A, y) by EQREL_1:19;
then Class (the InternalRel of A, y) meets LAp X by A4,XBOOLE_0:3;
hence thesis by A5;
end;
hence thesis by A4;
end;
end;
theorem
BndAp X = BndAp X`
proof
thus BndAp X c= BndAp X`
proof
let x be object;
assume
A1: x in BndAp X;
then x in UAp X by XBOOLE_0:def 5;
then not x in (UAp X)` by XBOOLE_0:def 5;
then
A2: not x in LAp X` by Th28;
not x in LAp X by A1,XBOOLE_0:def 5;
then x in (LAp X)` by A1,XBOOLE_0:def 5;
then x in UAp X` by Th29;
hence thesis by A2,XBOOLE_0:def 5;
end;
thus BndAp X` c= BndAp X
proof
let x be object;
assume
A3: x in BndAp X`;
then x in UAp X` by XBOOLE_0:def 5;
then x in (LAp X)` by Th29;
then
A4: not x in LAp X by XBOOLE_0:def 5;
not x in LAp X` by A3,XBOOLE_0:def 5;
then not x in (UAp X)` by Th28;
then x in (UAp X)`` by A3,SUBSET_1:29;
hence thesis by A4,XBOOLE_0:def 5;
end;
end;
reserve A for Approximation_Space,
X for Subset of A;
theorem
LAp LAp X = LAp X
proof
thus LAp LAp X c= LAp X by Th12;
let x be object;
assume
A1: x in LAp X;
then
A2: Class (the InternalRel of A, x) c= X by Th8;
Class (the InternalRel of A, x) c= LAp X
proof
let y be object;
assume
A3: y in Class (the InternalRel of A, x);
then Class (the InternalRel of A, x) = Class (the InternalRel of A, y)
by A1,EQREL_1:23;
hence thesis by A2,A3;
end;
hence thesis by A1;
end;
theorem Th34:
LAp LAp X = UAp LAp X
proof
thus LAp LAp X c= UAp LAp X by Th14;
let x be object;
assume
A1: x in UAp LAp X;
then Class (the InternalRel of A, x) meets LAp X by Th10;
then consider z being object such that
A2: z in Class (the InternalRel of A, x) and
A3: z in LAp X by XBOOLE_0:3;
Class (the InternalRel of A, z) c= X by A3,Th8;
then
A4: Class (the InternalRel of A, x) c= X by A1,A2,EQREL_1:23;
Class (the InternalRel of A, x) c= LAp X
proof
let y be object;
assume
A5: y in Class (the InternalRel of A, x);
then Class (the InternalRel of A, x) = Class (the InternalRel of A, y) by
A1,EQREL_1:23;
hence thesis by A4,A5;
end;
hence thesis by A1;
end;
theorem
UAp UAp X = UAp X
proof
hereby
let x be object;
assume
A1: x in UAp UAp X;
then Class (the InternalRel of A, x) meets UAp X by Th10;
then consider y being object such that
A2: y in Class (the InternalRel of A, x) and
A3: y in UAp X by XBOOLE_0:3;
A4: Class (the InternalRel of A, y) = Class (the InternalRel of A, x)
by A1,A2,EQREL_1:23;
Class (the InternalRel of A, y) meets X by A3,Th10;
hence x in UAp X by A1,A4;
end;
thus thesis by Th13;
end;
theorem Th36:
UAp UAp X = LAp UAp X
proof
thus UAp UAp X c= LAp UAp X
proof
let x be object;
assume
A1: x in UAp UAp X;
then Class (the InternalRel of A, x) meets UAp X by Th10;
then consider z being object such that
A2: z in Class (the InternalRel of A, x) and
A3: z in UAp X by XBOOLE_0:3;
A4: Class (the InternalRel of A, z) = Class (the InternalRel of A, x)
by A1,A2,EQREL_1:23;
A5: Class (the InternalRel of A, z) meets X by A3,Th10;
Class (the InternalRel of A, x) c= UAp X
proof
let y be object;
assume
A6: y in Class (the InternalRel of A, x); then
Class (the InternalRel of A, x) = Class (the InternalRel of A, y)
by A1,EQREL_1:23;
hence thesis by A5,A4,A6;
end;
hence thesis by A1;
end;
thus thesis by Th14;
end;
registration
let A be Tolerance_Space;
cluster exact for Subset of A;
existence
proof
take {}A;
LAp {}A = {} by Th18;
hence thesis by Th15;
end;
end;
registration
let A be Approximation_Space;
let X be Subset of A;
cluster LAp X -> exact;
coherence
proof
set Y = LAp X;
UAp Y = LAp Y by Th34;
then BndAp Y = {} by XBOOLE_1:37;
hence thesis;
end;
cluster UAp X -> exact;
coherence
proof
set Y = UAp X;
UAp Y = LAp Y by Th36;
then BndAp Y = {} by XBOOLE_1:37;
hence thesis;
end;
end;
theorem Th37:
for A being Approximation_Space, X being Subset of A, x, y being
set st x in UAp X & [x,y] in the InternalRel of A holds y in UAp X
proof
let A be Approximation_Space, X be Subset of A;
let x, y be set;
assume that
A1: x in UAp X and
A2: [x,y] in the InternalRel of A;
[y,x] in the InternalRel of A by A2,EQREL_1:6;
then y in Class (the InternalRel of A, x) by EQREL_1:19;
then
A3: Class (the InternalRel of A, x) = Class (the InternalRel of A, y) by A1,
EQREL_1:23;
Class (the InternalRel of A, x) meets X & y is Element of A by A1,A2,Th10,
ZFMISC_1:87;
hence thesis by A3;
end;
registration
let A be non diagonal Approximation_Space;
cluster rough for Subset of A;
existence
proof
consider x, y being Element of A such that
A1: x <> y and
A2: [x,y] in the InternalRel of A by Th4;
set X = {x};
x in X & X c= UAp X by Th13,TARSKI:def 1;
then y in UAp X by A2,Th37;
then UAp X <> X by A1,TARSKI:def 1;
then X is not exact by Th16;
hence thesis;
end;
end;
definition
let A be Approximation_Space;
let X be Subset of A;
mode RoughSet of X -> set means
it = [LAp X, UAp X];
existence;
end;
begin :: Membership Function
registration
let A be finite Tolerance_Space, x be Element of A;
cluster card Class (the InternalRel of A, x) -> non empty;
coherence
proof
x in Class (the InternalRel of A, x) by EQREL_1:20;
hence thesis;
end;
end;
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:
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
proof
deffunc F(object) = card (X /\ Class (the InternalRel of A, $1)) / (card
Class (the InternalRel of A, $1));
A1: for x being object st x in the carrier of A holds F(x) in REAL by
XREAL_0:def 1;
consider f being Function of the carrier of A, REAL such that
A2: for x being object st x in the carrier of A holds f.x = F(x)
from FUNCT_2:sch 2(A1);
take f;
let x be Element of A;
thus thesis by A2;
end;
uniqueness
proof
deffunc F(Element of A) = card (X /\ Class (the InternalRel of A, $1)) / (
card Class (the InternalRel of A, $1));
A3: for A1,A2 being Function of the carrier of A, REAL st (for x being
Element of A holds A1.x = F(x)) & (for x being Element of A holds A2.x = F(x))
holds A1 = A2 from BINOP_2:sch 1;
let A1, A2 be Function of the carrier of A, REAL;
assume ( for x being Element of A holds A1.x = F(x))& for x being Element
of A holds A2.x = F(x);
hence A1 = A2 by A3;
end;
end;
reserve A for finite Tolerance_Space,
X for Subset of A,
x for Element of A;
theorem Th38:
0 <= MemberFunc (X, A).x & MemberFunc (X, A).x <= 1
proof
card (X /\ Class (the InternalRel of A, x)) / (card Class (the
InternalRel of A, x)) >= 0;
hence 0 <= MemberFunc (X, A).x by Def9;
card (X /\ Class (the InternalRel of A, x)) <= (card Class (the
InternalRel of A, x)) by NAT_1:43,XBOOLE_1:17;
then card (X /\ Class (the InternalRel of A, x)) / (card Class (the
InternalRel of A, x)) <= 1 by XREAL_1:185;
hence thesis by Def9;
end;
theorem
MemberFunc (X, A).x in [. 0, 1 .]
proof
0 <= MemberFunc (X, A).x & MemberFunc (X, A).x <= 1 by Th38;
hence thesis by XXREAL_1:1;
end;
reserve A for finite Approximation_Space,
X, Y for Subset of A,
x for Element of A;
theorem Th40:
MemberFunc (X, A).x = 1 iff x in LAp X
proof
hereby
assume
A1: MemberFunc (X, A).x = 1;
MemberFunc (X, A).x = card (X /\ Class (the InternalRel of A, x)) / (
card Class (the InternalRel of A, x)) by Def9;
then card (X /\ Class (the InternalRel of A, x)) = (card Class (the
InternalRel of A, x)) by A1,XCMPLX_1:58;
then
X /\ Class (the InternalRel of A, x) = Class (the InternalRel of A, x)
by CARD_2:102,XBOOLE_1:17;
then Class (the InternalRel of A, x) c= X by XBOOLE_1:18;
hence x in LAp X;
end;
assume x in LAp X;
then
A2: card (X /\ Class (the InternalRel of A, x)) = card Class (the
InternalRel of A, x) by Th8,XBOOLE_1:28;
MemberFunc (X, A).x = card (X /\ Class (the InternalRel of A, x)) / (
card Class (the InternalRel of A, x)) by Def9;
hence thesis by A2,XCMPLX_1:60;
end;
theorem Th41:
MemberFunc (X, A).x = 0 iff x in (UAp X)`
proof
hereby
assume
A1: MemberFunc (X, A).x = 0;
MemberFunc (X, A).x = card (X /\ Class (the InternalRel of A, x)) / (
card Class (the InternalRel of A, x)) by Def9;
then X /\ Class (the InternalRel of A, x) = {} by A1,XCMPLX_1:50;
then X misses Class (the InternalRel of A, x);
then not x in UAp X by Th10;
hence x in (UAp X)` by XBOOLE_0:def 5;
end;
assume x in (UAp X)`;
then not x in UAp X by XBOOLE_0:def 5;
then X misses Class (the InternalRel of A, x);
then
A2: card (X /\ Class (the InternalRel of A, x)) = 0;
MemberFunc (X, A).x = card (X /\ Class (the InternalRel of A, x)) / (
card Class (the InternalRel of A, x)) by Def9;
hence thesis by A2;
end;
theorem Th42:
0 < MemberFunc (X, A).x & MemberFunc (X, A).x < 1 iff x in BndAp X
proof
hereby
assume that
A1: 0 < MemberFunc (X, A).x and
A2: MemberFunc (X, A).x < 1;
not x in (UAp X)` by A1,Th41;
then
A3: x in UAp X by XBOOLE_0:def 5;
not x in LAp X by A2,Th40;
hence x in BndAp X by A3,XBOOLE_0:def 5;
end;
assume
A4: x in BndAp X;
then not x in LAp X by XBOOLE_0:def 5;
then
A5: MemberFunc (X, A).x <> 1 by Th40;
x in UAp X by A4,XBOOLE_0:def 5;
then not x in (UAp X)` by XBOOLE_0:def 5;
then
A6: 0 <> MemberFunc (X, A).x by Th41;
MemberFunc (X, A).x <= 1 by Th38;
hence thesis by A6,A5,Th38,XXREAL_0:1;
end;
theorem Th43:
for A being discrete Approximation_Space, X being Subset of A
holds X is exact
proof
let A be discrete Approximation_Space, X be Subset of A;
A1: the InternalRel of A = id the carrier of A by ORDERS_3:def 1;
X = UAp X
proof
thus X c= UAp X by Th13;
let x be object;
assume
A2: x in UAp X;
then Class (the InternalRel of A, x) meets X by Th10;
then
A3: ex y being object st y in Class (the InternalRel of A, x) & y in X
by XBOOLE_0:3;
Class (the InternalRel of A, x) = {x} by A1,A2,EQREL_1:25;
hence thesis by A3,TARSKI:def 1;
end;
hence thesis;
end;
registration
let A be discrete Approximation_Space;
cluster -> exact for Subset of A;
coherence by Th43;
end;
theorem
for A being discrete finite Approximation_Space, X being Subset of A
holds MemberFunc (X, A) = chi (X, the carrier of A)
proof
let A be discrete finite Approximation_Space, X be Subset of A;
reconsider F = MemberFunc (X, A) as Function of the carrier of A, REAL;
set G = chi (X, the carrier of A);
{In(0,REAL),In(1,REAL)} c= REAL;
then reconsider G as Function of the carrier of A, REAL by FUNCT_2:7;
for x being object st x in the carrier of A holds F.x = G.x
proof
let x be object;
assume
A1: x in the carrier of A;
per cases;
suppose
A2: x in X;
then x in LAp X by Th15;
then F.x = 1 by Th40;
hence thesis by A2,FUNCT_3:def 3;
end;
suppose
A3: not x in X;
then not x in UAp X by Th16;
then x in (UAp X)` by A1,XBOOLE_0:def 5;
then F.x = 0 by Th41;
hence thesis by A1,A3,FUNCT_3:def 3;
end;
end;
hence thesis by FUNCT_2:12;
end;
theorem
for A being finite Approximation_Space, X being Subset of A,
x, y being set st [x,y] in the InternalRel of A holds
MemberFunc (X, A).x = MemberFunc (X, A).y
proof
let A be finite Approximation_Space, X be Subset of A, x, y be set;
assume
A1: [x,y] in the InternalRel of A;
then
A2: y is Element of A by ZFMISC_1:87;
x is Element of A by A1,ZFMISC_1:87;
then
A3: MemberFunc (X, A).x = card (X /\ Class (the InternalRel of A, x)) / (
card Class (the InternalRel of A, x)) by Def9;
x in Class (the InternalRel of A, y) by A1,EQREL_1:19;
then
Class (the InternalRel of A, x) = Class (the InternalRel of A, y) by A2,
EQREL_1:23;
hence thesis by A2,A3,Def9;
end;
theorem
MemberFunc (X`,A).x = 1 - (MemberFunc (X,A).x)
proof
A1: [#]A /\ Class (the InternalRel of A, x) = Class (the InternalRel of A, x
) by XBOOLE_1:28;
MemberFunc (X`,A).x = card (([#]A \ X) /\ Class (the InternalRel of A, x
)) / (card Class (the InternalRel of A, x)) by Def9
.= (card (([#]A /\ Class (the InternalRel of A, x)) \ (X /\ Class (the
InternalRel of A, x)))) / (card Class (the InternalRel of A, x)) by XBOOLE_1:50
.= (card ([#]A /\ Class (the InternalRel of A, x)) - card (X /\ Class (
the InternalRel of A, x))) / (card Class (the InternalRel of A, x)) by A1,
CARD_2:44,XBOOLE_1:17
.= card ([#]A /\ Class (the InternalRel of A, x))/ (card Class (the
InternalRel of A, x)) - (card (X /\ Class (the InternalRel of A, x)) / (card
Class (the InternalRel of A, x))) by XCMPLX_1:120
.= card (Class (the InternalRel of A, x))/ (card Class (the InternalRel
of A, x)) - (card (X /\ Class (the InternalRel of A, x)) / (card Class (the
InternalRel of A, x))) by XBOOLE_1:28
.= 1 - card (X /\ Class (the InternalRel of A, x)) / (card Class (the
InternalRel of A, x)) by XCMPLX_1:60
.= 1 - (MemberFunc (X,A).x) by Def9;
hence thesis;
end;
theorem Th47:
X c= Y implies MemberFunc (X, A).x <= MemberFunc (Y, A).x
proof
set CI = Class (the InternalRel of A, x);
assume X c= Y;
then card (Y /\ CI) >= card (X /\ CI) by NAT_1:43,XBOOLE_1:26;
then
A1: card (Y /\ CI) / (card CI) >= card (X /\ CI) / (card CI) by XREAL_1:72;
MemberFunc (X, A).x = card (X /\ CI) / (card CI) by Def9;
hence thesis by A1,Def9;
end;
theorem
MemberFunc (X \/ Y, A).x >= MemberFunc (X, A).x by Th47,XBOOLE_1:7;
theorem
MemberFunc (X /\ Y, A).x <= MemberFunc (X, A).x by Th47,XBOOLE_1:17;
theorem
MemberFunc (X \/ Y, A).x >= max (MemberFunc (X, A).x, MemberFunc (Y, A ).x)
proof
MemberFunc (X \/ Y, A).x >= MemberFunc (X, A).x & MemberFunc (X \/ Y, A)
.x >= MemberFunc (Y, A).x by Th47,XBOOLE_1:7;
hence thesis by XXREAL_0:28;
end;
theorem Th51:
X misses Y implies MemberFunc (X \/ Y, A).x =
MemberFunc (X, A).x + MemberFunc (Y, A).x
proof
assume
A1: X misses Y;
card ((X \/ Y) /\ Class (the InternalRel of A, x)) = card ((X /\ Class (
the InternalRel of A, x)) \/ (Y /\ Class (the InternalRel of A, x))) by
XBOOLE_1:23
.= card (X /\ Class (the InternalRel of A, x)) + card (Y /\ Class (the
InternalRel of A, x)) by A1,CARD_2:40,XBOOLE_1:76;
then
MemberFunc (X \/ Y, A).x = (card (X /\ Class (the InternalRel of A, x))
+ card (Y /\ Class (the InternalRel of A, x))) / (card Class (the InternalRel
of A, x)) by Def9
.= card (X /\ Class (the InternalRel of A, x)) / (card Class (the
InternalRel of A, x)) + card (Y /\ Class (the InternalRel of A, x)) / (card
Class (the InternalRel of A, x)) by XCMPLX_1:62
.= MemberFunc (X, A).x + card (Y /\ Class (the InternalRel of A, x)) / (
card Class (the InternalRel of A, x)) by Def9
.= MemberFunc (X, A).x + MemberFunc (Y, A).x by Def9;
hence thesis;
end;
theorem
MemberFunc (X /\ Y, A).x <= min (MemberFunc (X, A).x, MemberFunc (Y, A).x)
proof
MemberFunc (X /\ Y, A).x <= MemberFunc (X, A).x & MemberFunc (X /\ Y, A)
.x <= MemberFunc (Y, A).x by Th47,XBOOLE_1:17;
hence thesis by XXREAL_0:20;
end;
definition
let A be finite Tolerance_Space;
let X be FinSequence of bool the carrier of A;
let x be Element of A;
func FinSeqM (x,X) -> FinSequence of REAL means
:Def10:
dom it = dom X & for
n being Nat st n in dom X holds it.n = MemberFunc (X.n, A).x;
existence
proof
deffunc F(Nat) = MemberFunc (X.$1, A).x;
ex z being FinSequence of REAL st len z = len X & for j being Nat st j
in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
then consider z being FinSequence of REAL such that
A1: len z = len X and
A2: for j being Nat st j in dom z holds z.j = F(j);
take z;
thus dom z = Seg len z by FINSEQ_1:def 3
.= dom X by A1,FINSEQ_1:def 3;
let n be Nat;
assume n in dom X;
then
A3: n in Seg len X by FINSEQ_1:def 3;
dom z = Seg len X by A1,FINSEQ_1:def 3;
hence thesis by A2,A3;
end;
uniqueness
proof
let A1, A2 be FinSequence of REAL such that
A4: dom A1 = dom X and
A5: for n being Nat st n in dom X holds A1.n = MemberFunc (X.n, A).x and
A6: dom A2 = dom X and
A7: for n being Nat st n in dom X holds A2.n = MemberFunc (X.n, A).x;
for n being Nat st n in dom A1 holds A1.n = A2.n
proof
let n be Nat;
assume
A8: n in dom A1;
reconsider n as Element of NAT by ORDINAL1:def 12;
A1.n = MemberFunc (X.n, A).x by A4,A5,A8
.= A2.n by A4,A7,A8;
hence thesis;
end;
hence thesis by A4,A6,FINSEQ_1:13;
end;
end;
theorem Th53:
for X being FinSequence of bool the carrier of A,
x being Element of A, y being Subset of A holds
FinSeqM (x, X^<*y*>) = FinSeqM (x, X) ^ <* MemberFunc (y, A).x *>
proof
let X be FinSequence of bool the carrier of A, x be Element of A,
y be Subset of A;
set p = FinSeqM (x, X^<*y*>);
set q = FinSeqM (x, X) ^ <* MemberFunc (y, A).x *>;
dom X = dom FinSeqM (x, X) by Def10;
then Seg len X = dom FinSeqM (x, X) by FINSEQ_1:def 3
.= Seg len FinSeqM (x, X) by FINSEQ_1:def 3;
then
A1: len X = len FinSeqM (x, X) by FINSEQ_1:6;
A2: dom p = dom (X^<*y*>) by Def10
.= Seg (len X + len <* y *>) by FINSEQ_1:def 7
.= Seg (len X + 1) by FINSEQ_1:39;
A3: for k being Nat st k in dom p holds p.k = q.k
proof
let k be Nat;
assume
A4: k in dom p;
then reconsider k as Element of NAT;
A5: 1 <= k by A4,FINSEQ_3:25;
k in dom (X^<*y*>) by A4,Def10;
then
A6: p.k = MemberFunc ((X^<*y*>).k, A).x by Def10;
A7: k <= len X + 1 by A2,A4,FINSEQ_1:1;
per cases by A7,NAT_1:8;
suppose
A8: k <= len X; then
A9: k in dom X by A5,FINSEQ_3:25;
k in dom FinSeqM (x, X) by A1,A5,A8,FINSEQ_3:25;
then q.k = FinSeqM (x, X).k by FINSEQ_1:def 7
.= MemberFunc (X.k, A).x by A9,Def10;
hence thesis by A6,A9,FINSEQ_1:def 7;
end;
suppose
A10: k = len X + 1;
then q.k = MemberFunc (y, A).x by A1,FINSEQ_1:42;
hence thesis by A6,A10,FINSEQ_1:42;
end;
end;
dom q = Seg (len FinSeqM (x, X) + len <* MemberFunc (y, A).x *>)
by FINSEQ_1:def 7
.= Seg (len X + 1) by A1,FINSEQ_1:39;
hence thesis by A2,A3,FINSEQ_1:13;
end;
theorem Th54:
MemberFunc ({}A, A).x = 0
proof
UAp {}A = {} by Th19;
then (UAp {}A)` = [#] A;
hence thesis by Th41;
end;
theorem
for X being disjoint_valued FinSequence of bool the carrier of A holds
MemberFunc (Union X, A).x = Sum FinSeqM (x, X)
proof
let X be disjoint_valued FinSequence of bool the carrier of A;
defpred P[FinSequence of bool the carrier of A] means $1 is disjoint_valued
implies MemberFunc (Union $1, A).x = Sum FinSeqM (x, $1);
A1: for p being FinSequence of bool the carrier of A for y being Subset of A
st P[p] holds P[p^<*y*>]
proof
let p be FinSequence of bool the carrier of A;
let y be Subset of A;
assume
A2: P[p];
P[p^<*y*>]
proof
assume
A3: p^<*y*> is disjoint_valued;
A4: Union p misses y
proof
assume Union p meets y;
then consider x being object such that
A5: x in Union p and
A6: x in y by XBOOLE_0:3;
consider X being set such that
A7: x in X and
A8: X in rng p by A5,TARSKI:def 4;
consider m being object such that
A9: m in dom p and
A10: X = p.m by A8,FUNCT_1:def 3;
reconsider m as Element of NAT by A9;
A11: (p^<*y*>).m = p.m & m <= len p by A9,FINSEQ_1:def 7,FINSEQ_3:25;
A12: (p^<*y*>).(len p + 1) = y & len p < len p + 1 by FINSEQ_1:42,NAT_1:13;
p.m meets y by A6,A7,A10,XBOOLE_0:3;
hence thesis by A3,A12,A11;
end;
Union (p^<*y*>) = Union p \/ Union <*y*> by Th5
.= Union p \/ y by FINSEQ_3:135;
then MemberFunc (Union (p^<*y*>), A).x = MemberFunc (Union p, A).x +
MemberFunc (y, A).x by A4,Th51
.= Sum (FinSeqM (x, p) ^ <* MemberFunc (y, A).x *>)
by A2,A3,Th6,FINSEQ_6:10,RVSUM_1:74
.= Sum FinSeqM (x, p ^ <*y*>) by Th53;
hence thesis;
end;
hence thesis;
end;
A13: P[<*> bool the carrier of A]
proof
set F = FinSeqM (x, <*> bool the carrier of A);
assume <*> bool the carrier of A is disjoint_valued;
dom F = dom <*> bool the carrier of A by Def10;
then
A14: Sum F = 0 by RELAT_1:41,RVSUM_1:72;
Union <*> bool the carrier of A = {}A by ZFMISC_1:2;
hence thesis by A14,Th54;
end;
for p being FinSequence of bool the carrier of A holds P[p] from
FINSEQ_2:sch 2 (A13,A1);
hence thesis;
end;
theorem
LAp X = { x where x is Element of A : MemberFunc (X, A).x = 1 }
proof
thus LAp X c= { x where x is Element of A : MemberFunc (X, A).x = 1 }
proof
let y be object;
assume
A1: y in LAp X;
then reconsider y9 = y as Element of A;
MemberFunc (X, A).y9 = 1 by A1,Th40;
hence thesis;
end;
let y be object;
assume y in { x where x is Element of A : MemberFunc (X, A).x = 1 };
then ex y9 being Element of A st y9 = y & MemberFunc (X, A). y9 = 1;
hence thesis by Th40;
end;
theorem
UAp X = { x where x is Element of A : MemberFunc (X, A).x > 0 }
proof
thus UAp X c= { x where x is Element of A : MemberFunc (X, A).x > 0 }
proof
let y be object;
assume
A1: y in UAp X;
then reconsider y9 = y as Element of A;
not y in (UAp X)` by A1,XBOOLE_0:def 5;
then MemberFunc (X, A).y9 <> 0 by Th41;
then MemberFunc (X, A).y9 > 0 by Th38;
hence thesis;
end;
let y be object;
assume y in { x where x is Element of A : MemberFunc (X, A).x > 0 };
then
A2: ex y9 being Element of A st y9 = y & MemberFunc (X, A). y9 > 0;
then not y in (UAp X)` by Th41;
hence thesis by A2,XBOOLE_0:def 5;
end;
theorem
BndAp X = { x where x is Element of A : 0 < MemberFunc (X, A).x &
MemberFunc (X, A).x < 1 }
proof
thus BndAp X c= { x where x is Element of A : 0 < MemberFunc (X, A).x &
MemberFunc (X, A).x < 1 }
proof
let y be object;
assume
A1: y in BndAp X;
then reconsider y9 = y as Element of A;
0 < MemberFunc (X, A).y9 & MemberFunc (X, A).y9 < 1 by A1,Th42;
hence thesis;
end;
let y be object;
assume y in { x where x is Element of A : 0 < MemberFunc (X, A).x &
MemberFunc (X, A).x < 1 };
then ex y9 being Element of A st y9 = y & 0 < MemberFunc (X, A).y9 &
MemberFunc (X, A).y9 < 1;
hence thesis by Th42;
end;
begin :: Rough Inclusion
reserve A for Tolerance_Space,
X, Y, Z for Subset of A;
definition
let A be Tolerance_Space, X, Y be Subset of A;
pred X _c= Y means
LAp X c= LAp Y;
reflexivity;
pred X c=^ Y means
UAp X c= UAp Y;
reflexivity;
end;
definition
let A be Tolerance_Space, X, Y be Subset of A;
pred X _c=^ Y means
X _c= Y & X c=^ Y;
reflexivity;
end;
theorem Th59:
X _c= Y & Y _c= Z implies X _c= Z
proof
assume X _c= Y & Y _c= Z;
then LAp X c= LAp Y & LAp Y c= LAp Z;
then LAp X c= LAp Z;
hence thesis;
end;
theorem Th60:
X c=^ Y & Y c=^ Z implies X c=^ Z
proof
assume X c=^ Y & Y c=^ Z;
then UAp X c= UAp Y & UAp Y c= UAp Z;
then UAp X c= UAp Z;
hence thesis;
end;
theorem
X _c=^ Y & Y _c=^ Z implies X _c=^ Z by Th60,Th59;
begin :: Rough Equality of Sets
definition
let A be Tolerance_Space, X, Y be Subset of A;
pred X _= Y means
LAp X = LAp Y;
reflexivity;
symmetry;
pred X =^ Y means
UAp X = UAp Y;
reflexivity;
symmetry;
pred X _=^ Y means
LAp X = LAp Y & UAp X = UAp Y;
reflexivity;
symmetry;
end;
definition
let A be Tolerance_Space, X, Y be Subset of A;
redefine pred X _= Y means :: redefines _= (ROUGHS_1, definition)
X _c= Y & Y _c= X;
compatibility
proof
thus X _= Y implies X _c= Y & Y _c= X;
assume X _c= Y & Y _c= X;
then LAp X c= LAp Y & LAp Y c= LAp X;
then LAp X = LAp Y;
hence thesis;
end;
redefine pred X =^ Y means :: redefines =^ (ROUGHS_1, definition)
X c=^ Y & Y c=^ X;
compatibility
proof
thus X =^ Y implies X c=^ Y & Y c=^ X;
assume X c=^ Y & Y c=^ X;
then UAp X c= UAp Y & UAp Y c= UAp X;
then UAp X = UAp Y;
hence thesis;
end;
redefine pred X _=^ Y means :: redefines _=^ (ROUGHS_1, definition)
X _= Y & X =^ Y;
compatibility;
end;