:: Equivalence Relations and Classes of Abstraction
::  by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received November 16, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, RELAT_1, ZFMISC_1, SETFAM_1, TARSKI, PARTFUN1,
      RELAT_2, XBOOLE_0, FINSEQ_1, XXREAL_0, FUNCT_1, ARYTM_3, ORDINAL4,
      ARYTM_1, NAT_1, CARD_1, EQREL_1, MCART_1, CARD_3;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, MCART_1, DOMAIN_1, SUBSET_1,
      XCMPLX_0, XXREAL_0, RELAT_1, RELAT_2, SETFAM_1, FINSEQ_1, FUNCT_1,
      ORDINAL1, NUMBERS, NAT_1, FUNCT_3, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1;
 constructors SETFAM_1, RELAT_2, PARTFUN1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1,
      RELSET_1, FUNCT_3, BINOP_1, DOMAIN_1, XTUPLE_0, NUMBERS;
 registrations XBOOLE_0, SUBSET_1, PARTFUN1, XXREAL_0, XREAL_0, FINSEQ_1,
      RELAT_1, ORDINAL1, RELSET_1, FUNCT_2, ZFMISC_1, FUNCT_1, RELAT_2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve X,Y,Z for set, x,y,z for object;
reserve i,j for Nat;
reserve A,B,C for Subset of X;
reserve R,R1,R2 for Relation of X;
reserve AX for Subset of [:X,X:];
reserve SFXX for Subset-Family of [:X,X:];

:: Equivalence Relation and its properties

definition
  let X;
  func nabla X -> Relation of X equals
:: EQREL_1:def 1
  [:X,X:];
end;

registration
  let X;
  cluster nabla X -> total reflexive;
end;

definition
  let X,R1,R2;
  redefine func R1 /\ R2 -> Relation of X;
  redefine func R1 \/ R2 -> Relation of X;
end;

theorem :: EQREL_1:1
  nabla X \/ R1 = nabla X;

theorem :: EQREL_1:2
  id X is_reflexive_in X & id X is_symmetric_in X & id X is_transitive_in X;

definition
  let X;
  mode Tolerance of X is total reflexive symmetric Relation of X;
  mode Equivalence_Relation of X is total symmetric transitive Relation of X;
end;

theorem :: EQREL_1:3
  id X is Equivalence_Relation of X;

theorem :: EQREL_1:4
  nabla X is Equivalence_Relation of X;

registration
  let X;
  cluster nabla X -> total symmetric transitive;
end;

reserve EqR,EqR1,EqR2,EqR3 for Equivalence_Relation of X;

theorem :: EQREL_1:5
  for R being total reflexive Relation of X holds x in X implies [x,x] in R;

theorem :: EQREL_1:6
  for X being set, x,y being object, R being symmetric Relation of X
  st [x,y] in R holds [y,x] in R;

theorem :: EQREL_1:7
  for R being total transitive Relation of X
  for x,y being object
  holds [x,y] in R & [y,z] in R implies [x,z] in R;

theorem :: EQREL_1:8
  for R being total reflexive Relation of X holds
  (ex x being set st x in X) implies R <> {};

theorem :: EQREL_1:9
  R is Equivalence_Relation of X iff
    R is reflexive symmetric transitive & field R = X;

definition
  let X,EqR1,EqR2;
  redefine func EqR1 /\ EqR2 -> Equivalence_Relation of X;
end;

theorem :: EQREL_1:10
  id X /\ EqR = id X;

theorem :: EQREL_1:11
  for SFXX st (SFXX <> {} & for Y st Y in SFXX holds Y is
  Equivalence_Relation of X) holds meet SFXX is Equivalence_Relation of X;

theorem :: EQREL_1:12
  for R holds ex EqR st R c= EqR & for EqR2 st R c= EqR2 holds EqR c= EqR2;

definition
  let X;
  let EqR1,EqR2;
  func EqR1 "\/" EqR2 -> Equivalence_Relation of X means
:: EQREL_1:def 2

  EqR1 \/ EqR2 c= it & for EqR st EqR1 \/ EqR2 c= EqR holds it c= EqR;
  commutativity;
  idempotence;
end;

theorem :: EQREL_1:13
  (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3);

theorem :: EQREL_1:14
  EqR "\/" EqR = EqR;

