:: Finite Sets
::  by Agata Darmochwa\l
::
:: Received April 6, 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 FUNCT_1, RELAT_1, ORDINAL1, XBOOLE_0, FUNCOP_1, ORDINAL3,
      ORDINAL2, TARSKI, SUBSET_1, SETFAM_1, ZFMISC_1, MCART_1, FUNCT_4,
      FINSET_1, MATROID0, CARD_1;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, RELAT_1, FUNCT_1,
      FUNCOP_1, MCART_1, SETFAM_1, ORDINAL1, ORDINAL2, ORDINAL3, SUBSET_1,
      DOMAIN_1, RELSET_1, FUNCT_2, FUNCT_3, FUNCT_4;
 constructors DOMAIN_1, FUNCT_3, FUNCOP_1, ORDINAL3, FUNCT_4, SETFAM_1,
      RELSET_1, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, ORDINAL2,
      RELSET_1, FUNCOP_1, XTUPLE_0;
 requirements SUBSET, BOOLE, NUMERALS;


begin

definition
  let IT be set;
  attr IT is finite means
:: FINSET_1:def 1

  ex p being Function st rng p = IT & dom p in omega;
end;

notation
  let IT be set;
  antonym IT is infinite for IT is finite;
end;

reserve A, B, X, Y, Z, x, y for set;
reserve f for Function;

registration
  cluster non empty finite for set;
end;

registration
  cluster empty -> finite for set;
end;

scheme :: FINSET_1:sch 1
 OLambdaC{A()->set,C[object],F,G(object)->object}:
  ex f being Function st dom f = A() & for x being Ordinal st x in A() holds
  (C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x));

registration
  let x be object;
  cluster {x} -> finite;
end;

registration
  let x,y be object;
  cluster {x,y} -> finite;
end;

registration
  let x,y,z be object;
  cluster {x,y,z} -> finite;
end;

registration
  let x1,x2,x3,x4 be object;
  cluster {x1,x2,x3,x4} -> finite;
end;

registration
  let x1,x2,x3,x4,x5 be object;
  cluster {x1,x2,x3,x4,x5} -> finite;
end;

registration
  let x1,x2,x3,x4,x5,x6 be object;
  cluster {x1,x2,x3,x4,x5,x6} -> finite;
end;

registration
  let x1,x2,x3,x4,x5,x6,x7 be object;
  cluster {x1,x2,x3,x4,x5,x6,x7} -> finite;
end;

registration
  let x1,x2,x3,x4,x5,x6,x7,x8 be object;
  cluster {x1,x2,x3,x4,x5,x6,x7,x8} -> finite;
end;

registration
  let B be finite set;
  cluster -> finite for Subset of B;
end;

registration
  let X,Y be finite set;
  cluster X \/ Y -> finite;
end;

theorem :: FINSET_1:1
  A c= B & B is finite implies A is finite;

theorem :: FINSET_1:2
  A is finite & B is finite implies A \/ B is finite;

registration
  let A be set, B be finite set;
  cluster A /\ B -> finite;
end;

registration
  let A be finite set, B be set;
  cluster A /\ B -> finite;
  cluster A \ B -> finite;
end;

theorem :: FINSET_1:3
  A is finite implies A /\ B is finite;

theorem :: FINSET_1:4
  A is finite implies A \ B is finite;

registration
  let f be Function, A be finite set;
  cluster f.:A -> finite;
end;

theorem :: FINSET_1:5
  A is finite implies f.:A is finite;

reserve O for Ordinal;

theorem :: FINSET_1:6
  A is finite implies for X being Subset-Family of A st X <> {}
  ex x being set st x in X &
    for B being set st B in X holds x c= B implies B = x;

scheme :: FINSET_1:sch 2
 Finite{A()->set,P[set]} : P[A()]
provided
 A() is finite and
 P[{}] and
 for x,B being set st x in A() & B c= A() & P[B] holds P[B \/ {x}];

registration
  let A,B be finite set;
  cluster [:A,B:] -> finite;
end;

registration
  let A,B,C be finite set;
  cluster [:A,B,C:] -> finite;
end;

registration
  let A,B,C,D be finite set;
  cluster [:A,B,C,D:] -> finite;
end;

registration
  let A be finite set;
  cluster bool A -> finite;
end;

theorem :: FINSET_1:7
  A is finite & (for X st X in A holds X is finite) iff union A is finite;

theorem :: FINSET_1:8
  dom f is finite implies rng f is finite;

theorem :: FINSET_1:9
  Y c= rng f & f"Y is finite implies Y is finite;

registration
  let X, Y be finite set;
  cluster X \+\ Y -> finite;
end;

registration
  let X be set;
  cluster finite for Subset of X;
end;

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

begin :: Addenda
:: from AMI_1

theorem :: FINSET_1:10
  for f being Function holds dom f is finite iff f is finite;

:: from ALI2

