:: Properties of Binary Relations
::  by Edmund Woronowicz and Anna Zalewska
::
:: Received March 15, 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 RELAT_1, TARSKI, XBOOLE_0, ZFMISC_1, RELAT_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1;
 constructors TARSKI, SUBSET_1, RELAT_1, XTUPLE_0;
 registrations RELAT_1, XBOOLE_0;
 requirements BOOLE, SUBSET;


begin

reserve X for set, a,b,c,x,y,z for object;
reserve P,R for Relation;

definition
  let R,X;
  pred R is_reflexive_in X means
:: RELAT_2:def 1

  x in X implies [x,x] in R;
  pred R is_irreflexive_in X means
:: RELAT_2:def 2

  x in X implies not [x,x] in R;
  pred R is_symmetric_in X means
:: RELAT_2:def 3

  x in X & y in X & [x,y] in R implies [ y,x] in R;
  pred R is_antisymmetric_in X means
:: RELAT_2:def 4

  x in X & y in X & [x,y] in R & [y, x] in R implies x = y;
  pred R is_asymmetric_in X means
:: RELAT_2:def 5

  x in X & y in X & [x,y] in R implies not [y,x] in R;
  pred R is_connected_in X means
:: RELAT_2:def 6

  x in X & y in X & x <>y implies [x,y] in R or [y,x] in R;
  pred R is_strongly_connected_in X means
:: RELAT_2:def 7

  x in X & y in X implies [x,y] in R or [y,x] in R;
  pred R is_transitive_in X means
:: RELAT_2:def 8

  x in X & y in X & z in X & [x,y] in R & [y,z] in R implies [x,z] in R;
end;

definition
  let R;
  attr R is reflexive means
:: RELAT_2:def 9

  R is_reflexive_in field R;
  attr R is irreflexive means
:: RELAT_2:def 10

  R is_irreflexive_in field R;
  attr R is symmetric means
:: RELAT_2:def 11

  R is_symmetric_in field R;
  attr R is antisymmetric means
:: RELAT_2:def 12

  R is_antisymmetric_in field R;
  attr R is asymmetric means
:: RELAT_2:def 13

  R is_asymmetric_in field R;
  attr R is connected means
:: RELAT_2:def 14

  R is_connected_in field R;
  attr R is strongly_connected means
:: RELAT_2:def 15

  R is_strongly_connected_in field R;
  attr R is transitive means
:: RELAT_2:def 16

  R is_transitive_in field R;
end;

registration
  cluster empty -> reflexive irreflexive symmetric antisymmetric asymmetric
          connected strongly_connected transitive for Relation;
end;

theorem :: RELAT_2:1
  R is reflexive iff id field R c= R;

theorem :: RELAT_2:2
  R is irreflexive iff id field R misses R;

theorem :: RELAT_2:3
  R is_antisymmetric_in X iff R \ id X is_asymmetric_in X;

theorem :: RELAT_2:4
  R is_asymmetric_in X implies R \/ id X is_antisymmetric_in X;

::$CT 7

registration
  cluster symmetric transitive -> reflexive for Relation;
end;

registration
  let X;
  cluster id X -> symmetric transitive antisymmetric;
end;

registration
  cluster irreflexive transitive -> asymmetric for Relation;
  cluster asymmetric -> irreflexive antisymmetric for Relation;
end;

registration
  let R be reflexive Relation;
  cluster R~ -> reflexive;
end;

registration
  let R be irreflexive Relation;
  cluster R~ -> irreflexive;
end;

theorem :: RELAT_2:12
  R is reflexive implies dom R = dom(R~) & rng R = rng(R~);

theorem :: RELAT_2:13
  R is symmetric iff R = R~;

registration
  let P,R be reflexive Relation;
  cluster P \/ R -> reflexive;
  cluster P /\ R -> reflexive;
end;

registration
  let P,R be irreflexive Relation;
  cluster P \/ R -> irreflexive;
  cluster P /\ R -> irreflexive;
end;

registration
  let P be irreflexive Relation;
  let R be Relation;
  cluster P \ R -> irreflexive;
end;

registration
  let R be symmetric Relation;
  cluster R~ -> symmetric;
end;

registration
  let P,R be symmetric Relation;
  cluster P \/ R -> symmetric;
  cluster P /\ R -> symmetric;
  cluster P \ R -> symmetric;
end;

registration
  let R be asymmetric Relation;
  cluster R~ -> asymmetric;
end;

registration
  let P be Relation;
  let R be asymmetric Relation;
  cluster P /\ R -> asymmetric;
  cluster R /\ P -> asymmetric;
end;

registration
  let P be asymmetric Relation;
  let R be Relation;
  cluster P \ R -> asymmetric;
end;

::$CT 8

theorem :: RELAT_2:22
  R is antisymmetric iff R /\ (R~) c= id (dom R);

registration
  let R be antisymmetric Relation;
  cluster R~ -> antisymmetric;
end;

registration
  let P be antisymmetric Relation;
  let R be Relation;
  cluster P /\ R -> antisymmetric;
  cluster R /\ P -> antisymmetric;
  cluster P \ R -> antisymmetric;
end;

registration
  let R be transitive Relation;
  cluster R~ -> transitive;
end;

registration
  let P,R be transitive Relation;
  cluster P /\ R -> transitive;
end;

::$CT 4

theorem :: RELAT_2:27
  R is transitive iff R*R c= R;

theorem :: RELAT_2:28
  R is connected iff [:field R,field R:] \ id (field R) c= R \/ R~;

registration
  cluster strongly_connected -> connected reflexive for Relation;
end;

::$CT

theorem :: RELAT_2:30
  R is strongly_connected iff [:field R, field R:] = R \/ R~;

theorem :: RELAT_2:31
  R is transitive iff for x,y,z st [x,y] in R & [y,z] in R holds [x,z] in R;