theorem :: EQREL_1:15
  EqR1 "\/" EqR2 = EqR2 "\/" EqR1;

theorem :: EQREL_1:16
  EqR1 /\ (EqR1 "\/" EqR2) = EqR1;

theorem :: EQREL_1:17
  EqR1 "\/" (EqR1 /\ EqR2) = EqR1;

scheme :: EQREL_1:sch 1
  ExEqRel {X() -> set,P[object,object]}:
ex EqR being Equivalence_Relation of X() st
  for x,y holds [x,y] in EqR iff x in X() & y in X() & P[x,y]
provided
 for x st x in X() holds P[x,x] and
 for x,y st P[x,y] holds P[y,x] and
 for x,y,z st P[x,y] & P[y,z] holds P[x,z];

:: Classes of abstraction

notation
  let R be Relation, x be object;
  synonym Class(R,x) for Im(R,x);
end;

definition
  let X, Y be set, R be Relation of X, Y, x be object;
  redefine func Class(R,x) -> Subset of Y;
end;

theorem :: EQREL_1:18
  for R being Relation holds y in Class (R,x) iff [x,y] in R;

theorem :: EQREL_1:19
  for R being total symmetric Relation of X holds y in Class (R,x)
  iff [y,x] in R;

theorem :: EQREL_1:20
  for R being Tolerance of X holds for x st x in X holds x in Class (R,x);

theorem :: EQREL_1:21
  for R being Tolerance of X holds for x st x in X holds
  ex y st x in Class(R,y);

theorem :: EQREL_1:22
  for R being transitive Tolerance of X holds y in Class(R,x) & z in
  Class(R,x) implies [y,z] in R;

theorem :: EQREL_1:23
  for x st x in X holds y in Class(EqR,x) iff Class(EqR,x) = Class (EqR,y);

theorem :: EQREL_1:24
  for x,y st y in X holds
  Class(EqR,x) = Class(EqR,y) or Class(EqR,x) misses Class(EqR,y);

theorem :: EQREL_1:25
  for x st x in X holds Class(id X,x) = {x};

theorem :: EQREL_1:26
  for x st x in X holds Class(nabla X,x) = X;

theorem :: EQREL_1:27
  (ex x st Class(EqR,x) = X) implies EqR = nabla X;

theorem :: EQREL_1:28
  x in X implies ([x,y] in EqR1 "\/" EqR2 iff ex f being FinSequence st
1 <= len f & x = f.1 & y = f.(len f) & for i st 1 <= i & i < len f holds [f.i,f
  .(i+1)] in EqR1 \/ EqR2);

theorem :: EQREL_1:29
  for E being Equivalence_Relation of X st E = EqR1 \/ EqR2 holds
for x st x in X holds Class(E,x) = Class(EqR1,x) or Class(E,x) = Class(EqR2,x);

theorem :: EQREL_1:30
  EqR1 \/ EqR2 = nabla X implies EqR1 = nabla X or EqR2 = nabla X;

definition
  let X, EqR;
  func Class EqR -> Subset-Family of X means
:: EQREL_1:def 3

  A in it iff ex x st x in X & A = Class(EqR,x);
end;

theorem :: EQREL_1:31
  X = {} implies Class EqR = {};

definition
  let X;
  mode a_partition of X -> Subset-Family of X means
:: EQREL_1:def 4
    union it = X &
    for A st A in it holds A<>{} & for B st B in it holds A = B or A misses B;
end;

theorem :: EQREL_1:32
  for P being a_partition of {} holds P = {};

registration let X be empty set;
  cluster -> empty for a_partition of X;
end;

registration let X be empty set;
  cluster empty for a_partition of X;
end;

theorem :: EQREL_1:33
  Class EqR is a_partition of X;

theorem :: EQREL_1:34
  for P being a_partition of X holds ex EqR st P = Class EqR;

theorem :: EQREL_1:35
  for x st x in X holds [x,y] in EqR iff Class(EqR,x) = Class(EqR,y);

theorem :: EQREL_1:36
  x in Class EqR implies ex y being Element of X st x = Class(EqR,y);

begin :: Addenda
:: from FSM_1, PARTIT1, 2005.02.06, A.T.

registration
  let X be non empty set;
  cluster -> non empty for a_partition of X;
end;

:: from PUA2MSS1

