:: The {H}all {M}arriage {T}heorem
:: by Ewa Romanowicz and Adam Grabowski
::
:: Received May 11, 2004
:: Copyright (c) 2004-2018 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, FINSET_1, CARD_1, XBOOLE_0, ARYTM_3, ARYTM_1, SUBSET_1,
XXREAL_0, NAT_1, RELAT_1, FINSEQ_1, ZFMISC_1, FUNCT_1, TARSKI, FUNCT_4,
HALLMAR1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, CARD_1,
ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, FINSET_1, FINSEQ_1,
FUNCT_2, FUNCT_7;
constructors REAL_1, NAT_1, FUNCT_7, RELSET_1, XREAL_0;
registrations SUBSET_1, RELAT_1, FUNCT_1, FINSET_1, XXREAL_0, XREAL_0,
FINSEQ_1, CHAIN_1, ORDINAL1, CARD_1, RELSET_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Preliminaries
theorem :: HALLMAR1:1
for X,Y being finite set holds card (X \/ Y) + card (X /\ Y) =
card X + card Y;
scheme :: HALLMAR1:sch 1
Regr11 { n() -> Element of NAT, P[set] }: for k be Element of NAT st 1 <= k
& k <= n() holds P[k]
provided
P[n()] & n() >= 2 and
for k be Element of NAT st 1 <= k & k < n() & P[k+1] holds P[k];
scheme :: HALLMAR1:sch 2
Regr2 { P[set] } : P[1]
provided
ex n be Element of NAT st n > 1 & P[n] and
for k be Element of NAT st k >= 1 & P[k+1] holds P[k];
registration
let F be non empty set;
cluster non empty non-empty for FinSequence of bool F;
end;
theorem :: HALLMAR1:2
for F being non empty set, f being non-empty FinSequence of bool
F, i being Element of NAT st i in dom f holds f.i <> {};
registration
let F be finite set, A be FinSequence of bool F;
let i be Element of NAT;
cluster A.i -> finite;
end;
begin :: Union of Finite Sequences
definition
let F be set;
let A be FinSequence of bool F;
let J be set;
func union (A, J) -> set means
:: HALLMAR1:def 1
:: Union(A|J) ??? !!!
for x being object holds x in it iff ex j
being set st j in J & j in dom A & x in A.j;
end;
theorem :: HALLMAR1:3
for F being set, A being FinSequence of bool F, J being set holds
union (A, J) c= F;
theorem :: HALLMAR1:4
for F being finite set, A being FinSequence of bool F, J, K being set
st J c= K holds union (A, J) c= union (A, K);
registration
let F be finite set;
let A be FinSequence of bool F;
let J be set;
cluster union (A, J) -> finite;
end;
theorem :: HALLMAR1:5
for F being finite set, A being FinSequence of bool F,
i being Element of NAT st i in dom A holds union (A, {i}) = A.i;
theorem :: HALLMAR1:6
for F being finite set, A being FinSequence of bool F,
i,j being Element of NAT st i in dom A & j in dom A holds
union (A, {i,j}) = A.i \/ A.j;
theorem :: HALLMAR1:7
for J being set, F being finite set, A being FinSequence of bool
F, i being Element of NAT st i in J & i in dom A holds A.i c= union (A, J);
theorem :: HALLMAR1:8
for J being set, F being finite set, i being Element of NAT,
A being FinSequence of bool F st
i in J & i in dom A holds union (A, J) = union (A, J \ {i}) \/ A.i;
theorem :: HALLMAR1:9
for J1, J2 being set, F being finite set, i being Element of NAT,
A being FinSequence of bool F st
i in dom A holds union (A,{i} \/ J1 \/ J2) = A.i \/ union (A,J1 \/ J2);
theorem :: HALLMAR1:10
for F being finite set, A being FinSequence of bool F
for i being Element of NAT
for x,y being set st x <> y & x in A.i & y in A.i holds
(A.i \ {x}) \/ (A.i \ {y}) = A.i;
begin :: Cut Operation for Finite Sequences
definition
let F be finite set;
let A be FinSequence of bool F;
let i be Element of NAT;
let x be set;
func Cut (A, i, x) -> FinSequence of bool F means
:: HALLMAR1:def 2
dom it = dom A & for k being Element of NAT st k in dom it holds
(i = k implies it.k = A.k \ {x}) &
(i <> k implies it.k = A.k);
end;
theorem :: HALLMAR1:11
for F being finite set, A being FinSequence of bool F,
i being Element of NAT, x being set st i in dom A & x in A.i holds
card (Cut (A,i,x).i) = card (A.i) - 1;
theorem :: HALLMAR1:12
for F being finite set, A being FinSequence of bool F,
i being Element of NAT, x,
J being set holds
union (Cut (A, i, x), J \ {i}) = union (A,J \ {i});
theorem :: HALLMAR1:13
for F being finite set, A being FinSequence of bool F,
i being Element of NAT,
x, J being set st not i in J holds
union (A, J) = union (Cut(A, i, x), J);
theorem :: HALLMAR1:14
for F being finite set, A being FinSequence of bool F,
i being Element of NAT, x,
J being set st i in dom Cut (A, i, x) & i in J holds
union (Cut (A, i, x), J) = union (A, J \ {i}) \/ (A.i \ {x});
begin :: System of Different Representatives and Hall Property
definition
let F be finite set;
let X be FinSequence of bool F;
let A be set;
pred A is_a_system_of_different_representatives_of X means
:: HALLMAR1:def 3
ex f being FinSequence of F st f = A & dom X = dom f &
(for i being Element of NAT st i in dom f holds f.i in X.i) &
f is one-to-one;
end;
definition
let F be finite set;
let A be FinSequence of bool F;
attr A is Hall means
:: HALLMAR1:def 4
for J being finite set st J c= dom A holds card J <= card union (A, J);
end;
registration let F be finite non empty set;
cluster Hall non empty for FinSequence of bool F;
end;
registration let F be finite set;
cluster Hall for FinSequence of bool F;
end;
theorem :: HALLMAR1:15
for F being finite set, A being non empty FinSequence of bool F
st A is Hall holds A is non-empty;
registration let F be finite set;
cluster Hall -> non-empty for non empty FinSequence of bool F;
end;
theorem :: HALLMAR1:16
for F being finite set, A being FinSequence of bool F,
i being Element of NAT st i in dom A & A is Hall holds
card (A.i) >= 1;
theorem :: HALLMAR1:17
for F being non empty finite set, A being non empty FinSequence of bool F st
(for i being Element of NAT st i in dom A holds card (A.i) = 1) &
A is Hall holds
ex X being set st X is_a_system_of_different_representatives_of A;
theorem :: HALLMAR1:18 :: SDR --> Hall
for F being finite set, A being FinSequence of bool F holds
(ex X being set st X is_a_system_of_different_representatives_of A)
implies A is Hall;
begin :: Reductions and Singlifications of Finite Sequences
definition
let F be set, A be FinSequence of bool F, i be Element of NAT;
mode Reduction of A, i -> FinSequence of bool F means
:: HALLMAR1:def 5
dom it = dom A &
(for j being Element of NAT st j in dom A & j <> i holds A.j = it.j) &
it.i c= A.i;
end;
definition
let F be set, A be FinSequence of bool F;
mode Reduction of A -> FinSequence of bool F means
:: HALLMAR1:def 6
dom it = dom A &
for i being Element of NAT st i in dom A holds it.i c= A.i;
end;
definition
let F be set, A be FinSequence of bool F, i be Nat;
assume that
i in dom A and
A.i <> {};
mode Singlification of A, i -> Reduction of A means
:: HALLMAR1:def 7
card (it.i) = 1;
end;
theorem :: HALLMAR1:19
for F being finite set, A being FinSequence of bool F,
i being Element of NAT,
C being Reduction of A, i holds C is Reduction of A;
theorem :: HALLMAR1:20
for F being finite set,
A being FinSequence of bool F, i being Element of NAT,
x being set st i in dom A holds Cut (A,i,x) is Reduction of A,i;
theorem :: HALLMAR1:21
for F being finite set, A being FinSequence of bool F,
i being Element of NAT,
x being set st i in dom A holds Cut (A,i,x) is Reduction of A;
theorem :: HALLMAR1:22
for F being finite set, A being FinSequence of bool F, B being Reduction of A
for C being Reduction of B holds C is Reduction of A;
theorem :: HALLMAR1:23
for F being non empty finite set, A being non-empty FinSequence of
bool F, i being Element of NAT, B being Singlification of A, i st i in dom A
holds B.i <> {};
theorem :: HALLMAR1:24
for F being non empty finite set, A being non-empty FinSequence
of bool F, i, j being Element of NAT, B being Singlification of A, i, C being
Singlification of B, j st i in dom A & j in dom A & C.i <> {} & B.j <> {} holds
C is Singlification of A, j & C is Singlification of A, i;
theorem :: HALLMAR1:25
for F being set, A being FinSequence of bool F, i being Element of NAT
holds A is Reduction of A,i;
theorem :: HALLMAR1:26
for F being set, A being FinSequence of bool F holds A is Reduction of A;
definition
let F be non empty set, A be FinSequence of bool F;
assume
A is non-empty;
mode Singlification of A -> Reduction of A means
:: HALLMAR1:def 8
for i being Element of NAT st i in dom A holds card (it.i) = 1;
end;
theorem :: HALLMAR1:27
for F being non empty finite set,
A being non empty non-empty FinSequence of bool F,
f being Function holds f is Singlification of A iff
(dom f = dom A &
for i being Element of NAT st i in dom A holds
f is Singlification of A, i);
registration
let F be non empty finite set, A be non empty FinSequence of bool F,
k be Element of NAT;
cluster -> non empty for Singlification of A, k;
end;
registration
let F be non empty finite set, A be non empty FinSequence of bool F;
cluster -> non empty for Singlification of A;
end;
begin :: Rado Proof of the Hall Marriage Theorem
theorem :: HALLMAR1:28
for F being non empty finite set, A being non empty FinSequence of bool F,
X being set, B being Reduction of A st
X is_a_system_of_different_representatives_of B holds
X is_a_system_of_different_representatives_of A;
theorem :: HALLMAR1:29 :: Rado Lemma
for F being finite set, A being FinSequence of bool F st A is Hall
for i being Element of NAT st card (A.i) >= 2
ex x being set st x in A.i & Cut (A, i, x) is Hall;
theorem :: HALLMAR1:30
for F being finite set, A being FinSequence of bool F,
i being Element of NAT st i in dom A & A is Hall holds
ex G being Singlification of A, i st G is Hall;
theorem :: HALLMAR1:31
for F being non empty finite set,
A being non empty FinSequence of bool F st A is Hall holds
ex G being Singlification of A st G is Hall;
::$N Hall Marriage Theorem
theorem :: HALLMAR1:32
for F being non empty finite set,
A being non empty FinSequence of bool F holds
(ex X being set st X is_a_system_of_different_representatives_of A) iff
A is Hall;