theorem :: FINSET_1:11
  for F being set st F is finite & F <> {} & F is c=-linear
  ex m being set st m in F & for C being set st C in F holds m c= C;

:: from FIN_TOPO

theorem :: FINSET_1:12
  for F being set st F is finite & F <> {} & F is c=-linear
  ex m being set st m in F & for C being set st C in F holds C c= m;

:: 2006.08.25, A.T.

definition
  let R be Relation;
  attr R is finite-yielding means
:: FINSET_1:def 2

  for x being set st x in rng R holds x is finite;
end;

:: from CQC_THE1, 2007.03.15, A.T.

reserve a for set;

theorem :: FINSET_1:13
  X is finite & X c= [:Y,Z:] implies
  ex A,B being set st A is finite & A c= Y & B is finite & B c= Z &
  X c= [:A,B:];

theorem :: FINSET_1:14
  X is finite & X c= [:Y,Z:] implies
  ex A being set st A is finite & A c= Y & X c= [:A,Z:];

:: restored, 2007.07.22, A.T.

registration
  cluster finite non empty for Function;
end;

registration
  let R be finite Relation;
  cluster dom R -> finite;
end;

:: from SCMFSA_4, 2007.07.22, A.T.

registration
  let f be Function, g be finite Function;
  cluster f*g -> finite;
end;

:: from SF_MASTR, 2007.07.25, A.T.

registration
  let A be finite set, B be set;
  cluster -> finite for Function of A, B;
end;

:: from GLIB_000, 2007.10.24, A.T.

registration
  let x,y be object;
  cluster x .--> y -> finite;
end;

:: from FINSEQ_1, 2008.02.19, A.T.

registration
  let R be finite Relation;
  cluster rng R -> finite;
end;

:: from FINSEQ_1, 2008.05.06, A.T.

registration
  let f be finite Function, x be set;
  cluster f"x -> finite;
end;

registration
  let f, g be finite Function;
  cluster f +* g -> finite;
end;

:: from COMPTS_1, 2008.07.16, A.T

definition
  let F be set;
  attr F is centered means
:: FINSET_1:def 3
  F <> {} &
  for G being set st G <> {} & G c= F & G is finite holds meet G <> {};
end;

definition
 let f be Function;
  redefine attr f is finite-yielding means
:: FINSET_1:def 4
 for i being object st i in dom f holds f.i is finite;
end;

:: from PRE_CIRC, 2009.03.04, A.T.

definition
  let I be set;
  let IT be I-defined Function;
  redefine attr IT is finite-yielding means
:: FINSET_1:def 5
  for i being object st i in I holds IT.i is finite;
end;

:: new, 2009.08.26, A.T

theorem :: FINSET_1:15
  B is infinite implies not B in [:A,B:];

:: new, 2009.09.30, A.T.

registration
 let I be set, f be I-defined Function;
 cluster finite I-defined f-compatible for Function;
end;

registration
 let X,Y be set;
 cluster finite X-defined Y-valued for Function;
end;

registration
 let X,Y be non empty set;
 cluster X-defined Y-valued non empty finite for Function;
end;

registration
  let A be set, F be finite Relation;
  cluster A|`F -> finite;
end;

registration
  let A be set, F be finite Relation;
  cluster F|A -> finite;
end;

registration
  let A be finite set, F be Function;
  cluster F|A -> finite;
end;

registration
  let R be finite Relation;
  cluster field R -> finite;
end;

registration
  cluster trivial -> finite for set;
end;

registration
  cluster infinite -> non trivial for set;
end;

registration
  let X be non trivial set;
  cluster finite non trivial for Subset of X;
end;

:: 2011.04.07, A.T,

registration
  let x,y,a,b be object;
  cluster (x,y) --> (a,b) -> finite;
end;

:: from MATROID0, 2011.07.25, A.T.

definition
  let A be set;
  attr A is finite-membered means
:: FINSET_1:def 6
 for B being set st B in A holds B is finite;
end;

registration
 cluster empty -> finite-membered for set;
end;

registration
  let A be finite-membered set;
  cluster -> finite for Element of A;
end;

registration
  cluster non empty finite finite-membered for set;
end;

:: from SIMPLEX0, 2011.07.25, A.T.

registration
  let X be finite set;
  cluster {X} -> finite-membered;
  cluster bool X -> finite-membered;
  let Y be finite set;
  cluster {X,Y} -> finite-membered;
end;

registration
  let X be finite-membered set;
  cluster -> finite-membered for Subset of X;
  let Y be finite-membered set;
  cluster X \/ Y -> finite-membered;
end;

registration
  let X be finite finite-membered set;
  cluster union X -> finite;
end;

registration
  cluster non empty finite-yielding for Function;
  cluster empty -> finite-yielding for Relation;
end;

registration
  let F be finite-yielding Function, x be object;
  cluster F.x -> finite;
end;

registration let F be finite-yielding Relation;
 cluster rng F -> finite-membered;
end;