registration
  let X be set;
  cluster -> with_non-empty_elements for a_partition of X;
end;

definition
  let X be set, R be Equivalence_Relation of X;
  redefine func Class R -> a_partition of X;
end;

:: from PRALG_3

registration
  let I be non empty set, R be Equivalence_Relation of I;
  cluster Class R -> non empty;
end;

registration
  let I be non empty set, R be Equivalence_Relation of I;
  cluster Class R -> with_non-empty_elements;
end;

notation
  let I be non empty set, R be Equivalence_Relation of I;
  let x be Element of I;
  synonym EqClass(R,x) for Class(R,x);
end;

definition
  let I be non empty set, R be Equivalence_Relation of I;
  let x be Element of I;
  redefine func EqClass(R,x) -> Element of Class R;
end;

definition
  let X be set;
  func SmallestPartition X -> set equals
:: EQREL_1:def 5
  Class id X;
end;

definition
  let X be set;
  redefine func SmallestPartition X -> a_partition of X;
end;

theorem :: EQREL_1:37
  for X being non empty set holds
    SmallestPartition X = the set of all {x} where x is Element of X;

:: from T_1TOPSP, 30.12.2006, AK
:: Classes of partitions of a set

reserve X for non empty set,
  x for Element of X;

definition
  let X be non empty set,x be Element of X,S1 be a_partition of X;
  func EqClass(x,S1) -> Subset of X means
:: EQREL_1:def 6

  x in it & it in S1;
end;

theorem :: EQREL_1:38
  for S1,S2 being a_partition of X st (for x being Element of X
  holds EqClass(x,S1) = EqClass(x,S2)) holds S1=S2;

theorem :: EQREL_1:39
  for X being non empty set holds {X} is a_partition of X;

definition
  let X be set;
  mode Family-Class of X is Subset-Family of bool X;
end;

definition
  let X be set;
  let F be Family-Class of X;
  attr F is partition-membered means
:: EQREL_1:def 7
  for S being set st S in F holds S is a_partition of X;
end;

registration
  let X be set;
  cluster partition-membered for Family-Class of X;
end;

definition
  let X be set;
  mode Part-Family of X is partition-membered Family-Class of X;
end;

reserve F for Part-Family of X;

registration
  let X be non empty set;
  cluster non empty for a_partition of X;
end;

theorem :: EQREL_1:40
  for X being set, p being a_partition of X holds {p} is Part-Family of X;

registration
  let X be set;
  cluster non empty for Part-Family of X;
end;

theorem :: EQREL_1:41
  for S1 being a_partition of X, x,y being Element of X holds
  EqClass(x,S1) meets EqClass(y,S1) implies EqClass(x,S1) = EqClass(y,S1);

theorem :: EQREL_1:42
  for A being set,X being non empty set,S being a_partition of X holds A
  in S implies ex x being Element of X st A = EqClass(x,S);

definition
  let X be non empty set,F be non empty Part-Family of X;
  func Intersection F -> non empty a_partition of X means
:: EQREL_1:def 8
  for x being Element
of X holds EqClass(x,it) = meet{EqClass(x,S) where S is a_partition of X : S in
  F};
end;

theorem :: EQREL_1:43
  for X being non empty set, S being a_partition of X,
      A being Subset of S holds (union S) \ (union A) = union (S \ A);

theorem :: EQREL_1:44
  for X being non empty set,A being Subset of X, S being a_partition of
  X holds A in S implies union(S \ {A}) = X \ A;

:: Added 2007.10.17, AK

registration
  let A be empty set;
  cluster -> empty for a_partition of A;
end;

theorem :: EQREL_1:45
  {} is a_partition of {};

registration
  let A be empty set;
  cluster empty for a_partition of A;
end;

begin :: Moved from BORSUK_1, 2010.03.15, A.T.

reserve e,u,v for object, E,X,Y,X1 for set;

theorem :: EQREL_1:46
  for F being Function st X c= F"X1 holds F.:X c= X1;

theorem :: EQREL_1:47
  E c= [:X,Y:] implies (.:pr1(X,Y)).E = pr1(X,Y).:E;

theorem :: EQREL_1:48
  E c= [:X,Y:] implies (.:pr2(X,Y)).E = pr2(X,Y).:E;

