Copyright (c) 2003 Association of Mizar Users
environ vocabulary ROUGHS_1, ARYTM_3, RCOMP_1, SQUARE_1, ARYTM_1, FUNCT_1, BOOLE, TARSKI, RELAT_1, RELAT_2, SUBSET_1, ORDERS_1, PARTFUN1, EQREL_1, CARD_1, FINSET_1, TOLER_1, NATTRA_1, REALSET1, FUNCT_3, PROB_2, FINSEQ_1, PROB_1, RLVECT_1, FINSEQ_2, FUNCOP_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, CARD_1, XREAL_0, REAL_1, NAT_1, SQUARE_1, FINSET_1, FUNCOP_1, RELAT_1, RELAT_2, FUNCT_1, FINSEQ_1, RVSUM_1, FINSEQ_2, RELSET_1, PARTFUN1, REALSET1, PROB_1, PROB_2, FUNCT_2, FUNCT_3, STRUCT_0, PRE_TOPC, GROUP_1, ORDERS_1, EQREL_1, RCOMP_1, TOLER_1, ORDERS_3; constructors RELAT_2, MCART_1, WELLORD1, PRE_TOPC, PARTFUN1, MEMBERED, XBOOLE_0, ORDERS_1, EQREL_1, SUBSET_1, CARD_1, CARD_2, XCMPLX_0, NUMBERS, XREAL_0, FINSET_1, SQUARE_1, RCOMP_1, TOLER_1, NAT_1, GROUP_1, ORDINAL2, ORDINAL1, REAL_1, FSM_1, REALSET1, ORDERS_3, PROB_1, FUNCT_3, PROB_2, FINSEQ_1, RVSUM_1, FUNCOP_1, FINSEQ_2, TAXONOM2; clusters RELSET_1, STRUCT_0, PRE_TOPC, SUBSET_1, MEMBERED, ZFMISC_1, PARTFUN1, XBOOLE_0, XREAL_0, FINSET_1, ORDINAL2, ARYTM_3, FSM_1, ORDERS_1, EQREL_1, TAXONOM2, REALSET1, FINSEQ_1, FUNCOP_1; requirements BOOLE, SUBSET, ARITHM, NUMERALS, REAL; definitions TARSKI, XBOOLE_0, PROB_2; theorems EQREL_1, XBOOLE_0, XBOOLE_1, PRE_TOPC, SUBSET_1, XCMPLX_1, TRIANG_1, CARD_2, CARD_1, KURATO_2, REAL_1, TOPREAL5, TOLER_1, REAL_2, NAT_1, SQUARE_1, GROUP_1, TARSKI, ZFMISC_1, RELAT_1, RELAT_2, ORDERS_3, SPPOL_1, CHAIN_1, FUNCT_2, FUNCT_3, RVSUM_1, CARD_3, FUNCT_6, FINSEQ_1, PROB_1, FINSEQ_3, PROB_2, FUNCT_1, GRFUNC_1, FINSEQ_6, FINSEQ_2, REALSET1, ORDERS_1, RELSET_1, SYSREL, FUNCOP_1; schemes FUNCT_2, COMPLSP1, FINSEQ_2; begin :: Preliminaries definition 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 set such that A2: x in X & y in X & x <> y by SPPOL_1:3; [x,y] in Total X by A2, TOLER_1:15; hence thesis by A1, A2, 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; definition let A be non trivial set; cluster RelStr (# A, Total A #) -> non diagonal; coherence proof not Total A c= id A by Th1; hence thesis by Def1; end; 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 set st [a,b] in id the carrier of L holds [a,b] in the InternalRel of L proof let a,b be set; 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_1:def 4; 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; A2: the carrier of A is trivial by A1, REALSET1:def 13; per cases by A2, REALSET1:def 12; suppose A3: the carrier of A is empty; then the InternalRel of A = {} by RELSET_1:26; hence thesis by A3, ORDERS_3:def 1, RELAT_1:81; suppose ex x being set st the carrier of A = {x}; then consider x being set such that A4: the carrier of A = {x}; the InternalRel of A c= [:{x}, {x}:] by A4; then the InternalRel of A c= { [x, x] } by ZFMISC_1:35; then A5: the InternalRel of A = { [x, x] } or the InternalRel of A = {} by ZFMISC_1:39; A6: the InternalRel of A is_reflexive_in the carrier of A by A1, ORDERS_1:def 4; x in the carrier of A by A4, TARSKI:def 1; then the InternalRel of A = id {x} by A5, SYSREL:30, A6, RELAT_2:def 1; hence thesis by A4, ORDERS_3:def 1; end; definition cluster non discrete -> non trivial (reflexive RelStr); coherence by Lm1; cluster reflexive trivial -> discrete RelStr; coherence by Lm1; 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 EQREL_1:15; hence thesis by RELAT_2:17; end; Lm2: for A being RelStr st A is discrete holds A is diagonal proof let A be RelStr; assume A is discrete; then the InternalRel of A = id the carrier of A by ORDERS_3:def 1; hence thesis by Def1; end; definition cluster discrete -> diagonal RelStr; coherence by Lm2; cluster non diagonal -> non discrete RelStr; coherence by Lm2; end; definition cluster non diagonal non empty RelStr; existence proof consider A being 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; the InternalRel of A c= id the carrier of A proof for a,b being set st [a,b] in the InternalRel of A holds [a,b] in id the carrier of A proof let a,b be set; assume A2: [a,b] in the InternalRel of A; then A3: a is Element of A & b is Element of A by ZFMISC_1:106; then a = b by A1, A2; hence [a,b] in id the carrier of A by A3, RELAT_1:def 10; end; hence thesis by RELAT_1:def 3; end; 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:44 .= union rng p \/ union rng q by ZFMISC_1:96 .= Union p \/ union rng q by PROB_1:def 3 .= Union p \/ Union q by PROB_1:def 3; hence thesis by PROB_1:def 3; 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 A1: q is disjoint_valued & p c= q; for x, y being set st x <> y holds p.x misses p.y proof let x, y be set; assume A2: x <> y; assume A3: 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 4; hence thesis by A3, XBOOLE_1:65; end; then p.x = q.x & p.y = q.y by A1, GRFUNC_1:8; hence thesis by A2, A3, A1, PROB_2:def 3; end; hence thesis by PROB_2:def 3; end; definition cluster empty -> disjoint_valued Function; coherence proof let X be Function; assume A1: X is empty; X is disjoint_valued proof let x, y be set; assume x <> y; X.x = {} by FUNCT_1:def 4, A1, RELAT_1:60; hence thesis by XBOOLE_1:65; end; hence thesis; end; end; definition let A be set; cluster disjoint_valued FinSequence of A; existence proof per cases; suppose A is empty; reconsider X = {} as empty FinSequence of A by FINSEQ_1:29; X is disjoint_valued; hence thesis; suppose A1: A is non empty; consider a being Element of A; reconsider X = 1 |-> a as FinSequence of A by A1, FINSEQ_2:77; X is disjoint_valued proof let x, y be set; assume A2: x <> y; per cases; suppose x in dom X & y in dom X; then x in Seg 1 & y in Seg 1 by FINSEQ_2:68; then x = 1 & y = 1 by TARSKI:def 1, FINSEQ_1:4; hence thesis by A2; suppose not x in dom X or not y in dom X; then X.x = {} or X.y = {} by FUNCT_1:def 4; hence thesis by XBOOLE_1:65; end; hence thesis; end; end; Lm3: :: move to FINSEQ_2 for a being set, k being Nat holds dom (k |-> a) = Seg k proof let a be set, k be Nat; dom (k |-> a) = dom (Seg k --> a) by FINSEQ_2:def 2; hence thesis by FUNCOP_1:19; end; definition let A be non empty set; cluster non empty disjoint_valued FinSequence of A; existence proof consider a being Element of A; reconsider X = 1 |-> a as FinSequence of A by FINSEQ_2:77; A1: X is non empty by Lm3, RELAT_1:60, FINSEQ_1:4; X is disjoint_valued proof let x, y be set; assume A2: x <> y; per cases; suppose x in dom X & y in dom X; then x in Seg 1 & y in Seg 1 by FINSEQ_2:68; then x = 1 & y = 1 by TARSKI:def 1, FINSEQ_1:4; hence thesis by A2; suppose not x in dom X or not y in dom X; then X.x = {} or X.y = {} by FUNCT_1:def 4; hence thesis by XBOOLE_1:65; end; 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 4; hence thesis by XBOOLE_1:2; suppose n in dom X; hence thesis by FINSEQ_2:13; 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 set; assume x in union rng X; then consider Y being set such that A1: x in Y & Y in rng X by TARSKI:def 4; thus thesis by A1; end; hence thesis by PROB_1:def 3; end; end; definition let A be finite set; let R be Relation of A; cluster RelStr (# A, R #) -> finite; coherence by GROUP_1:def 13; end; theorem Th7: for X, x, y being set, T being Tolerance of X st x in Class (T, y) holds y in Class (T, x) proof let X, x, y be set, T be Tolerance of X; assume x in Class (T, y); then [x,y] in T by EQREL_1:27; then [y,x] in T by EQREL_1:12; hence thesis by EQREL_1:27; 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; definition cluster with_equivalence -> with_tolerance RelStr; coherence proof let L be RelStr; assume L is with_equivalence; then the InternalRel of L is Equivalence_Relation of the carrier of L by Def2; hence thesis by Def3; end; end; definition let A be set; cluster RelStr (# A, id A #) -> with_equivalence; coherence by Def2; end; definition cluster discrete finite with_equivalence non empty RelStr; existence proof set E = RelStr (# {{}}, id {{}} #); E is discrete; hence thesis; end; cluster non diagonal finite with_equivalence non empty RelStr; existence proof set C = {0,1}; set R = Total C; set E = RelStr (# C, R #); reconsider E as non empty RelStr; A1: E is with_equivalence by Def2; E is non diagonal proof C is non trivial by CHAIN_1:4; then not the InternalRel of E c= id the carrier of E by Th1; hence thesis by Def1; end; hence thesis by A1; end; end; definition mode Approximation_Space is with_equivalence non empty RelStr; mode Tolerance_Space is with_tolerance non empty RelStr; end; definition let A be Tolerance_Space; cluster the InternalRel of A -> total reflexive symmetric; coherence by Def3; end; definition let A be Approximation_Space; cluster the InternalRel of A -> transitive; coherence by Def2; end; definition let A be Tolerance_Space; let X be Subset of A; func LAp X -> Subset of A equals :Def4: { 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 set; assume y in { x where x is Element of A : Class (the InternalRel of A, x) c= X }; then consider x being Element of A such that A1: y = x & Class (the InternalRel of A, x) c= X; thus thesis by A1; end; hence thesis; end; func UAp X -> Subset of A equals :Def5: { 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 set; assume y in { x where x is Element of A : Class (the InternalRel of A, x) meets X }; then consider x being Element of A such that A2: y = x & Class (the InternalRel of A, x) meets X; thus thesis by A2; end; hence thesis; end; end; definition let A be Tolerance_Space; let X be Subset of A; func BndAp X -> Subset of A equals :Def6: UAp X \ LAp X; coherence; end; definition let A be Tolerance_Space; let X be Subset of A; attr X is rough means :Def7: BndAp X <> {}; antonym X is exact; end; reserve A for Tolerance_Space, X, Y for Subset of A; theorem Th8: for x being set st x in LAp X holds Class (the InternalRel of A, x) c= X proof let x be set; assume x in LAp X; then x in { x1 where x1 is Element of A : Class (the InternalRel of A, x1) c= X } by Def4; then consider x1 being Element of A such that A1: x = x1 & Class (the InternalRel of A, x1) c= X; thus thesis by A1; end; theorem Th9: for x being Element of A st Class (the InternalRel of A, x) c= X holds x in LAp X proof let x be Element of A; assume Class (the InternalRel of A, x) c= X; then x in { x1 where x1 is Element of A : Class (the InternalRel of A, x1) c= X }; hence thesis by Def4; end; 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 x in { x1 where x1 is Element of A : Class (the InternalRel of A, x1) meets X } by Def5; then consider x1 being Element of A such that A1: x = x1 & Class (the InternalRel of A, x1) meets X; thus thesis by A1; end; theorem Th11: for x being Element of A st Class (the InternalRel of A, x) meets X holds x in UAp X proof let x be Element of A; assume Class (the InternalRel of A, x) meets X; then x in { x1 where x1 is Element of A : Class (the InternalRel of A, x1) meets X }; hence thesis by Def5; end; theorem Th12: LAp X c= X proof let x be set; assume x in LAp X; then x in { y where y is Element of A : Class (the InternalRel of A, y) c= X } by Def4; 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:28; hence thesis by A1; end; theorem Th13: X c= UAp X proof let x be set; assume A1: x in X; then reconsider x' = x as Element of A; x' in Class (the InternalRel of A, x') by EQREL_1:28; then Class (the InternalRel of A, x') meets X by A1, XBOOLE_0:3; then x in { y where y is Element of A : Class (the InternalRel of A, y) meets X }; hence thesis by Def5; end; theorem Th14: LAp X c= UAp X proof A1: LAp X c= X by Th12; X c= UAp X by Th13; hence thesis by A1, XBOOLE_1:1; 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 = {} by Def7; then UAp X \ LAp X = {} by Def6; then UAp X c= LAp X by XBOOLE_1:37; then UAp X = LAp X by A1, XBOOLE_0:def 10; then A2: X c= LAp X by Th13; LAp X c= X by Th12; hence LAp X = X by A2, XBOOLE_0:def 10; end; assume A3: LAp X = X; UAp X c= X proof let y be set; assume y in UAp X; then Class (the InternalRel of A, y) meets X by Th10; then consider z being set such that A4: z in Class (the InternalRel of A, y) & z in LAp X by A3, XBOOLE_0:3; A5: Class (the InternalRel of A, z) c= X by A4, Th8; y in Class (the InternalRel of A, z) by A4, Th7; hence thesis by A5; end; then UAp X \ LAp X = {} by XBOOLE_1:37, A3; then BndAp X = {} by Def6; hence thesis by Def7; end; theorem Th16: X is exact iff UAp X = X proof hereby assume X is exact; then BndAp X = {} by Def7; then UAp X \ LAp X = {} by Def6; then A1: UAp X c= LAp X by XBOOLE_1:37; LAp X c= X by Th12; then A2: UAp X c= X by A1, XBOOLE_1:1; X c= UAp X by Th13; hence UAp X = X by A2, XBOOLE_0:def 10; end; assume A3: UAp X = X; X c= LAp X proof let x be set; assume A4: x in X; Class (the InternalRel of A, x) c= X proof let y be set; assume A5: y in Class (the InternalRel of A, x); then [y,x] in the InternalRel of A by EQREL_1:27; then [x,y] in the InternalRel of A by EQREL_1:12; then x in Class (the InternalRel of A, y) by EQREL_1:27; then Class (the InternalRel of A, y) meets X by A4, XBOOLE_0:3; hence thesis by A3, A5, Th11; end; hence thesis by A4, Th9; end; then UAp X \ LAp X = {} by A3, XBOOLE_1:37; then BndAp X = {} by Def6; hence thesis by Def7; end; theorem X = LAp X iff X = UAp X proof X = LAp X iff X is exact by Th15; hence thesis by Th16; end; theorem Th18: LAp {}A = {} proof assume LAp {}A <> {}; then consider x being set such that A1: x in LAp {}A by XBOOLE_0:def 1; x in { y where y is Element of A : Class (the InternalRel of A, y) c= {}A } by A1, Def4; then consider y being Element of A such that A2: y = x & Class (the InternalRel of A, y) c= {}A; Class (the InternalRel of A, y) = {} by A2, XBOOLE_1:3; hence thesis by EQREL_1:28; end; theorem Th19: UAp {}A = {} proof assume UAp {}A <> {}; then consider x being set such that A1: x in UAp {}A by XBOOLE_0:def 1; x in { y where y is Element of A : Class (the InternalRel of A, y) meets {}A } by A1, Def5; then consider y being Element of A such that A2: y = x & Class (the InternalRel of A, y) meets {}A; thus thesis by A2, XBOOLE_1:65; end; theorem Th20: LAp [#]A = [#]A proof thus LAp [#]A c= [#]A by PRE_TOPC:14; let x be set; assume A1: x in [#]A; Class (the InternalRel of A, x) c= [#]A by PRE_TOPC:14; hence thesis by A1, Th9; end; theorem UAp [#]A = [#]A proof LAp [#]A c= UAp [#]A by Th14; then A1: [#]A c= UAp [#]A by Th20; UAp [#]A c= [#]A by PRE_TOPC:14; hence thesis by A1, XBOOLE_0:def 10; end; theorem LAp (X /\ Y) = LAp X /\ LAp Y proof thus LAp (X /\ Y) c= LAp X /\ LAp Y proof let x be set; assume A1: x in LAp (X /\ Y); Class (the InternalRel of A, x) c= X /\ Y by A1, Th8; then Class (the InternalRel of A, x) c= X & Class (the InternalRel of A, x) c= Y by XBOOLE_1:18; then x in LAp X & x in LAp Y by A1, Th9; hence thesis by XBOOLE_0:def 3; end; let x be set; assume A2: x in LAp X /\ LAp Y; x in LAp X & x in LAp Y by A2, XBOOLE_0:def 3; then Class (the InternalRel of A, x) c= X & Class (the InternalRel of A, x) c= Y by Th8; then Class (the InternalRel of A, x) c= X /\ Y by XBOOLE_1:19; hence thesis by A2, Th9; end; theorem UAp (X \/ Y) = UAp X \/ UAp Y proof thus UAp (X \/ Y) c= UAp X \/ UAp Y proof let x be set; assume A1: x in UAp (X \/ Y); Class (the InternalRel of A, x) meets (X \/ Y) by A1, 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, Th11; hence thesis by XBOOLE_0:def 2; end; let x be set; assume A2: x in UAp X \/ UAp Y; x in UAp X or x in UAp Y by A2, XBOOLE_0:def 2; 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, Th11; end; theorem Th24: X c= Y implies LAp X c= LAp Y proof assume A1: X c= Y; let x be set; assume A2: x in LAp X; Class (the InternalRel of A, x) c= X by A2, Th8; then Class (the InternalRel of A, x) c= Y by A1, XBOOLE_1:1; hence thesis by A2, Th9; end; theorem Th25: X c= Y implies UAp X c= UAp Y proof assume A1: X c= Y; let x be set; assume A2: x in UAp X; Class (the InternalRel of A, x) meets X by A2, Th10; then Class (the InternalRel of A, x) meets Y by A1, XBOOLE_1:63; hence thesis by A2, Th11; end; theorem LAp X \/ LAp Y c= LAp (X \/ Y) proof let x be set; assume A1: x in LAp X \/ LAp Y; per cases by A1, XBOOLE_0:def 2; suppose x in LAp X; then Class (the InternalRel of A, x) c= X by Th8; then Class (the InternalRel of A, x) c= X \/ Y by XBOOLE_1:10; hence thesis by A1, Th9; suppose x in LAp Y; then Class (the InternalRel of A, x) c= Y by Th8; then Class (the InternalRel of A, x) c= X \/ Y by XBOOLE_1:10; hence thesis by A1, Th9; end; theorem UAp (X /\ Y) c= UAp X /\ UAp Y proof let x be set; assume A1: x in UAp (X /\ Y); Class (the InternalRel of A, x) meets X /\ Y by A1, Th10; then Class (the InternalRel of A, x) meets X & Class (the InternalRel of A, x) meets Y by XBOOLE_1:74; then x in UAp X & x in UAp Y by A1, Th11; hence thesis by XBOOLE_0:def 3; end; theorem Th28: LAp X` = (UAp X)` proof LAp X` misses UAp X proof assume LAp X` meets UAp X; then consider x being set such that A1: x in LAp X` & x in UAp X by XBOOLE_0:3; A2: Class (the InternalRel of A, x) meets X by A1, Th10; Class (the InternalRel of A, x) c= X` by A1, Th8; then X meets X` by A2, XBOOLE_1:63; hence thesis by PRE_TOPC:26; end; hence LAp X` c= (UAp X)` by PRE_TOPC:21; let x be set; assume A3: x in (UAp X)`; not x in UAp X by A3, SUBSET_1:54; then Class (the InternalRel of A, x) misses X by Th11, A3; then Class (the InternalRel of A, x) c= X` by PRE_TOPC:21; hence thesis by A3, Th9; 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 set; assume x in UAp LAp UAp X; then Class (the InternalRel of A, x) meets LAp UAp X by Th10; then consider y being set such that A1: y in Class (the InternalRel of A, x) & y in LAp UAp X by XBOOLE_0:3; [y, x] in the InternalRel of A by A1, EQREL_1:27; then A2: [x, y] in the InternalRel of A by EQREL_1:12; A3: Class (the InternalRel of A, y) c= UAp X by A1, Th8; x in Class (the InternalRel of A, y) by A2, EQREL_1:27; hence thesis by A3; end; thus UAp X c= UAp LAp UAp X proof X c= LAp UAp X proof let x be set; assume A4: x in X; Class (the InternalRel of A, x) c= UAp X proof let y be set; assume A5: y in Class (the InternalRel of A, x); then [y,x] in the InternalRel of A by EQREL_1:27; then [x,y] in the InternalRel of A by EQREL_1:12; then A6: x in Class (the InternalRel of A, y) by EQREL_1:27; Class (the InternalRel of A, y) meets X by A4, A6, XBOOLE_0:3; hence thesis by A5, Th11; end; hence thesis by A4, Th9; end; hence thesis by Th25; end; end; theorem LAp UAp LAp X = LAp X proof UAp LAp X c= X proof let y be set; assume y in UAp LAp X; then Class (the InternalRel of A, y) meets LAp X by Th10; then consider z being set such that A1: z in Class (the InternalRel of A, y) & z in LAp X by XBOOLE_0:3; [z,y] in the InternalRel of A by A1, EQREL_1:27; then [y,z] in the InternalRel of A by EQREL_1:12; then A2: y in Class (the InternalRel of A, z) by EQREL_1:27; Class (the InternalRel of A, z) c= X by A1, Th8; hence thesis by A2; end; hence LAp UAp LAp X c= LAp X by Th24; thus LAp X c= LAp UAp LAp X proof let x be set; assume A3: x in LAp X; Class (the InternalRel of A, x) c= UAp LAp X proof let y be set; assume A4: y in Class (the InternalRel of A, x); then [y,x] in the InternalRel of A by EQREL_1:27; then [x,y] in the InternalRel of A by EQREL_1:12; then x in Class (the InternalRel of A, y) by EQREL_1:27; then Class (the InternalRel of A, y) meets LAp X by A3, XBOOLE_0:3; hence thesis by A4, Th11; end; hence thesis by A3, Th9; end; end; theorem BndAp X = BndAp X` proof thus BndAp X c= BndAp X` proof let x be set; assume x in BndAp X; then x in UAp X \ LAp X by Def6; then A1: x in UAp X & not x in LAp X by XBOOLE_0:def 4; then x in (LAp X)` by SUBSET_1:50; then A2: x in UAp X` by Th29; not x in (UAp X)` by A1, SUBSET_1:54; then A3: not x in LAp X` by Th28; x in UAp X` \ LAp X` by A2, A3, XBOOLE_0:def 4; hence thesis by Def6; end; thus BndAp X` c= BndAp X proof let x be set; assume A4: x in BndAp X`; then x in UAp X` \ LAp X` by Def6; then A5: x in UAp X` & not x in LAp X` by XBOOLE_0:def 4; then x in (LAp X)` by Th29; then A6: not x in LAp X by SUBSET_1:54; not x in (UAp X)` by A5, Th28; then x in (UAp X)`` by A4, SUBSET_1:50; then x in UAp X \ LAp X by A6, XBOOLE_0:def 4; hence thesis by Def6; end; end; reserve A for Approximation_Space, X, Y for Subset of A; theorem LAp LAp X = LAp X proof thus LAp LAp X c= LAp X by Th12; let x be set; assume A1: x in LAp X; A2: Class (the InternalRel of A, x) c= X by A1, Th8; Class (the InternalRel of A, x) c= LAp X proof let y be set; 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:31; hence thesis by A2, A3, Th9; end; hence thesis by A1, Th9; end; theorem Th34: LAp LAp X = UAp LAp X proof thus LAp LAp X c= UAp LAp X by Th14; let x be set; assume A1: x in UAp LAp X; Class (the InternalRel of A, x) meets LAp X by A1, Th10; then consider z being set such that A2: z in Class (the InternalRel of A, x) & z in LAp X by XBOOLE_0:3; Class (the InternalRel of A, z) c= X by A2, Th8; then A3: Class (the InternalRel of A, x) c= X by A2, A1, EQREL_1:31; Class (the InternalRel of A, x) c= LAp X proof let y be set; assume A4: 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:31; hence thesis by A4, Th9, A3; end; hence thesis by A1, Th9; end; theorem UAp UAp X = UAp X proof hereby let x be set; assume A1: x in UAp UAp X; Class (the InternalRel of A, x) meets UAp X by A1, Th10; then consider y being set such that A2: y in Class (the InternalRel of A, x) & y in UAp X by XBOOLE_0:3; A3: Class (the InternalRel of A, y) meets X by A2, Th10; Class (the InternalRel of A, y) = Class (the InternalRel of A, x) by A2, A1, EQREL_1:31; hence x in UAp X by A1, A3, Th11; end; thus UAp X c= UAp UAp X by Th13; end; theorem Th36: UAp UAp X = LAp UAp X proof thus UAp UAp X c= LAp UAp X proof let x be set; assume A1: x in UAp UAp X; Class (the InternalRel of A, x) meets UAp X by A1, Th10; then consider z being set such that A2: z in Class (the InternalRel of A, x) & z in UAp X by XBOOLE_0:3; A3: Class (the InternalRel of A, z) meets X by A2, Th10; A4: Class (the InternalRel of A, z) = Class (the InternalRel of A, x) by A2, A1, EQREL_1:31; Class (the InternalRel of A, x) c= UAp X proof let y be set; 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:31; hence thesis by A5, Th11, A4, A3; end; hence thesis by Th9, A1; end; thus LAp UAp X c= UAp UAp X by Th14; end; definition let A be Approximation_Space; cluster exact Subset of A; existence proof take {}A; LAp {}A = {} by Th18; hence thesis by Th15; end; end; definition 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 UAp Y \ LAp Y = {} by XBOOLE_1:37; then BndAp Y = {} by Def6; hence thesis by Def7; end; cluster UAp X -> exact; coherence proof set Y = UAp X; UAp Y = LAp Y by Th36; then UAp Y \ LAp Y = {} by XBOOLE_1:37; then BndAp Y = {} by Def6; hence thesis by Def7; 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 A1: x in UAp X & [x,y] in the InternalRel of A; then A2: Class (the InternalRel of A, x) meets X by Th10; A3: x is Element of A & y is Element of A by A1, ZFMISC_1:106; [y,x] in the InternalRel of A by A1, EQREL_1:12; then y in Class (the InternalRel of A, x) by EQREL_1:27; then Class (the InternalRel of A, x) = Class (the InternalRel of A, y) by A1, EQREL_1:31; hence thesis by A3, Th11, A2; end; definition let A be non diagonal Approximation_Space; cluster rough Subset of A; existence proof consider x, y being Element of A such that A1: x <> y & [x,y] in the InternalRel of A by Th4; set X = {x}; A2: x in X by TARSKI:def 1; X c= UAp X by Th13; then y in UAp X by A1, A2, Th37; then UAp X <> X by TARSKI:def 1, A1; 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 means it = [LAp X, UAp X]; existence; end; begin :: Membership Function definition 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:28; hence thesis by CARD_2:59; 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(Element of A) = card (X /\ Class (the InternalRel of A, $1)) / (card Class (the InternalRel of A, $1)); A1: for x being set st x in the carrier of A holds F(x) in REAL; ex f being Function of the carrier of A, REAL st for x being set st x in the carrier of A holds f.x = F(x) from Lambda1(A1); then consider f being Function of the carrier of A, REAL such that A2: for x being set st x in the carrier of A holds f.x = F(x); 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)); let A1, A2 be Function of the carrier of A, REAL such that A3: for x being Element of A holds A1.x = F(x) and A4: for x being Element of A holds A2.x = F(x); for A1,A2 being Function of the carrier of A, REAL st (for x being Element of the carrier of A holds A1.x = F(x)) & (for x being Element of the carrier of A holds A2.x = F(x)) holds A1 = A2 from FuncDefUniq; hence A1 = A2 by A3, A4; end; end; reserve A for finite Tolerance_Space, X, Y for Subset of A, x for Element of A; theorem Th38: 0 <= MemberFunc (X, A).x & MemberFunc (X, A).x <= 1 proof A1: card Class (the InternalRel of A, x) > 0 by NAT_1:19; card (X /\ Class (the InternalRel of A, x)) >= 0 by NAT_1:18; then card (X /\ Class (the InternalRel of A, x)) / (card Class (the InternalRel of A, x)) >= 0 by A1, REAL_2:125; hence 0 <= MemberFunc (X, A).x by Def9; X /\ Class (the InternalRel of A, x) c= Class (the InternalRel of A, x) by XBOOLE_1:17; then card (X /\ Class (the InternalRel of A, x)) <= (card Class (the InternalRel of A, x)) by CARD_1:80; then card (X /\ Class (the InternalRel of A, x)) / (card Class (the InternalRel of A, x)) <= 1 by A1, REAL_2:117; 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 TOPREAL5: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; A2: X /\ Class (the InternalRel of A, x) c= Class (the InternalRel of A, x) by XBOOLE_1:17; 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 A2, TRIANG_1:3; then Class (the InternalRel of A, x) c= X by XBOOLE_1:18; hence x in LAp X by Th9; end; assume x in LAp X; then Class (the InternalRel of A, x) c= X by Th8; then A5: card (X /\ Class (the InternalRel of A, x)) = card Class (the InternalRel of A, x) by 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 A5, 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 card (X /\ Class (the InternalRel of A, x)) = 0 by A1, XCMPLX_1:50; then X /\ Class (the InternalRel of A, x) = {} by CARD_2:59; then X misses Class (the InternalRel of A, x) by XBOOLE_0:def 7; then not x in UAp X by Th10; hence x in (UAp X)` by KURATO_2:1; end; assume x in (UAp X)`; then A3: not x in UAp X by SUBSET_1:54; X misses Class (the InternalRel of A, x) by Th11, A3; then A4: card (X /\ Class (the InternalRel of A, x)) = 0 by CARD_1:78, XBOOLE_0:def 7; MemberFunc (X, A).x = card (X /\ Class (the InternalRel of A, x)) / (card Class (the InternalRel of A, x)) by Def9; hence thesis by A4; end; theorem Th42: 0 < MemberFunc (X, A).x & MemberFunc (X, A).x < 1 iff x in BndAp X proof hereby assume A1: 0 < MemberFunc (X, A).x & MemberFunc (X, A).x < 1; then not x in (UAp X)` by Th41; then x in UAp X & not x in LAp X by KURATO_2:1, A1, Th40; then x in UAp X \ LAp X by XBOOLE_0:def 4; hence x in BndAp X by Def6; end; A2: 0 <= MemberFunc (X, A).x & MemberFunc (X, A).x <= 1 by Th38; assume x in BndAp X; then x in UAp X \ LAp X by Def6; then A3: x in UAp X & not x in LAp X by XBOOLE_0:def 4; then not x in (UAp X)` & not x in LAp X by SUBSET_1:54; then A4: 0 <> MemberFunc (X, A).x by Th41; MemberFunc (X, A).x <> 1 by A3, Th40; hence thesis by A4, A2, REAL_1:def 5; 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 set; assume A2: x in UAp X; then Class (the InternalRel of A, x) meets X by Th10; then consider y being set such that A3: y in Class (the InternalRel of A, x) & y in X by XBOOLE_0:3; Class (the InternalRel of A, x) = {x} by A2, A1, EQREL_1:33; hence thesis by A3, TARSKI:def 1; end; hence thesis; end; definition let A be discrete Approximation_Space; cluster -> exact 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); {0,1} c= REAL by ZFMISC_1:38; then reconsider G as Function of the carrier of A, REAL by FUNCT_2:9; for x being set st x in the carrier of A holds F.x = G.x proof let x be set; 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; suppose A3: not x in X; then not x in UAp X by Th16; then x in (UAp X)` by A1, KURATO_2:1; then F.x = 0 by Th41; hence thesis by A3, A1, FUNCT_3:def 3; end; hence thesis by FUNCT_2:18; 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: x is Element of A & y is Element of A by ZFMISC_1:106; A3: MemberFunc (X, A).x = card (X /\ Class (the InternalRel of A, x)) / (card Class (the InternalRel of A, x)) by A2, Def9; x in Class (the InternalRel of A, y) by A1, EQREL_1:27; then Class (the InternalRel of A, x) = Class (the InternalRel of A, y) by A2, EQREL_1:31; hence thesis by A3, A2, Def9; end; theorem MemberFunc (X`,A).x = 1 - (MemberFunc (X,A).x) proof [#]A /\ Class (the InternalRel of A, x) = Class (the InternalRel of A, x) by PRE_TOPC:15; then A1: X /\ Class (the InternalRel of A, x) c= [#]A /\ Class (the InternalRel of A, x) by XBOOLE_1:17; MemberFunc (X`,A).x = card (X` /\ Class (the InternalRel of A, x)) / (card Class (the InternalRel of A, x)) by Def9 .= card (([#]A \ X) /\ Class (the InternalRel of A, x)) / (card Class (the InternalRel of A, x)) by PRE_TOPC:17 .= (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:63 .= 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:121 .= 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 PRE_TOPC:15 .= 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 A1: X c= Y; A2: card CI > 0 by NAT_1:19; A3: MemberFunc (X, A).x = card (X /\ CI) / (card CI) by Def9; X /\ CI c= Y /\ CI by A1, XBOOLE_1:26; then card (Y /\ CI) >= card (X /\ CI) by CARD_1:80; then card (Y /\ CI) / (card CI) >= card (X /\ CI) / (card CI) by A2, REAL_1:73; hence thesis by A3, Def9; end; theorem Th48: MemberFunc (X \/ Y, A).x >= MemberFunc (X, A).x proof X c= X \/ Y by XBOOLE_1:7; hence thesis by Th47; end; theorem Th49: MemberFunc (X /\ Y, A).x <= MemberFunc (X, A).x proof X /\ Y c= X by XBOOLE_1:17; hence thesis by Th47; end; theorem MemberFunc (X \/ Y, A).x >= max (MemberFunc (X, A).x, MemberFunc (Y, A).x) proof A1: MemberFunc (X \/ Y, A).x >= MemberFunc (X, A).x by Th48; MemberFunc (X \/ Y, A).x >= MemberFunc (Y, A).x by Th48; hence thesis by A1, SQUARE_1:50; 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; A2: X /\ Class (the InternalRel of A, x) misses Y /\ Class (the InternalRel of A, x) by A1, XBOOLE_1:76; A3: 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 A2, CARD_2:53; 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 A3, 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:63 .= 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 A1: MemberFunc (X /\ Y, A).x <= MemberFunc (X, A).x by Th49; MemberFunc (X /\ Y, A).x <= MemberFunc (Y, A).x by Th49; hence thesis by A1, SQUARE_1:39; 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 Seg len X holds z.j = F(j) from SeqLambdaD; then consider z being FinSequence of REAL such that A1: len z = len X & for j being Nat st j in Seg len X 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 n in Seg len X by FINSEQ_1:def 3; hence thesis by A1; end; uniqueness proof let A1, A2 be FinSequence of REAL such that A2: dom A1 = dom X & for n being Nat st n in dom X holds A1.n = MemberFunc (X.n, A).x and A3: dom A2 = dom X & 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 A4: n in dom A1; then A1.n = MemberFunc (X.n, A).x by A2 .= A2.n by A2, A3, A4; hence thesis; end; hence thesis by A2, A3, FINSEQ_1:17; end; end; theorem Th53: for X being FinSequence of bool the carrier of A, x being Element of A, y being Element of bool the carrier 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 Element of bool the carrier 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:8; 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:56; A3: 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:56; 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 k in dom (X^<*y*>) by Def10; then A5: p.k = MemberFunc ((X^<*y*>).k, A).x by Def10; A6: k <= len X + 1 by A4, A2, FINSEQ_1:3; A7: 1 <= k by A4, FINSEQ_3:27; per cases by A6, NAT_1:26; suppose A8: k <= len X; then A9: k in dom X by A7, FINSEQ_3:27; k in dom FinSeqM (x, X) by A7, A8, A1, FINSEQ_3:27; then q.k = FinSeqM (x, X).k by FINSEQ_1:def 7 .= MemberFunc (X.k, A).x by A9, Def10; hence thesis by A9, A5, FINSEQ_1:def 7; suppose A10: k = len X + 1; then q.k = MemberFunc (y, A).x by A1, FINSEQ_1:59; hence thesis by A5, FINSEQ_1:59, A10; end; hence thesis by A3, A2, FINSEQ_1:17; end; theorem Th54: MemberFunc ({}A, A).x = 0 proof UAp {}A = {} by Th19; then A1: (UAp {}A)` = [#] A by PRE_TOPC:27; x in the carrier of A; then x in (UAp {}A)` by A1, PRE_TOPC:12; 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: P[<*> bool the carrier of A] proof assume <*> bool the carrier of A is disjoint_valued; set F = FinSeqM (x, <*> bool the carrier of A); dom F = dom <*> bool the carrier of A by Def10; then A2: Sum F = 0 by RVSUM_1:102, RELAT_1:64, RELAT_1:60; Union <*> bool the carrier of A = {}A by CARD_3:14; hence thesis by A2, Th54; end; A3: for p being FinSequence of bool the carrier of A for y being Element of bool the carrier of A st P[p] holds P[p^<*y*>] proof let p be FinSequence of bool the carrier of A; let y be Element of bool the carrier of A; assume A4: P[p]; P[p^<*y*>] proof assume A5: p^<*y*> is disjoint_valued; A6: p c= p^<*y*> by FINSEQ_6:12; A7: Union (p^<*y*>) = Union p \/ Union <*y*> by Th5 .= Union p \/ y by FUNCT_6:39; A8: Union p misses y proof assume Union p meets y; then consider x being set such that A9: x in Union p & x in y by XBOOLE_0:3; x in union rng p by A9, PROB_1:def 3; then consider X being set such that A10: x in X & X in rng p by TARSKI:def 4; consider m being set such that A11: m in dom p & X = p.m by A10, FUNCT_1:def 5; reconsider m as Nat by A11; A12: p.m meets y by A9, A10, A11, XBOOLE_0:3; A13: (p^<*y*>).m = p.m by A11, FINSEQ_1:def 7; A14: (p^<*y*>).(len p + 1) = y by FINSEQ_1:59; A15: len p < len p + 1 by NAT_1:38; m <= len p by A11, FINSEQ_3:27; hence thesis by A12, A13, A14, A5, PROB_2:def 3, A15; end; MemberFunc (Union (p^<*y*>), A).x = MemberFunc (Union p, A).x + MemberFunc (y, A).x by A7, A8, Th51 .= Sum (FinSeqM (x, p) ^ <* MemberFunc (y, A).x *>) by RVSUM_1:104, A4, A6, A5, Th6 .= Sum FinSeqM (x, p ^ <*y*>) by Th53; hence thesis; end; hence thesis; end; for p being FinSequence of bool the carrier of A holds P[p] from IndSeqD (A1,A3); 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 set; assume A1: y in LAp X; then reconsider y' = y as Element of A; MemberFunc (X, A).y' = 1 by A1, Th40; hence thesis; end; let y be set; assume y in { x where x is Element of A : MemberFunc (X, A).x = 1 }; then consider y' being Element of A such that A2: y' = y & MemberFunc (X, A).y' = 1; thus thesis by A2, 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 set; assume A1: y in UAp X; then reconsider y' = y as Element of A; not y in (UAp X)` by A1, SUBSET_1:54; then MemberFunc (X, A).y' <> 0 by Th41; then MemberFunc (X, A).y' > 0 by Th38; hence thesis; end; let y be set; assume y in { x where x is Element of A : MemberFunc (X, A).x > 0 }; then consider y' being Element of A such that A2: y' = y & MemberFunc (X, A).y' > 0; not y in (UAp X)` by A2, Th41; hence thesis by A2, KURATO_2:1; 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 set; assume A1: y in BndAp X; then reconsider y' = y as Element of A; A2: 0 < MemberFunc (X, A).y' by A1, Th42; MemberFunc (X, A).y' < 1 by A1, Th42; hence thesis by A2; end; let y be set; assume y in { x where x is Element of A : 0 < MemberFunc (X, A).x & MemberFunc (X, A).x < 1 }; then consider y' being Element of A such that A3: y' = y & 0 < MemberFunc (X, A).y' & MemberFunc (X, A).y' < 1; thus thesis by A3, 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 :Def11: LAp X c= LAp Y; pred X c=^ Y means :Def12: UAp X c= UAp Y; end; definition let A be Tolerance_Space, X, Y be Subset of A; pred X _c=^ Y means :Def13: X _c= Y & X c=^ Y; 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 by Def11; then LAp X c= LAp Z by XBOOLE_1:1; hence thesis by Def11; 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 by Def12; then UAp X c= UAp Z by XBOOLE_1:1; hence thesis by Def12; end; theorem X _c=^ Y & Y _c=^ Z implies X _c=^ Z proof assume X _c=^ Y & Y _c=^ Z; then X _c= Y & Y _c= Z & X c=^ Y & Y c=^ Z by Def13; then X _c= Z & X c=^ Z by Th59, Th60; hence thesis by Def13; end; begin :: Rough Equality of Sets definition let A be Tolerance_Space, X, Y be Subset of A; pred X _= Y means :Def14: LAp X = LAp Y; reflexivity; symmetry; pred X =^ Y means :Def15: UAp X = UAp Y; reflexivity; symmetry; pred X _=^ Y means :Def16: 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 hereby assume X _= Y; then LAp X = LAp Y by Def14; hence X _c= Y & Y _c= X by Def11; end; assume X _c= Y & Y _c= X; then LAp X c= LAp Y & LAp Y c= LAp X by Def11; then LAp X = LAp Y by XBOOLE_0:def 10; hence thesis by Def14; end; redefine pred X =^ Y means X c=^ Y & Y c=^ X; compatibility proof hereby assume X =^ Y; then UAp X = UAp Y by Def15; hence X c=^ Y & Y c=^ X by Def12; end; assume X c=^ Y & Y c=^ X; then UAp X c= UAp Y & UAp Y c= UAp X by Def12; then UAp X = UAp Y by XBOOLE_0:def 10; hence thesis by Def15; end; redefine pred X _=^ Y means X _= Y & X =^ Y; compatibility proof hereby assume X _=^ Y; then LAp X = LAp Y & UAp X = UAp Y by Def16; hence X _= Y & X =^ Y by Def15, Def14; end; assume X _= Y & X =^ Y; then LAp X = LAp Y & UAp X = UAp Y by Def15, Def14; hence thesis by Def16; end; end;