The Mizar article:

Basic Properties of Rough Sets and Rough Membership Function

by
Adam Grabowski

Received November 23, 2003

Copyright (c) 2003 Association of Mizar Users

MML identifier: ROUGHS_1
[ MML identifier index ]


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;

Back to top