theorem :: EQREL_1:49
  for X1 being Subset of X, Y1 being Subset of Y st [:X1,Y1:] <>
  {} holds pr1(X,Y).:[:X1,Y1:] = X1 & pr2(X,Y).:[:X1,Y1:] = Y1;

theorem :: EQREL_1:50
  for X1 being Subset of X, Y1 being Subset of Y st [:X1,Y1:] <>
  {} holds .:pr1(X,Y). [:X1,Y1:] = X1 & .:pr2(X,Y). [:X1,Y1:] = Y1;

theorem :: EQREL_1:51
  for A being Subset of [:X,Y:], H being Subset-Family of [:X,Y:]
st for E st E in H holds E c= A &
    ex X1 being Subset of X, Y1 being Subset of Y
  st E =[:X1,Y1:] holds [:union(.:pr1(X,Y).:H), meet(.:pr2(X,Y).:H):] c= A;

theorem :: EQREL_1:52
  for A being Subset of [:X,Y:], H being Subset-Family of [:X,Y:] st for E
 st E in H holds E c= A & ex X1 being Subset of X, Y1 being Subset of Y
    st E = [:X1,Y1:]
  holds [:meet(.:pr1(X,Y).:H), union(.:pr2(X,Y).:H):] c= A;

theorem :: EQREL_1:53
  for X being set, Y being non empty set, f being Function of X,Y
  for H being Subset-Family of X holds union(.:f.:H) = f.: union H;

reserve X,Y,Z for non empty set;

theorem :: EQREL_1:54
  for X being set, a being Subset-Family of X holds union union a
  = union { union A where A is Subset of X: A in a };

theorem :: EQREL_1:55
  for X being set for D being Subset-Family of X st union D = X
for A being Subset of D, B being Subset of X st B = union A holds
  B` c= union A`;

theorem :: EQREL_1:56
  for F being Function of X,Y, G being Function of X,Z st
  for x,x9 being Element of X st F.x=F.x9 holds G.x=G.x9
  ex H being Function of Y,Z st H*F = G;

theorem :: EQREL_1:57
  for X,Y,Z for y being Element of Y, F being (Function of X,Y),
      G being Function of Y,Z holds F"{y} c= (G*F)"{G.y};

theorem :: EQREL_1:58
  for F being Function of X,Y, x being Element of X,
      z being Element of Z holds [:F,id Z:].(x,z) = [F.x,z];

theorem :: EQREL_1:59
  for F being Function of X,Y, A being Subset of X, B being Subset of Z
  holds [:F,id Z:].:[:A,B:] = [:F.:A,B:];

theorem :: EQREL_1:60
  for F being Function of X,Y, y being Element of Y,
      z being Element of Z holds [:F,id Z:]"{[y,z]} = [:F"{y},{z}:];

theorem :: EQREL_1:61
  for D being Subset-Family of X, A being Subset of D holds
    union A is Subset of X;

theorem :: EQREL_1:62
  for X being set, D being a_partition of X, A,B being Subset of D
  holds union(A /\ B) = union A /\ union B;

theorem :: EQREL_1:63
  for D being a_partition of X, A being Subset of D, B being
  Subset of X st B = union A holds B` = union A`;

theorem :: EQREL_1:64 :: Class(id X) is non-empty
  for E being Equivalence_Relation of X holds Class(E) is non empty;

definition
  let X;
  let D be non empty a_partition of X;
  func proj D -> Function of X, D means
:: EQREL_1:def 9

  for p being Element of X holds p in it.p;
end;

theorem :: EQREL_1:65
  for D being non empty a_partition of X, p being Element of X,
      A being Element of D st p in A holds A = (proj D).p;

theorem :: EQREL_1:66
  for D being non empty a_partition of X, p being Element of D
  holds p = proj D " {p};

theorem :: EQREL_1:67
  for D being non empty a_partition of X, A being Subset of D
  holds (proj D)"A = union A;

theorem :: EQREL_1:68
  for D being non empty a_partition of X, W being Element of D
  ex W9 being Element of X st proj(D).W9=W;

theorem :: EQREL_1:69
  for D being non empty a_partition of X, W being Subset of X st
for B being Subset of X st B in D & B meets W holds B c= W holds W = proj D " (
  proj D .: W);

theorem :: EQREL_1:70
  for X being set, P being a_partition of X, x, a, b being set st
    x in a & a in P & x in b & b in P holds a = b;