:: Basic Properties of Rough Sets and Rough Membership Function :: by Adam Grabowski :: :: Received November 23, 2003 :: Copyright (c) 2003-2018 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; 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 total reflexive Relation of X holds id X c= R proof let X be set, R be total reflexive Relation of X; field R = X by ORDERS_1:12; hence thesis by RELAT_2:1; 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; 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; 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 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 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 X _= Y & X =^ Y; compatibility; end;