:: The {H}all {M}arriage {T}heorem
:: by Ewa Romanowicz and Adam Grabowski
::
:: Received May 11, 2004
:: Copyright (c) 2004-2026 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;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, ORDINAL1;
expansions TARSKI, XBOOLE_0;
theorems CARD_2, SPPOL_1, EULER_1, XBOOLE_1, ZFMISC_1, FUNCT_1, PARTFUN1,
FINSET_1, PENCIL_1, CARD_1, TARSKI, NAT_1, XBOOLE_0, FINSEQ_1, FUNCT_7,
FINSEQ_3, FINSEQ_5, TAXONOM1, RELAT_1, FUNCT_2, ENUMSET1, FINSEQ_2,
XREAL_1, XXREAL_0, ORDINAL1;
schemes NAT_1, FUNCT_2, XBOOLE_0;
begin :: Preliminaries
theorem Th1:
for X,Y being finite set holds card (X \/ Y) + card (X /\ Y) =
card X + card Y
proof
let X,Y be finite set;
card (X \/ Y) = card X + card Y - card (X /\ Y) by CARD_2:45;
hence thesis;
end;
scheme
Regr11 { n() -> Element of NAT, P[set] }: for k be Element of NAT st 1 <= k
& k <= n() holds P[k]
provided
A1: P[n()] & n() >= 2 and
A2: for k be Element of NAT st 1 <= k & k < n() & P[k+1] holds P[k]
proof
defpred X[Nat] means 1 <= $1 & $1 <= n() & not P[$1];
assume ex k be Element of NAT st X[k];
then
A3: ex k be Nat st X[k];
A4: for l be Nat st X[l] holds l <= n();
consider l be Nat such that
A5: X[l] and
A6: for n be Nat st X[n] holds n <= l from NAT_1:sch 6(A4,A3);
A7: l + 1 >= 1 by NAT_1:12;
A8: l < n() by A1,A5,XXREAL_0:1;
then
A9: l + 1 <= n() by NAT_1:13;
A10: now
assume not P[l+1];
then l + 1 <= l by A6,A9,A7;
hence contradiction by XREAL_1:29;
end;
l in NAT by ORDINAL1:def 12;
hence contradiction by A2,A5,A8,A10;
end;
scheme
Regr2 { P[set] } : P[1]
provided
A1: ex n be Element of NAT st n > 1 & P[n] and
A2: for k be Element of NAT st k >= 1 & P[k+1] holds P[k]
proof
consider n be Element of NAT such that
A3: n > 1 and
A4: P[n] by A1;
n >= 1+1 by A3,NAT_1:13;
then
A5: P[n] & n >= 2 by A4;
A6: for k be Element of NAT st 1 <= k & k < n & P[k+1] holds P[k] by A2;
for k be Element of NAT st 1 <= k & k <= n holds P[k] from Regr11(A5, A6);
hence thesis by A3;
end;
registration
let F be non empty set;
cluster non empty non-empty for FinSequence of bool F;
existence
proof
set x = the non empty Subset of F;
take v = <*x*>;
thus v is non empty;
rng v = {x} by FINSEQ_1:39;
then not {} in rng v by TARSKI:def 1;
hence thesis by RELAT_1:def 9;
end;
end;
theorem Th2:
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 <> {}
proof
let F be non empty set, f be non-empty FinSequence of bool F,
i be Element of NAT;
assume
A1: i in dom f;
assume f.i = {};
then {} in rng f by A1,FUNCT_1:3;
hence thesis by RELAT_1:def 9;
end;
registration
let F be finite set, A be FinSequence of bool F;
let i be Element of NAT;
cluster A.i -> finite;
coherence
proof
per cases;
suppose
i in dom A;
then A.i in bool F by PARTFUN1:4;
hence thesis;
end;
suppose
not i in dom A;
hence thesis by FUNCT_1:def 2;
end;
end;
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
:Def1:
:: 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;
existence
proof
defpred P[object] means ex j being set st j in J & j in dom A & $1 in A.j;
consider X being set such that
A1: for x being object holds x in X iff x in F & P[x] from XBOOLE_0:sch 1;
take X;
let x be object;
thus x in X implies ex j being set st j in J & j in dom A & x in A.j by A1;
given j being set such that
A2: j in J and
A3: j in dom A and
A4: x in A.j;
rng A c= bool F & A.j in rng A by A3,FINSEQ_1:def 4,FUNCT_1:3;
hence thesis by A1,A2,A3,A4;
end;
uniqueness
proof
defpred P[object] means
ex j being set st j in J & j in dom A & $1 in A.j;
let A1, A2 be set such that
A5: for x being object holds x in A1 iff ex j being set st j in J & j in
dom A & x in A.j and
A6: for x being object holds x in A2 iff ex j being set st j in J & j in
dom A & x in A.j;
A7: for x being object holds x in A2 iff P[x] by A6;
A8: for x being object holds x in A1 iff P[x] by A5;
A1 = A2 from XBOOLE_0:sch 2(A8,A7);
hence thesis;
end;
end;
theorem Th3:
for F being set, A being FinSequence of bool F, J being set holds
union (A, J) c= F
proof
let F be set, A be FinSequence of bool F, J be set;
let x be object;
assume x in union (A, J);
then consider j being set such that
j in J and
A1: j in dom A and
A2: x in A.j by Def1;
rng A c= bool F & A.j in rng A by A1,FINSEQ_1:def 4,FUNCT_1:3;
hence thesis by A2;
end;
theorem
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)
proof
let F be finite set, A be FinSequence of bool F, J, K be set;
assume
A1: J c= K;
thus union (A, J) c= union (A, K)
proof
let a be object;
assume a in union (A, J);
then ex j being set st j in J & j in dom A & a in A.j by Def1;
hence thesis by A1,Def1;
end;
end;
registration
let F be finite set;
let A be FinSequence of bool F;
let J be set;
cluster union (A, J) -> finite;
coherence by Th3,FINSET_1:1;
end;
theorem Th5:
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
proof
let F be finite set, A be FinSequence of bool F, i be Element of NAT such
that
A1: i in dom A;
thus union (A, {i}) c= A.i
proof
let x be object;
assume x in union (A, {i});
then ex j be set st j in {i} & j in dom A & x in A.j by Def1;
hence thesis by TARSKI:def 1;
end;
thus A.i c= union (A, {i})
proof
let x be object;
A2: i in {i} by TARSKI:def 1;
assume x in A.i;
hence thesis by A1,A2,Def1;
end;
end;
theorem Th6:
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
proof
let F be finite set, A be FinSequence of bool F, i,j be Element of NAT such
that
A1: i in dom A and
A2: j in dom A;
thus union (A, { i,j }) c= A.i \/ A.j
proof
let x be object;
assume x in union (A, { i,j });
then consider k be set such that
A3: k in {i,j} & k in dom A & x in A.k by Def1;
per cases by A3,TARSKI:def 2;
suppose
k = i & k in dom A & x in A.k;
hence thesis by XBOOLE_0:def 3;
end;
suppose
k = j & k in dom A & x in A.k;
hence thesis by XBOOLE_0:def 3;
end;
end;
thus A.i \/ A.j c= union (A, { i,j })
proof
let x be object;
assume
A4: x in A.i \/ A.j;
per cases by A4,XBOOLE_0:def 3;
suppose
A5: x in A.i;
i in {i,j} by TARSKI:def 2;
hence thesis by A1,A5,Def1;
end;
suppose
A6: x in A.j;
j in {i,j} by TARSKI:def 2;
hence thesis by A2,A6,Def1;
end;
end;
end;
theorem Th7:
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)
by Def1;
theorem Th8:
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
proof
let J be set;
let F be finite set;
let i be Element of NAT;
let A be FinSequence of bool F;
assume i in J & i in dom A;
then
A1: A.i c= union (A, J) by Th7;
thus union (A, J) c= union (A, J \{i}) \/ A.i
proof
let x be object;
assume x in union (A, J);
then consider j be set such that
A2: j in J and
A3: j in dom A and
A4: x in A.j by Def1;
per cases;
suppose
i = j;
hence thesis by A4,XBOOLE_0:def 3;
end;
suppose
i <> j;
then not j in {i} by TARSKI:def 1;
then j in J \ {i} by A2,XBOOLE_0:def 5;
then x in union (A, J\{i}) by A3,A4,Def1;
hence thesis by XBOOLE_0:def 3;
end;
end;
thus union (A, J\{i}) \/ A.i c= union (A, J)
proof
let x be object;
assume x in union (A, J\{i}) \/ A.i;
then
A5: x in union (A, J\{i}) or x in A.i by XBOOLE_0:def 3;
per cases by A1,A5;
suppose
x in union (A, J\{i});
then ex j be set st j in J\{i} & j in dom A & x in A.j by Def1;
hence thesis by Def1;
end;
suppose
x in union (A, J);
hence thesis;
end;
end;
end;
theorem Th9:
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)
proof
let J1, J2 be set;
let F be finite set;
let i be Element of NAT;
let A be FinSequence of bool F;
assume i in dom A;
then
A1: union (A, {i}) = A.i by Th5;
thus union (A,{i}\/J1\/J2) c= A.i \/ union (A,J1\/J2)
proof
let x be object;
assume x in union (A,{i}\/J1\/J2);
then consider j be set such that
A2: j in {i}\/J1\/J2 and
A3: j in dom A and
A4: x in A.j by Def1;
per cases;
suppose
i = j;
hence thesis by A4,XBOOLE_0:def 3;
end;
suppose
A5: i <> j;
j in {i}\/(J1\/J2) by A2,XBOOLE_1:4;
then j in {i} or j in J1\/J2 by XBOOLE_0:def 3;
then x in union (A, J1\/J2) by A3,A4,A5,Def1,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
end;
thus A.i \/ union (A,J1\/J2) c= union (A,{i}\/J1\/J2)
proof
let x be object;
assume
A6: x in A.i \/ union (A,J1\/J2);
per cases by A1,A6,XBOOLE_0:def 3;
suppose
x in union (A, {i});
then consider j be set such that
A7: j in {i} and
A8: j in dom A & x in A.j by Def1;
j in {i}\/(J1\/J2) by A7,XBOOLE_0:def 3;
then j in {i}\/J1\/J2 by XBOOLE_1:4;
hence thesis by A8,Def1;
end;
suppose
x in union (A,J1\/J2);
then consider j be set such that
A9: j in J1 \/ J2 and
A10: j in dom A & x in A.j by Def1;
j in {i} \/ (J1\/J2) by A9,XBOOLE_0:def 3;
then j in {i}\/J1\/J2 by XBOOLE_1:4;
hence thesis by A10,Def1;
end;
end;
end;
theorem Th10:
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
proof
let F be finite set;
let A be FinSequence of bool F;
let i be Element of NAT;
let x,y be set such that
A1: x <> y and
A2: x in A.i and
A3: y in A.i;
A.i c= (A.i\{x}) \/ (A.i\{y})
proof
{} = {y} \ ({y} \/ {}) by XBOOLE_1:46;
then A.i = A.i \ ({y} \ {y});
then A.i = (A.i \ {y}) \/ A.i /\ {y} by XBOOLE_1:52;
then
A4: A.i = A.i \ {y} \/ {y} by A3,ZFMISC_1:46;
let z be object;
not x in {y} by A1,TARSKI:def 1;
then
A5: x in A.i\{y} by A2,XBOOLE_0:def 5;
assume z in A.i;
then z in (A.i \ {x} \/ {x}) \/ (A.i \ {y} \/ {y}) by A4,XBOOLE_0:def 3;
then z in (A.i \ {x}) \/ ({x} \/ ({y} \/ (A.i \{y}))) by XBOOLE_1:4;
then z in (A.i \ {x}) \/ (({x} \/ {y}) \/ (A.i \{y})) by XBOOLE_1:4;
then z in ((A.i \ {x}) \/ ({y} \/ {x})) \/ (A.i \{y}) by XBOOLE_1:4;
then z in (((A.i \ {x}) \/ {y}) \/ {x}) \/ (A.i \{y}) by XBOOLE_1:4;
then
A6: z in ((A.i \ {x}) \/ {y}) \/ ({x} \/ (A.i \{y})) by XBOOLE_1:4;
not y in {x} by A1,TARSKI:def 1;
then y in A.i\{x} by A3,XBOOLE_0:def 5;
then z in (A.i \ {x}) \/ ({x} \/ (A.i \{y})) by A6,ZFMISC_1:40;
hence thesis by A5,ZFMISC_1:40;
end;
hence thesis;
end;
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
:Def2:
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);
existence
proof
A.i c= F
proof
per cases;
suppose
i in dom A;
then A.i in bool F by FINSEQ_2:11;
hence thesis;
end;
suppose
not i in dom A;
then A.i = {} by FUNCT_1:def 2;
hence thesis;
end;
end;
then reconsider EX = A.i \ {x} as Subset of F by XBOOLE_1:1;
set XX = A +* (i, EX);
reconsider XX as FinSequence of bool F;
take XX;
dom XX = dom A by FUNCT_7:30;
hence thesis by FUNCT_7:31,32;
end;
uniqueness
proof
let f1, f2 be FinSequence of bool F;
assume that
A1: dom f1 = dom A and
A2: for k being Element of NAT st k in dom f1 holds (i = k implies f1.
k = A.k \ {x}) & (i <> k implies f1.k = A.k) and
A3: dom f2 = dom A and
A4: for k being Element of NAT st k in dom f2 holds
(i = k implies f2.k = A.k \ {x}) & (i <> k implies f2.k = A.k);
for z being Nat st z in dom f1 holds f1. z = f2. z
proof
let z be Nat;
assume
A5: z in dom f1;
per cases;
suppose
A6: z = i;
then f1. z = A.i \ {x} by A2,A5
.= f2. z by A1,A3,A4,A5,A6;
hence thesis;
end;
suppose
A7: z <> i;
then f1. z = A.z by A2,A5
.= f2. z by A1,A3,A4,A5,A7;
hence thesis;
end;
end;
hence thesis by A1,A3,FINSEQ_1:13;
end;
end;
theorem Th11:
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
proof
let F be finite set, A be FinSequence of bool F, i be Element of NAT,
x be set;
set f = Cut (A,i,x);
assume that
A1: i in dom A and
A2: x in A.i;
i in dom f by A1,Def2;
then
A3: f.i = A.i \ {x} by Def2;
{x} c= A.i by A2,ZFMISC_1:31;
then card (f.i) = card (A.i) - card {x} by A3,CARD_2:44
.= card (A.i) - 1 by CARD_2:42;
hence thesis;
end;
theorem Th12:
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})
proof
let F be finite set, A be FinSequence of bool F, i be Element of NAT, x, J
be set;
thus union (Cut (A, i, x), J\{i}) c= union (A, J\{i})
proof
let z be object;
assume z in union (Cut (A, i, x), J\{i});
then consider j be set such that
A1: j in J\{i} and
A2: j in dom Cut (A, i, x) and
A3: z in Cut (A, i, x).j by Def1;
not j in {i} by A1,XBOOLE_0:def 5;
then i <> j by TARSKI:def 1;
then
A4: z in A.j by A2,A3,Def2;
j in dom A by A2,Def2;
hence thesis by A1,A4,Def1;
end;
A5: dom Cut (A, i, x) = dom A by Def2;
thus union (A, J\{i}) c= union (Cut (A, i, x), J\{i})
proof
let z be object;
assume z in union (A, J\{i});
then consider j be set such that
A6: j in J \ {i} and
A7: j in dom A and
A8: z in A.j by Def1;
not j in {i} by A6,XBOOLE_0:def 5;
then i <> j by TARSKI:def 1;
then Cut (A, i, x).j = A.j by A5,A7,Def2;
hence thesis by A5,A6,A7,A8,Def1;
end;
end;
theorem Th13:
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)
proof
let F be finite set, A be FinSequence of bool F, i be Element of NAT, x, J
be set;
assume
A1: not i in J;
thus union (A, J) c= union (Cut(A, i, x), J)
proof
let z be object;
assume z in union (A, J);
then consider j being set such that
A2: j in J and
A3: j in dom A and
A4: z in A.j by Def1;
A5: j in dom (Cut(A,i,x)) by A3,Def2;
per cases;
suppose
i = j;
hence thesis by A1,A2;
end;
suppose
i <> j;
then (Cut(A,i,x)).j = A.j by A5,Def2;
hence thesis by A2,A4,A5,Def1;
end;
end;
let z be object;
assume z in union (Cut(A, i, x), J);
then consider j being set such that
A6: j in J and
A7: j in dom Cut(A, i, x) and
A8: z in (Cut(A, i, x)).j by Def1;
A9: j in dom A by A7,Def2;
per cases;
suppose
i = j;
hence thesis by A1,A6;
end;
suppose
i <> j;
then (Cut(A,i,x)).j = A.j by A7,Def2;
hence thesis by A6,A8,A9,Def1;
end;
end;
theorem Th14:
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})
proof
let F be finite set, A be FinSequence of bool F, i be Element of NAT,
x, J be set such that
A1: i in dom Cut (A, i, x) and
A2: i in J;
union (Cut (A, i, x), J) = union (Cut (A, i, x), J \ {i}) \/ (Cut (A, i,
x).i) by A1,A2,Th8
.= union (A, J \ {i}) \/ (Cut (A, i, x).i) by Th12
.= union (A, J \ {i}) \/ (A.i \ {x}) by A1,Def2;
hence thesis;
end;
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
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
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;
existence
proof
set c = the Element of F;
reconsider b = {c} as Element of bool F by ZFMISC_1:31;
reconsider f = <*b*> as FinSequence of bool F;
for J being finite set st J c= dom f holds card J <= card union (f, J)
proof
let J be finite set;
assume
A1: J c= dom f;
A2: dom f = {1} by FINSEQ_1:2,38; then
A3: J = {} or J = {1} by A1,ZFMISC_1:33;
per cases by A3;
suppose J = {}; then
card J = 0;
hence thesis by NAT_1:2;
end;
suppose
A4: J = {1};
1 in dom f & 1 in NAT by A2,TARSKI:def 1; then
union (f, {1}) = f.1 by Th5
.= b; then
card union (f, J) = 1 by A4,CARD_1:30;
hence thesis by A4,CARD_1:30;
end;
end; then
f is Hall;
hence thesis;
end;
end;
registration let F be finite set;
cluster Hall for FinSequence of bool F;
existence
proof
reconsider f = <*>bool F as FinSequence of bool F;
for J being finite set st J c= dom f holds card J <= card union (f, J)
proof
let J be finite set;
assume J c= dom f; then
card J = 0;
hence thesis by NAT_1:2;
end; then
A1: f is Hall;
take f;
thus thesis by A1;
end;
end;
theorem Th15:
for F being finite set, A being non empty FinSequence of bool F
st A is Hall holds A is non-empty
proof
let F be finite set, A be non empty FinSequence of bool F;
assume
A1: A is Hall;
assume A is non non-empty;
then {} in rng A by RELAT_1:def 9;
then consider i being object such that
A2: i in dom A & A.i = {} by FUNCT_1:def 3;
set J = {i};
A3: card J = 1 by CARD_2:42;
J c= dom A & card (union (A, J)) = 0 by A2,Th5,CARD_1:27,ZFMISC_1:31;
hence thesis by A1,A3;
end;
registration let F be finite set;
cluster Hall -> non-empty for non empty FinSequence of bool F;
coherence by Th15;
end;
theorem Th16:
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
proof
let F be finite set, A be FinSequence of bool F, i be Element of NAT;
assume that
A1: i in dom A and
A2: A is Hall;
set J = {i};
J c= dom A by A1,ZFMISC_1:31; then
A3: card J <= card (union (A,J)) by A2;
assume
A4: card (A.i) < 1;
union (A,J) = A.i by A1,Th5;
hence thesis by A4,A3,CARD_2:42;
end;
theorem Th17:
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
proof
let F be non empty finite set, A be non empty FinSequence of bool F;
assume
A1: for i be Element of NAT st i in dom A holds card (A.i) = 1;
reconsider dA = dom A as non empty set;
deffunc F(Element of dA) = A.$1;
assume
A2: A is Hall;
A3: for a being Element of dA holds F meets F(a)
proof
let a be Element of dA;
set z = the Element of A.a;
A.a <> {} by A2;
then
A4: z in A.a;
rng A c= bool F & A.a in rng A by FINSEQ_1:def 4,FUNCT_1:3;
hence thesis by A4,XBOOLE_0:3;
end;
ex f being Function of dA, F st for a being Element of dA holds f.a in F
(a) from FUNCT_2:sch 10(A3);
then consider f being Function of dA, F such that
A5: for a being Element of dA holds f.a in F(a);
A6: dom f = dom A by FUNCT_2:def 1;
A7: rng f c= F
proof
let x be object;
A8: rng A c= bool F by FINSEQ_1:def 4;
assume x in rng f;
then consider y being object such that
A9: y in dom f and
A10: x = f.y by FUNCT_1:def 3;
f.y in A.y & A.y in rng A by A5,A6,A9,FUNCT_1:3;
hence thesis by A10,A8;
end;
ex n being Nat st dom A = Seg n by FINSEQ_1:def 2;
then f is FinSequence by A6,FINSEQ_1:def 2;
then reconsider f as FinSequence of F by A7,FINSEQ_1:def 4;
A11: dom A = dom f by FUNCT_2:def 1;
A12: card { {} } = 1 by CARD_1:30;
for i, j being Element of NAT st i in dom f & j in dom f & i <> j holds
f.i <> f.j
proof
let i, j be Element of NAT;
assume that
A13: i in dom f and
A14: j in dom f and
A15: i <> j;
thus f.i <> f.j
proof
card (A.i) = card { {} } by A1,A12,A11,A13;
then consider y being object such that
A16: A.i = { y } by CARD_1:29;
A17: A.i = { f.i }
proof
thus A.i c= { f.i }
proof
let x be object;
assume
A18: x in A.i;
x = f.i
proof
f.i in A.i by A5,A6,A13;
then
A19: f.i = y by A16,TARSKI:def 1;
assume x <> f.i;
hence thesis by A16,A18,A19,TARSKI:def 1;
end;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in { f.i };
then x = f.i by TARSKI:def 1;
hence thesis by A5,A6,A13;
end;
A20: j in dom A by A14,FUNCT_2:def 1;
then card (A.j) = card { {} } by A1,A12;
then consider z being object such that
A21: A.j = { z } by CARD_1:29;
A22: A.j = { f.j }
proof
thus A.j c= { f.j }
proof
let x be object;
assume
A23: x in A.j;
x = f.j
proof
f.j in A.j by A5,A6,A14;
then
A24: f.j = z by A21,TARSKI:def 1;
assume x <> f.j;
hence thesis by A21,A23,A24,TARSKI:def 1;
end;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in { f.j };
then x = f.j by TARSKI:def 1;
hence thesis by A5,A6,A14;
end;
set J = { i, j };
assume f.i = f.j;
then
A25: {f.i, f.j} = {f.i} by ENUMSET1:29;
A26: card J = 2 by A15,CARD_2:57;
A27: i in dom A by A13,FUNCT_2:def 1;
then
A28: J c= dom A by A20,ZFMISC_1:32;
card (union (A, J)) = card (A.i \/ A.j) by A27,A20,Th6
.= card ({f.i, f.j}) by A17,A22,ENUMSET1:1
.= 1 by A25,CARD_1:30;
hence contradiction by A2,A26,A28;
end;
end;
then for i, j being object st i in dom f & j in dom f & f.i = f.j
holds i = j;
then
A29: f is one-to-one by FUNCT_1:def 4;
for i being Element of NAT st i in dom f holds f.i in A.i by A5,A6;
then f is_a_system_of_different_representatives_of A by A11,A29;
hence thesis;
end;
theorem Th18: :: 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
proof
let F be finite set, A be FinSequence of bool F;
given X being set such that
A1: X is_a_system_of_different_representatives_of A;
consider f being FinSequence of F such that
f = X and
A2: dom A = dom f and
A3: for i being Element of NAT st i in dom f holds f.i in A.i and
A4: f is one-to-one by A1;
for J being finite set st J c= dom A holds card J <= card (union (A, J))
proof
let J be finite set;
set X = J;
set Y = union (A, J);
set g = f | X;
assume
A5: J c= dom A;
then
A6: dom g = X by A2,RELAT_1:62;
A7: dom g c= dom f by RELAT_1:60;
A8: rng g c= Y
proof
let x be object;
assume x in rng g;
then consider a being object such that
A9: a in dom g and
A10: x = g.a by FUNCT_1:def 3;
a in dom f by A7,A9;
then reconsider a as Element of NAT;
f.a in A.a by A2,A3,A5,A6,A9;
then g.a in A.a by A9,FUNCT_1:47;
hence thesis by A5,A6,A9,A10,Def1;
end;
g is one-to-one by A4,FUNCT_1:52;
then Segm card X c= Segm card Y by A6,A8,CARD_1:10;
hence thesis by NAT_1:39;
end;
hence thesis;
end;
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
:Def5:
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;
existence
proof
take A;
thus thesis;
end;
end;
definition
let F be set, A be FinSequence of bool F;
mode Reduction of A -> FinSequence of bool F means
:Def6:
dom it = dom A &
for i being Element of NAT st i in dom A holds it.i c= A.i;
existence
proof
for i being Element of NAT st i in dom A holds A.i c= A.i;
hence thesis;
end;
end;
definition
let F be set, A be FinSequence of bool F, i be Nat;
assume that
A1: i in dom A and
A2: A.i <> {};
mode Singlification of A, i -> Reduction of A means :Def7:
card (it.i) = 1;
existence
proof
set x = the Element of A.i;
A.i in bool F & x in A.i by A1,A2,PARTFUN1:4;
then reconsider E = {x} as Subset of F by ZFMISC_1:31;
reconsider G = A +* (i,E) as FinSequence of bool F;
A3: for j being Element of NAT st j in dom A holds G.j c= A.j
proof
let j be Element of NAT;
assume j in dom A;
per cases;
suppose
A4: j = i;
G.i = {x} by A1,FUNCT_7:31;
hence thesis by A2,A4,ZFMISC_1:31;
end;
suppose
j <> i;
hence thesis by FUNCT_7:32;
end;
end;
G.i = {x} by A1,FUNCT_7:31;
then
A5: card (G.i) = 1 by CARD_2:42;
dom G = dom A by FUNCT_7:30;
then G is Reduction of A by A3,Def6;
hence thesis by A5;
end;
end;
theorem Th19:
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
proof
let F be finite set, A be FinSequence of bool F, i be Element of NAT, C be
Reduction of A, i;
A1: dom C = dom A by Def5;
for j being Element of NAT st j in dom C holds C.j c= A.j
proof
let j be Element of NAT;
assume
A2: j in dom C;
per cases;
suppose
j = i;
hence thesis by Def5;
end;
suppose
j <> i;
hence thesis by A1,A2,Def5;
end;
end;
hence thesis by A1,Def6;
end;
theorem Th20:
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
proof
let F be finite set, A be FinSequence of bool F,
i be Element of NAT, x be set;
set f = Cut (A,i,x);
A1: dom f = dom A by Def2;
then
A2: for j being Element of NAT st j in dom A & j <> i holds A.j = f.j by Def2;
assume i in dom A;
then f.i = A.i \ {x} by A1,Def2;
hence thesis by A1,A2,Def5;
end;
theorem Th21:
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
proof
let F be finite set, A be FinSequence of bool F,
i be Element of NAT, x be set;
assume i in dom A;
then Cut (A,i,x) is Reduction of A,i by Th20;
hence thesis by Th19;
end;
theorem Th22:
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
proof
let F be finite set, A be FinSequence of bool F, B be Reduction of A;
let C be Reduction of B;
A1: for i being Element of NAT st i in dom A holds C.i c= A.i
proof
let i be Element of NAT;
assume
A2: i in dom A;
then i in dom B by Def6;
then
A3: C.i c= B.i by Def6;
B.i c= A.i by A2,Def6;
hence thesis by A3;
end;
dom B = dom C by Def6;
hence thesis by A1,Def6;
end;
theorem
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 <> {}
proof
let F be non empty finite set, A be non-empty FinSequence of bool F, i be
Element of NAT, B be Singlification of A, i;
assume
A1: i in dom A;
then A.i <> {} by Th2;
hence thesis by A1,Def7,CARD_1:27;
end;
theorem Th24:
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
proof
let F be non empty finite set, A be non-empty FinSequence of bool F,
i, j be Element of NAT, B be Singlification of A, i,
C be Singlification of B, j;
assume that
A1: i in dom A and
A2: j in dom A and
A3: C.i <> {} and
A4: B.j <> {};
A5: dom B = dom A by Def6;
then
A6: C.i c= B.i by A1,Def6;
A7: A.i <> {} by A1,Th2;
then card (B.i) = 1 by A1,Def7;
then
A8: card (C.i) = 1 by A3,A6,NAT_1:25,43;
A9: A.j <> {} by A2,Th2;
A10: C is Reduction of A by Th22;
card (C.j) = 1 by A2,A4,A5,Def7;
hence thesis by A1,A2,A7,A9,A10,A8,Def7;
end;
theorem
for F being set, A being FinSequence of bool F, i being Element of NAT
holds A is Reduction of A,i
proof
let F be set, A be FinSequence of bool F, i be Element of NAT;
( for j being Element of NAT st j in dom A & j <> i holds A.j = A.j)& A.
i c= A .i;
hence thesis by Def5;
end;
theorem Th26:
for F being set, A being FinSequence of bool F holds A is Reduction of A
proof
let F be set, A be FinSequence of bool F;
for i being Element of NAT st i in dom A holds A.i c= A.i;
hence thesis by Def6;
end;
definition
let F be non empty set, A be FinSequence of bool F;
assume
A1: A is non-empty;
mode Singlification of A -> Reduction of A means
:Def8:
for i being Element of NAT st i in dom A holds card (it.i) = 1;
existence
proof
deffunc F(object) = {the Element of A.$1};
A2: for x being object st x in dom A holds F(x) in bool F
proof
let x be object;
assume
A3: x in dom A;
then A.x <> {} by A1,Th2;
then
A4: {the Element of A.x} c= A.x by ZFMISC_1:31;
A.x in bool F by A3,PARTFUN1:4;
then {the Element of A.x} c= F by A4,XBOOLE_1:1;
hence thesis;
end;
ex f being Function of dom A, bool F st
for x being object st x in dom A
holds f.x = F(x) from FUNCT_2:sch 2(A2);
then consider f being Function of dom A, bool F such that
A5: for x being object st x in dom A holds f.x = F(x);
A6: for i being Element of NAT st i in dom f
holds f.i = {the Element of A.i}
proof
let i be Element of NAT;
assume i in dom f;
then i in dom A by FUNCT_2:def 1;
hence thesis by A5;
end;
A7: dom f = dom A by FUNCT_2:def 1;
A8: for i being Element of NAT st i in dom A holds f.i c= A.i
proof
let i be Element of NAT;
assume
A9: i in dom A;
then A.i <> {} by A1,Th2;
then {the Element of A.i} c= A.i by ZFMISC_1:31;
hence thesis by A7,A6,A9;
end;
dom f = dom A by FUNCT_2:def 1
.= Seg len A by FINSEQ_1:def 3;
then
A10: f is FinSequence by FINSEQ_1:def 2;
rng f c= bool F by RELAT_1:def 19;
then f is FinSequence of bool F by A10,FINSEQ_1:def 4;
then reconsider f as Reduction of A by A7,A8,Def6;
for i being Element of NAT st i in dom A holds card (f.i) = 1
proof
let i be Element of NAT;
assume i in dom A;
then i in dom f by FUNCT_2:def 1;
then f.i = {the Element of A.i} by A6;
hence thesis by CARD_2:42;
end;
hence thesis;
end;
end;
theorem Th27:
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)
proof
let F be non empty finite set, A be non empty non-empty FinSequence of bool
F, f be Function;
hereby
assume f is Singlification of A;
then reconsider f9 = f as Singlification of A;
f9 is Reduction of A;
hence dom f = dom A by Def6;
let i be Element of NAT;
assume
A1: i in dom A;
then card (f9.i) = 1 & A.i <> {} by Def8;
hence f is Singlification of A, i by A1,Def7;
end;
assume that
A2: dom f = dom A and
A3: for i being Element of NAT st i in dom A holds f is Singlification of A, i;
reconsider f as FinSequence of bool F by A3,FINSEQ_5:6;
for i being Element of NAT st i in dom A holds f.i c= A.i
proof
let i be Element of NAT;
assume
A4: i in dom A;
then f is Singlification of A, i by A3;
hence thesis by A4,Def6;
end;
then reconsider f9 = f as Reduction of A by A2,Def6;
for i being Element of NAT st i in dom A holds card (f9.i) = 1
proof
let i be Element of NAT;
assume
A5: i in dom A;
then f is Singlification of A, i & A.i <> {} by A3;
hence thesis by A5,Def7;
end;
hence thesis by Def8;
end;
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;
coherence
proof
let G be Singlification of A, k;
dom G = dom A by Def6;
hence thesis;
end;
end;
registration
let F be non empty finite set, A be non empty FinSequence of bool F;
cluster -> non empty for Singlification of A;
coherence
proof
let G be Singlification of A;
dom G = dom A by Def6;
hence thesis;
end;
end;
begin :: Rado Proof of the Hall Marriage Theorem
theorem Th28:
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
proof
let F be non empty finite set, A be non empty FinSequence of bool F, X be
set, B be Reduction of A such that
A1: X is_a_system_of_different_representatives_of B;
X is_a_system_of_different_representatives_of A
proof
consider f being FinSequence of F such that
A2: f = X and
A3: dom B = dom f and
A4: for i being Element of NAT st i in dom f holds f.i in B.i and
A5: f is one-to-one by A1;
A6: for i being Element of NAT st i in dom f holds f.i in A.i
proof
let i be Element of NAT such that
A7: i in dom f;
A8: f.i in B.i by A4,A7;
dom B = dom A by Def6;
then B.i c= A.i by A3,A7,Def6;
hence thesis by A8;
end;
dom A = dom B by Def6;
hence thesis by A2,A3,A5,A6;
end;
hence thesis;
end;
theorem Th29: :: 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
proof
let F be finite set;
let A be FinSequence of bool F such that
A1: A is Hall;
let i be Element of NAT such that
A2: card (A.i) >= 2;
Segm 2 c= Segm card (A.i) by A2,NAT_1:39;
then reconsider Ai = A.i as non trivial finite set by PENCIL_1:4;
consider x, y be object such that
A3: x in Ai and
A4: y in Ai and
A5: x <> y by ZFMISC_1:def 10;
assume
A6: for z being set st z in A.i holds not Cut (A, i, z) is Hall;
reconsider x,y as set by TARSKI:1;
not Cut (A, i, x) is Hall by A3,A6;
then consider JJ1 being finite set such that
A7: JJ1 c= dom Cut (A, i, x) and
A8: card JJ1 > card (union (Cut (A, i, x), JJ1));
ex J1 being finite set st not i in J1 & J1 c= dom Cut (A, i, x) & card
J1 >= card (union (A,J1) \/ (A.i \ {x}))
proof
per cases;
suppose
A9: i in JJ1;
set J1 = JJ1 \ {i};
A10: card J1 = card JJ1 - card {i} by A9,EULER_1:4
.= card JJ1 - 1 by CARD_1:30;
A11: J1 c= dom Cut (A, i, x) & {i} misses J1 by A7,XBOOLE_1:79;
union (Cut (A, i, x), JJ1) = union (A, JJ1 \ {i}) \/ (A.i \ {x}) by A7,A9
,Th14;
then card J1 >= card (union (A, J1) \/ (A.i \ {x})) by A8,A10,SPPOL_1:1;
hence thesis by A11,ZFMISC_1:48;
end;
suppose
A12: not i in JJ1;
take J1 = JJ1;
A13: J1 c= dom A by A7,Def2;
card J1 > card (union (A, J1)) by A8,A12,Th13;
hence thesis by A1,A13;
end;
end;
then consider J1 being finite set such that
A14: not i in J1 and
A15: J1 c= dom Cut (A, i, x) and
A16: card J1 >= card (union (A,J1) \/ (A.i \ {x}));
not Cut (A, i, y) is Hall by A4,A6;
then consider JJ2 being finite set such that
A17: JJ2 c= dom Cut (A, i, y) and
A18: card JJ2 > card (union (Cut (A, i, y), JJ2));
ex J2 being finite set st not i in J2 & J2 c= dom Cut (A, i, y) & card
J2 >= card (union (A,J2) \/ (A.i \ {y}))
proof
per cases;
suppose
A19: i in JJ2;
set J2 = JJ2 \ {i};
A20: card J2 = card JJ2 - card {i} by A19,EULER_1:4
.= card JJ2 - 1 by CARD_1:30;
A21: J2 c= dom Cut (A, i, y) & {i} misses J2 by A17,XBOOLE_1:79;
union (Cut (A, i, y), JJ2) = union (A, JJ2 \ {i}) \/ (A.i \ {y}) by A17
,A19,Th14;
then card J2 >= card (union (A, J2) \/ (A.i \ {y})) by A18,A20,SPPOL_1:1;
hence thesis by A21,ZFMISC_1:48;
end;
suppose
A22: not i in JJ2;
set J2 = JJ2;
take J2;
A23: J2 c= dom A by A17,Def2;
card J2 > card (union (A, J2)) by A18,A22,Th13;
hence thesis by A1,A23;
end;
end;
then consider J2 being finite set such that
A24: not i in J2 and
A25: J2 c= dom Cut (A, i, y) and
A26: card J2 >= card (union (A,J2) \/ (A.i \ {y}));
reconsider L = {i} \/ (J1\/J2) as finite set;
A27: J2 c= dom A by A25,Def2;
union (A,J1\/J2) \/ Ai c= ( union (A,J1) \/ (Ai\{x}) ) \/ ( union (A,J2
) \/ (Ai\{y}) )
proof
let a be object;
assume
A28: a in union (A, J1 \/ J2) \/ Ai;
per cases by A28,XBOOLE_0:def 3;
suppose
a in union (A, J1 \/ J2);
then consider j be set such that
A29: j in J1 \/ J2 and
A30: j in dom A & a in A.j by Def1;
j in J1 or j in J2 by A29,XBOOLE_0:def 3;
then a in union (A, J1) or a in union (A, J2) by A30,Def1;
then a in union (A, J1) \/ union (A, J2) by XBOOLE_0:def 3;
then a in union (A, J1) \/ union (A, J2) \/ ((Ai\{x}) \/ (Ai\{y})) by
XBOOLE_0:def 3;
then a in union (A, J1) \/ union (A, J2) \/ (Ai\{x}) \/ (Ai\{y}) by
XBOOLE_1:4;
then a in union (A, J1) \/ (Ai\{x}) \/ union (A, J2) \/ (Ai\{y}) by
XBOOLE_1:4;
hence thesis by XBOOLE_1:4;
end;
suppose
a in Ai;
then a in (Ai\{x}) \/ (Ai\{y}) or a in union (A, J1) or a in union (A,
J2) by A3,A4,A5,Th10;
then a in ((Ai\{x}) \/ (Ai\{y})) \/ union (A, J1) or a in union (A, J2)
by XBOOLE_0:def 3;
then a in ((Ai\{x}) \/ (Ai\{y})) \/ union (A, J1) \/ union (A, J2) by
XBOOLE_0:def 3;
then a in union (A, J1) \/ union (A, J2) \/ ((Ai\{x}) \/ (Ai\{y})) by
XBOOLE_1:4;
then a in union (A, J1) \/ union (A, J2) \/ (Ai\{x}) \/ (Ai\{y}) by
XBOOLE_1:4;
then a in union (A, J1) \/ (Ai\{x}) \/ union (A, J2) \/ (Ai\{y}) by
XBOOLE_1:4;
hence thesis by XBOOLE_1:4;
end;
end;
then
A31: card ((union (A,J1) \/ (Ai\{x}) ) \/ ( union (A,J2) \/ (Ai\{y}) )) >=
card (union (A,J1\/J2) \/ Ai) by NAT_1:43;
union (A,J1/\J2) c= union (A,J1) /\ union (A,J2)
proof
let x be object;
assume x in union (A,J1/\J2);
then consider j be set such that
A32: j in J1/\J2 and
A33: j in dom A & x in A.j by Def1;
j in J2 by A32,XBOOLE_0:def 4;
then
A34: x in union (A, J2) by A33,Def1;
j in J1 by A32,XBOOLE_0:def 4;
then x in union (A, J1) by A33,Def1;
hence thesis by A34,XBOOLE_0:def 4;
end;
then card(union (A,J1) /\ union (A,J2)) >= card( union (A,J1/\J2)) by
NAT_1:43;
then
A35: card (union (A,J1\/J2) \/ Ai) + card (union (A,J1) /\ (union (A,J2)))
>= card (Ai \/ union (A,J1\/J2)) + card (union (A,J1/\J2)) by XREAL_1:7;
J1 c= dom A by A15,Def2;
then
A36: (J1 \/ J2) c= dom A by A27,XBOOLE_1:8;
A37: i in dom A by A2,CARD_1:27,FUNCT_1:def 2;
then {i} c= dom A by ZFMISC_1:31;
then L c= dom A by A36,XBOOLE_1:8;
then card (union (A,{i}\/(J1\/J2))) >= card ({i}\/(J1\/J2)) by A1;
then
A38: card (union (A,{i}\/J1\/J2)) >= card ({i}\/(J1\/J2)) by XBOOLE_1:4;
not i in J1 \/ J2 by A14,A24,XBOOLE_0:def 3;
then
A39: card ({i}\/(J1\/J2)) = card {i} + card (J1\/J2) by CARD_2:40,ZFMISC_1:50;
J1 /\ J2 c= J1 & J1 c= dom A by A15,Def2,XBOOLE_1:17;
then J1 /\ J2 c= dom A;
then
A40: card (union (A,J1/\J2)) >= card (J1/\J2) by A1;
set S2 = union (A,J2) \/ (A.i \ {y});
set S1 = union (A,J1) \/ (A.i \ {x});
card J1 + card J2 >= card S1 + card S2 by A16,A26,XREAL_1:7;
then
A41: card J1 + card J2 >= card ( (union (A,J1) \/ (Ai\{x})) \/ (union (A,J2)
\/ (Ai\{y})) ) + card ( (union (A,J1) \/ (Ai\{x})) /\ (union (A,J2) \/ (Ai\{y})
) ) by Th1;
union (A,J1) /\ union (A,J2) c= (union (A,J1) \/ (Ai\{x})) /\ (union (A
,J2) \/ (Ai\{y}))
proof
let a be object;
assume
A42: a in union (A,J1) /\ union (A,J2);
then a in union (A,J2) by XBOOLE_0:def 4;
then
A43: a in union (A, J2) \/ (Ai\{y}) by XBOOLE_0:def 3;
a in union (A,J1) by A42,XBOOLE_0:def 4;
then a in union (A, J1) \/ (Ai\{x}) by XBOOLE_0:def 3;
hence thesis by A43,XBOOLE_0:def 4;
end;
then card((union (A,J1) \/ (Ai\{x})) /\ (union (A,J2) \/ (Ai\{y}))) >= card
(union (A,J1) /\ union (A,J2)) by NAT_1:43;
then card ( (union (A,J1) \/ (Ai\{x})) \/ (union (A,J2) \/ (Ai\{y})) ) +
card ( (union (A,J1) \/ (Ai\{x})) /\ (union (A,J2) \/ (Ai\{y})) ) >= card (
union (A,J1\/J2) \/ Ai) + card (union (A,J1) /\ (union (A,J2))) by A31,
XREAL_1:7;
then
card J1 + card J2 >= card (union (A,J1\/J2) \/ Ai) + card (union (A,J1)
/\ (union (A,J2))) by A41,XXREAL_0:2;
then
A44: card J1 + card J2 >= card (Ai \/ union (A,J1\/J2)) + card (union (A,J1
/\J2)) by A35,XXREAL_0:2;
card (union (A,{i}\/J1\/J2)) = card (Ai \/ union (A,J1\/J2)) by A37,Th9;
then card (Ai \/ union (A,J1\/J2)) >= 1 + card (J1\/J2) by A38,A39,CARD_1:30;
then
A45: card (Ai \/ union (A,J1\/J2)) + card (union (A,J1/\J2)) >= 1 + card (J1
\/J2) + card (J1/\J2) by A40,XREAL_1:7;
card (J1\/J2) + card (J1/\J2) = card J1 + card J2 by Th1;
then 1 + card (J1\/J2) + card (J1/\J2) = 1 + (card J1 + card J2);
hence thesis by A44,A45,NAT_1:13;
end;
theorem Th30:
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
proof
let F be finite set, A be FinSequence of bool F, i be Element of NAT such
that
A1: i in dom A and
A2: A is Hall;
A3: A.i <> {} by A1,A2,Th16,CARD_1:27;
set n = card (A.i);
A4: n >= 1 by A1,A2,Th16;
defpred P[Element of NAT] means ex G being Reduction of A st G is Hall &
card (G.i) = $1;
A5: A is Reduction of A by Th26;
per cases by A4,XXREAL_0:1;
suppose
n = 1;
then A is Singlification of A, i by A1,A5,Def7,CARD_1:27;
hence thesis by A2;
end;
suppose
A6: n > 1;
A7: for k be Element of NAT st k >= 1 & P[k+1] holds P[k]
proof
let k be Element of NAT;
assume that
A8: k >= 1 and
A9: P[k+1];
consider G being Reduction of A such that
A10: G is Hall and
A11: card (G.i) = k+1 by A9;
1 + 1 <= k + 1 by A8,XREAL_1:6;
then consider x being set such that
A12: x in G.i and
A13: Cut (G, i, x) is Hall by A10,A11,Th29;
set H = Cut (G,i,x);
A14: dom G = dom A by Def6;
then H is Reduction of G by A1,Th21;
then
A15: H is Reduction of A by Th22;
card (H.i) = k + 1 - 1 by A1,A11,A14,A12,Th11
.= k;
hence thesis by A13,A15;
end;
A is Reduction of A by Th26;
then
A16: ex n be Element of NAT st n > 1 & P[n] by A2,A6;
P[1] from Regr2(A16,A7);
then consider G being Reduction of A such that
A17: G is Hall and
A18: card (G.i) = 1;
G is Singlification of A, i by A1,A3,A18,Def7;
hence thesis by A17;
end;
end;
theorem Th31:
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
proof
let F be non empty finite set, A be non empty FinSequence of bool F;
defpred P[Nat] means $1 in dom A implies ex g being
Singlification of A, $1 st g is Hall & for k being Element of NAT st 1 <= k & k
<= $1 holds g is Singlification of A, k;
assume
A1: A is Hall;
then
A2: A is non-empty;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A4: P[k];
k+1 in dom A implies ex g being Singlification of A, k + 1 st g is
Hall & for l being Element of NAT st 1 <= l & l <= k + 1 holds g is
Singlification of A, l
proof
assume
A5: k+1 in dom A;
per cases by A5,TAXONOM1:1;
suppose
A6: k = 0;
consider g being Singlification of A, k + 1 such that
A7: g is Hall by A1,A5,Th30;
for l being Element of NAT st 1 <= l & l <= k + 1 holds g is
Singlification of A, l by A6,XXREAL_0:1;
hence thesis by A7;
end;
suppose
A8: k in dom A;
then consider g being Singlification of A, k such that
A9: g is Hall and
A10: for l being Element of NAT st 1 <= l & l <= k holds g is
Singlification of A, l by A4;
k+1 in dom g by A5,Def6;
then consider G being Singlification of g, k + 1 such that
A11: G is Hall by A9,Th30;
A12: dom g = dom A by Def6;
then
A13: dom G = dom A by Def6;
then
A14: G.k <> {} by A8,A11;
k in NAT by ORDINAL1:def 12;
then
A15: g.(k+1) <> {} by A9,A5,A12;
then reconsider G as Singlification of A, k + 1 by A2,A5,A8,A14,Th24;
for l being Element of NAT st 1 <= l & l <= k + 1 holds G is
Singlification of A, l
proof
let l be Element of NAT;
assume that
A16: 1 <= l and
A17: l <= k + 1;
k + 1 <= len A by A5,FINSEQ_3:25;
then l <= len A by A17,XXREAL_0:2;
then
A18: l in dom A by A16,FINSEQ_3:25;
then
A19: G.l <> {} by A13,A11;
per cases by A17,NAT_1:8;
suppose
l <= k;
then g is Singlification of A, l by A10,A16;
hence thesis by A2,A5,A15,A18,A19,Th24;
end;
suppose
l = k + 1;
hence thesis;
end;
end;
hence thesis by A11;
end;
end;
hence thesis;
end;
A20: P[0]
proof
assume 0 in dom A;
then consider G being Singlification of A, 0 such that
A21: G is Hall by A1,Th30;
for k being Element of NAT st 1 <= k & k <= 0 holds G is
Singlification of A, k;
hence thesis by A21;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A20,A3);
then len A in dom A implies ex g being Singlification of A, len A st g is
Hall & for l being Element of NAT st 1 <= l & l <= len A holds g is
Singlification of A, l;
then consider G being Singlification of A, len A such that
A22: G is Hall and
A23: for l being Element of NAT st 1 <= l & l <= len A holds G is
Singlification of A, l by FINSEQ_5:6;
A24: for i being Element of NAT st i in dom A holds G is Singlification of A
, i
proof
let i be Element of NAT;
assume i in dom A;
then 1 <= i & i <= len A by FINSEQ_3:25;
hence thesis by A23;
end;
dom G = dom A by Def6;
then G is Singlification of A by A2,A24,Th27;
hence thesis by A22;
end;
::$N Hall Marriage Theorem
::$L https://en.wikipedia.org/wiki/Hall's_marriage_theorem Hall Marriage Theorem
theorem
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
proof
let F be non empty finite set, A be non empty FinSequence of bool F;
thus (ex X being set st X is_a_system_of_different_representatives_of A)
implies A is Hall by Th18;
assume
A1: A is Hall;
then consider G being Singlification of A such that
A2: G is Hall by Th31;
for i being Element of NAT st i in dom G holds card (G.i) = 1
proof
let i be Element of NAT;
assume
A3: i in dom G;
dom G = dom A by Def6;
hence thesis by A1,A3,Def8;
end; then
ex X being set st X is_a_system_of_different_representatives_of G
by A2,Th17;
hence thesis by Th28;
end;