:: Boolean Properties of Sets - Definitions
::  by Library Committee
::
:: Received April 6, 2002
:: Copyright (c) 2002-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 TARSKI, XBOOLE_0, MATROID0, AOFA_000;
 notations TARSKI;
 constructors TARSKI;


begin

reserve X, Y, Z for set, x, y, z for object;

scheme :: XBOOLE_0:sch 1
  Separation { A()-> set, P[object] } :
  ex X being set st for x holds x in X iff x in A() & P[x];

definition
  let X be set;
  attr X is empty means
:: XBOOLE_0:def 1

  not ex x st x in X;
end;

registration
  cluster empty for set;
end;

definition
  func {} -> set equals
:: XBOOLE_0:def 2
the empty set;
  let X,Y be set;
  func X \/ Y -> set means
:: XBOOLE_0:def 3

  for x holds x in it iff x in X or x in Y;
  commutativity;
  idempotence;
  func X /\ Y -> set means
:: XBOOLE_0:def 4

  for x holds x in it iff x in X & x in Y;
  commutativity;
  idempotence;
  func X \ Y -> set means
:: XBOOLE_0:def 5

  for x holds x in it iff x in X & not x in Y;
end;

definition
  let X, Y be set;
  func X \+\ Y -> set equals
:: XBOOLE_0:def 6
  (X \ Y) \/ (Y \ X);
  commutativity;
  pred X misses Y means
:: XBOOLE_0:def 7

  X /\ Y = {};
  symmetry;
  pred X c< Y means
:: XBOOLE_0:def 8

  X c= Y & X <> Y;
  irreflexivity;
  asymmetry;
  pred X,Y are_c=-comparable means
:: XBOOLE_0:def 9
  X c= Y or Y c= X;
  reflexivity;
  symmetry;
  redefine pred X = Y means
:: XBOOLE_0:def 10
  X c= Y & Y c= X;
end;

notation
  let X, Y be set;
  antonym X meets Y for X misses Y;
end;

theorem :: XBOOLE_0:1
  x in X \+\ Y iff not (x in X iff x in Y);

theorem :: XBOOLE_0:2
  (for x holds not x in X iff (x in Y iff x in Z)) implies X = Y \+\ Z;

registration
  cluster {} -> empty;
end;

registration
  let x;
  cluster { x } -> non empty;
  let y;
  cluster { x, y } -> non empty;
end;

registration
  cluster non empty for set;
end;

registration
  let D be non empty set, X be set;
  cluster D \/ X -> non empty;
  cluster X \/ D -> non empty;
end;

theorem :: XBOOLE_0:3
  X meets Y iff ex x st x in X & x in Y;

theorem :: XBOOLE_0:4
  X meets Y iff ex x st x in X /\ Y;

theorem :: XBOOLE_0:5
  X misses Y & x in X \/ Y implies x in X & not x in Y or x in Y & not x in X;

scheme :: XBOOLE_0:sch 2
  Extensionality { X,Y() -> set, P[object] } :
  X() = Y()
provided
 for x holds x in X() iff P[x] and
 for x holds x in Y() iff P[x];

scheme :: XBOOLE_0:sch 3
  SetEq { P[object] } :
  for X1,X2 being set st
    (for x holds x in X1 iff P[x]) &
    (for x holds x in X2 iff P[x]) holds X1 = X2;

begin :: Addenda
:: from RLSUB_2, 2006.12.02, AT

theorem :: XBOOLE_0:6
  X c< Y implies ex x st x in Y & not x in X;

:: 2008.08.07, A.T.

theorem :: XBOOLE_0:7
  X <> {} implies ex x st x in X;

:: 2012.10.08, A.T.

theorem :: XBOOLE_0:8
 X c< Y implies ex x st x in Y & X c= Y \ {x};

:: from MATROID0, 2013.01.18, A.T.

notation
  let x,y be set;
  antonym x c/= y for x c= y;
end;

:: from AOFA_000, 2013.01.18, A.T.

notation
  let x be object,y be set;
  antonym x nin y for x in y;
end;