:: Introduction to Matroids
:: by Grzegorz Bancerek and Yasunari Shidama
::
:: Received July 30, 2008
:: Copyright (c) 2008 Association of Mizar Users
environ
vocabularies CLASSES1, PRE_TOPC, FINSET_1, BVFUNC_2, CARD_1, AMI_1, BOOLE,
VECTSP_1, RLVECT_3, FUNCT_1, RELAT_1, SETFAM_1, ORDERS_1, MATROID0,
TARSKI, SUBSET_1, JORDAN13, NATTRA_1, TAXONOM2, EQREL_1, MATRLIN, ARYTM,
ARYTM_1, RLVECT_1, RLVECT_2, AOFA_000, QC_LANG1, LEXBFS;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, SETFAM_1, FINSET_1,
NUMBERS, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_1,
EQREL_1, ORDERS_1, TAXONOM2, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, CARD_1,
CLASSES1, SEQ_1, MEMBERED, VALUED_1, LEXBFS, AOFA_000, STRUCT_0,
ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1, VECTSP_4, VECTSP_6, VECTSP_7,
PRE_TOPC, TDLAT_3, MATRLIN, PENCIL_1, RANKNULL;
constructors XXREAL_0, ARYTM_2, ARYTM_3, XBOOLE_0, NUMBERS, XREAL_0, NAT_1,
PCOMPS_1, EQREL_1, DOMAIN_1, FINSET_1, XCMPLX_0, CARD_1, CLASSES1,
COH_SP, TDLAT_3, FINSEQ_1, TAXONOM2, SEQ_1, MEMBERED, LEXBFS, VALUED_0,
VALUED_1, RANKNULL, VECTSP_1, VECTSP_7, GROUP_1, PRE_TOPC, MATRLIN,
PENCIL_1, SETFAM_1, TARSKI, ZFMISC_1, RELAT_1, REALSET1, STRUCT_0,
RLVECT_1, VECTSP_6, VECTSP_4;
registrations FINSET_1, ZFMISC_1, XBOOLE_0, NUMBERS, CARD_1, RELSET_1,
STRUCT_0, PSCOMP_1, SUBSET_1, ARYTM_2, XCMPLX_0, ARYTM_3, WAYBEL11,
PENCIL_1, TDLAT_3, FSM_1, MSAFREE1, PUA2MSS1, SETFAM_1, EQREL_1, MATRLIN,
XREAL_0, ORDINAL1, MEMBERED, VALUED_1, ALGSTR_0, ALGSTR_1, BINOM,
RLVECT_1, VECTSP_1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, FUNCT_1, CLASSES1, TAXONOM2, XBOOLE_0, STRUCT_0, LEXBFS,
GROUP_1, PRE_TOPC, PENCIL_1;
theorems TARSKI, XBOOLE_1, ZFMISC_1, CARD_1, COH_SP, PRE_TOPC, NAT_1,
CLASSES1, TDLAT_3, XXREAL_0, XREAL_1, XBOOLE_0, TAXONOM2, ORDERS_1,
FUNCT_2, FUNCT_1, EQREL_1, WELLORD2, VECTSP_7, VECTSP_9, MATRLIN,
STRUCT_0, CARD_FIN, CARD_2, VECTSP_4, ORDINAL1, CARD_FIL, RANKNULL,
VECTSP_1, VECTSP_6, ALGSTR_0, SETWISEO, HALLMAR1, BORSUK_5;
schemes FUNCT_2, NAT_1;
begin :: Definition by Independent Sets
notation
let x,y be set;
antonym x c/= y for x c= y;
end;
definition
mode SubsetFamilyStr is TopStruct;
end;
notation
let M be SubsetFamilyStr;
let A be Subset of M;
synonym A is independent for A is open;
antonym A is dependent for A is open;
end;
definition
let M be SubsetFamilyStr;
func the_family_of M -> Subset-Family of M equals the topology of M;
coherence;
end;
definition
let M be SubsetFamilyStr;
let A be Subset of M;
redefine attr A is independent means: Def8: A in the_family_of M;
compatibility by PRE_TOPC:def 5;
end;
definition
let M be SubsetFamilyStr;
attr M is subset-closed means: Def2: the_family_of M is subset-closed;
attr M is with_exchange_property means
for A,B being finite Subset of M
st A in the_family_of M & B in the_family_of M & card B = (card A) + 1
ex e being Element of M st e in B \ A & A \/ {e} in the_family_of M;
end;
registration
cluster strict non empty non void finite subset-closed with_exchange_property
SubsetFamilyStr;
existence
proof
bool {0} c= bool {0}; then
reconsider S = bool {0} as Subset-Family of {0};
take M = TopStruct(#{0}, S#);
thus M is strict;
thus the carrier of M is non empty;
thus the topology of M is non empty;
thus the carrier of M is finite;
thus the_family_of M is subset-closed by COH_SP:2;
let A,B be finite Subset of M;
assume A in the_family_of M;
assume B in the_family_of M;
assume
02: card B = (card A) + 1;
bool {0} = {{},{0}} by ZFMISC_1:30; then
04: (A = {} or A = {0}) & (B = {} or B = {0}) by TARSKI:def 2; then
05: (card A = 0 or card A = 1) & (card B = 0 or card B = 1) by CARD_1:50;
reconsider e = 0 as Element of M by TARSKI:def 1;
take e;
thus thesis by 02,04,05;
end;
end;
registration
let M be non void SubsetFamilyStr;
cluster independent Subset of M;
existence
proof
consider a being Element of the topology of M;
reconsider a as Subset of M;
take a; thus a in the_family_of M;
end;
end;
registration
let M be subset-closed SubsetFamilyStr;
cluster the_family_of M -> subset-closed;
coherence by Def2;
end;
theorem Th2:
for M being non void subset-closed SubsetFamilyStr
for A being independent Subset of M
for B being set st B c= A
holds B is independent Subset of M
proof
let M be non void subset-closed SubsetFamilyStr;
let A be independent Subset of M;
let B be set;
assume 01: B c= A;
A in the_family_of M by Def8; then
B in the_family_of M by 01,CLASSES1:def 1;
hence B is independent Subset of M by Def8;
end;
registration
let M be non void subset-closed SubsetFamilyStr;
cluster finite independent Subset of M;
existence
proof
consider a being Element of the topology of M;
reconsider a as independent Subset of M by PRE_TOPC:def 5;
{} c= a by XBOOLE_1:2; then
reconsider b = {} as independent Subset of M by Th2;
take b; thus thesis;
end;
end;
definition
mode Matroid is non empty non void subset-closed with_exchange_property
SubsetFamilyStr;
end;
theorem M0:
for M being subset-closed SubsetFamilyStr
holds M is non void iff {} in the_family_of M
proof
let M be subset-closed SubsetFamilyStr;
hereby
assume M is non void; then
reconsider M' = M as non void subset-closed SubsetFamilyStr;
consider a being independent Subset of M';
{} c= a by XBOOLE_1:2; then
{} is independent Subset of M' by Th2;
hence {} in the_family_of M by Def8;
end;
assume {} in the_family_of M;
hence the topology of M is non empty;
end;
registration
let M be non void subset-closed SubsetFamilyStr;
cluster {} the carrier of M -> independent;
coherence
proof
thus {} the carrier of M in the_family_of M by M0;
end;
end;
theorem M1:
for M being non void SubsetFamilyStr
holds M is subset-closed iff
for A,B being Subset of M st A is independent & B c= A holds B is independent
proof
let M be non void SubsetFamilyStr;
thus M is subset-closed implies for A,B being Subset of M
st A is independent & B c= A holds B is independent by Th2;
assume
03: for A,B being Subset of M st A is independent & B c= A
holds B is independent;
let x,y be set; assume x in the_family_of M; then
04: x is independent Subset of M by Def8;
assume y c= x; then
y is independent Subset of M by 03,04,XBOOLE_1:1;
hence thesis by Def8;
end;
registration
let M be non void subset-closed SubsetFamilyStr;
let A be independent Subset of M;
let B be set;
cluster A/\B -> independent Subset of M;
coherence
proof
A/\B c= A by XBOOLE_1:17;
hence thesis by M1;
end;
cluster B/\A -> independent Subset of M;
coherence;
cluster A\B -> independent Subset of M;
coherence
proof
A\B c= A by XBOOLE_1:36;
hence thesis by M1;
end;
end;
theorem M2:
for M being non void non empty SubsetFamilyStr
holds M is with_exchange_property iff
for A,B being finite Subset of M
st A is independent & B is independent & card B = (card A) + 1
ex e being Element of M st e in B \ A & A \/ {e} is independent
proof
let M be non void non empty SubsetFamilyStr;
consider e0 being Element of M;
thus M is with_exchange_property implies
for A,B being finite Subset of M
st A is independent & B is independent & card B = (card A) + 1
ex e being Element of M st e in B \ A & A \/ {e} is independent
proof assume
00: for A,B being finite Subset of M
st A in the_family_of M & B in the_family_of M & card B = (card A) + 1
ex e being Element of M st e in B \ A & A \/ {e} in the_family_of M;
let A,B be finite Subset of M;
assume
A in the_family_of M & B in the_family_of M & card B = (card A) + 1; then
consider e being Element of M such that
01: e in B \ A & A \/ {e} in the_family_of M by 00;
take e; thus e in B \ A & A \/ {e} in the_family_of M by 01;
end;
assume
02: for A,B being finite Subset of M
st A is independent & B is independent & card B = (card A) + 1
ex e being Element of M st e in B \ A & A \/ {e} is independent;
let A,B be finite Subset of M;
assume A in the_family_of M & B in the_family_of M; then
03: A is independent & B is independent by Def8;
assume card B = (card A) + 1; then
consider e being Element of M such that
04: e in B \ A & A \/ {e} is independent by 02,03;
take e; thus thesis by 04,Def8;
end;
notation
let A be set;
synonym A is finite-membered for A is with_finite-elements;
end;
definition
let A be set;
redefine attr A is finite-membered means:
Def6:
for B being set st B in A holds B is finite;
compatibility
proof
thus A is finite-membered implies
for B being set st B in A holds B is finite
proof
assume for a being Element of A holds a is finite;
hence thesis;
end;
assume
A1: for B being set st B in A holds B is finite;
let a be Element of A;
A <> {} or A = {};
hence thesis by A1;
end;
end;
definition
let M be SubsetFamilyStr;
attr M is finite-membered means:
Def7:
the_family_of M is finite-membered;
end;
definition
let M be SubsetFamilyStr;
attr M is finite-degree means:
Def9:
M is finite-membered &
ex n being Nat st
for A being finite Subset of M st A is independent holds card A <= n;
end;
registration
cluster finite-degree -> finite-membered SubsetFamilyStr;
coherence
proof let M be SubsetFamilyStr;
assume M is finite-membered;
hence thesis;
end;
cluster finite -> finite-degree SubsetFamilyStr;
coherence
proof let M be SubsetFamilyStr;
assume the carrier of M is finite; then
reconsider X = the carrier of M as finite set;
thus M is finite-membered
proof
let x be set; assume x in the_family_of M; then
x c= X;
hence thesis;
end;
take n = card X;
let A be finite Subset of M;
thus thesis by NAT_1:44;
end;
end;
begin :: Examples
registration
cluster mutually-disjoint non empty with_non-empty_elements set;
existence
proof
take Y = {{0}};
thus thesis by TAXONOM2:10;
end;
end;
theorem Th11:
for A,B being finite set st card A < card B
ex x being set st x in B \ A
proof
let A,B be finite set;
assume card A < card B; then
not B c= A by NAT_1:44; then
consider x being set such that
00: x in B & x nin A by TARSKI:def 3;
take x;
thus x in B \ A by 00,XBOOLE_0:def 4;
end;
theorem
for P being mutually-disjoint with_non-empty_elements non empty set
for f being Choice_Function of P holds f is one-to-one
proof
let P be mutually-disjoint with_non-empty_elements non empty set;
let f be Choice_Function of P;
let x1,x2 be set; assume
00: x1 in dom f & x2 in dom f & f.x1 = f.x2;
not {} in P; then
f.x1 in x1 & f.x1 in x2 by 00,ORDERS_1:def 1; then
x1 meets x2 by XBOOLE_0:3;
hence x1 = x2 by 00,TAXONOM2:def 5;
end;
registration
cluster -> non void subset-closed with_exchange_property
(discrete SubsetFamilyStr);
coherence
proof
let T be discrete SubsetFamilyStr;
thus
01: T is non void
proof
thus the topology of T is non empty by TDLAT_3:def 1;
end;
for A,B being Subset of T st A is independent & B c= A
holds B is independent by TDLAT_3:17;
hence T is subset-closed by 01,M1;
let A,B be finite Subset of T such that
A in the_family_of T & B in the_family_of T and
02: card B = card A + 1;
now assume B c= A; then
card B c= card A by CARD_1:27; then
card B <= card A & 0 < 1 by NAT_1:40; then
card B + 0 < card A + 1 by XREAL_1:10;
hence contradiction by 02;
end; then
consider x being set such that
03: x in B & not x in A by TARSKI:def 3;
reconsider x as Element of T by 03;
take x; thus x in B \ A by 03,XBOOLE_0:def 4;
{x} c= the carrier of T by 03,ZFMISC_1:37; then
reconsider C = A \/ {x} as Subset of T by XBOOLE_1:8;
C is independent by TDLAT_3:17;
hence thesis by Def8;
end;
end;
theorem
for T being non empty discrete TopStruct holds T is Matroid;
definition
let P be set;
func ProdMatroid P -> strict SubsetFamilyStr means:
Def4:
the carrier of it = union P &
the_family_of it = {A where A is Subset of union P:
for D being set st D in P ex d being set st A /\ D c= {d}};
existence
proof
set X = union P;
set F = {A where A is Subset of union P:
for D being set st D in P ex d being set st A /\ D c= {d}};
F c= bool X
proof
let x be set; assume x in F; then
ex A being Subset of X st x = A &
for D being set st D in P ex d being set st A /\ D c= {d};
hence thesis;
end; then
reconsider F as Subset-Family of X;
take M = TopStruct(#X,F#);
thus thesis;
end;
uniqueness;
end;
registration
let P be non empty with_non-empty_elements set;
cluster ProdMatroid P -> non empty;
coherence
proof set M = ProdMatroid P;
the carrier of M = union P by Def4;
hence the carrier of M is non empty;
end;
end;
theorem Th10:
for P being set
for A being Subset of ProdMatroid P holds A is independent iff
for D being Element of P ex d being Element of D st A /\ D c= {d}
proof
let P be set;
set M = ProdMatroid P;
00: the_family_of M = {A where A is Subset of union P:
for D being set st D in P ex d being set st A /\ D c= {d}} by Def4;
03: the carrier of M = union P by Def4;
let A be Subset of ProdMatroid P;
thus A is independent implies
for D being Element of P ex d being Element of D st A /\ D c= {d}
proof assume A in the_family_of M; then
01: ex B being Subset of union P st A = B & for D being set st D in P
ex d being set st B /\ D c= {d} by 00;
let D be Element of P;
P = {} implies A = {} & {} /\ D = {} by 03,ZFMISC_1:2; then
P = {} implies A /\ D c= {1} by XBOOLE_1:2; then
consider d being set such that
02: A /\ D c= {d} by 01;
consider d0 being Element of D;
now assume d nin D; then
d nin A /\ D by XBOOLE_0:def 3; then
A /\ D <> {d} by TARSKI:def 1; then
A /\ D = {} by 02,ZFMISC_1:39;
hence A /\ D c= {d0} by XBOOLE_1:2;
end;
hence thesis by 02;
end;
assume
03: for D being Element of P ex d being Element of D st A /\ D c= {d};
04: the carrier of M = union P by Def4;
now let D be set; assume D in P; then
ex d being Element of D st A /\ D c= {d} by 03;
hence ex d being set st A /\ D c= {d};
end;
hence A in the_family_of M by 00,04;
end;
registration
let P be set;
cluster ProdMatroid P -> non void subset-closed;
coherence
proof set M = ProdMatroid P;
00: the_family_of M = {A where A is Subset of union P:
for D being set st D in P ex d being set st A /\ D c= {d}} by Def4;
set A = {} union P;
now let D be set; assume D in P;
consider d being set;
take d; thus A /\ D c= {d} by XBOOLE_1:2;
end; then
A in the_family_of M by 00;
hence the topology of M is non empty;
thus the_family_of M is subset-closed
proof
let a,b be set;
assume
01: a in the_family_of M & b c= a; then
02: ex B being Subset of union P st a = B & for D being set st D in P
ex d being set st B /\ D c= {d} by 00; then
03: b is Subset of union P by 01,XBOOLE_1:1;
now let D be set; assume D in P; then
consider d being set such that
03: a /\ D c= {d} by 02;
take d;
b /\ D c= a /\ D by 01,XBOOLE_1:26;
hence b /\ D c= {d} by 03,XBOOLE_1:1;
end;
hence b in the_family_of M by 00,03;
end;
end;
end;
theorem Th14:
for P being mutually-disjoint set
for x being Subset of ProdMatroid P
ex f being Function of x,P st
for a being set st a in x holds a in f.a
proof
let P be mutually-disjoint set;
let x be Subset of ProdMatroid P;
defpred P[set,set] means $1 in $2;
00: now
let a be set;
assume a in x; then
a in the carrier of ProdMatroid P; then
a in union P by Def4;
then ex y being set st a in y & y in P by TARSKI:def 4;
hence ex y being set st y in P & P[a,y];
end;
consider f being Function of x,P such that
01: for a being set st a in x holds P[a,f.a] from FUNCT_2:sch 1(00);
take f; thus thesis by 01;
end;
theorem Th13:
for P being mutually-disjoint set
for x being Subset of ProdMatroid P
for f being Function of x,P st
for a being set st a in x holds a in f.a
holds x is independent iff f is one-to-one
proof
let P be mutually-disjoint set, x be Subset of ProdMatroid P;
let f be Function of x,P;
assume
01: for a being set st a in x holds a in f.a;
hereby
assume
03: x is independent;
thus f is one-to-one
proof
let a,b be set;
assume a in dom f & b in dom f; then
06: f.a in rng f & f.b in rng f & a in x & b in x by FUNCT_1:def 5; then
reconsider D1 = f.a, D2 = f.b as Element of P;
consider d1 being Element of D1 such that
04: x /\ D1 c= {d1} by 03,Th10;
consider d2 being Element of D2 such that
05: x /\ D2 c= {d2} by 03,Th10;
a in D1 & b in D2 by 01,06; then
07: a in x /\ D1 & b in x /\ D2 by 06,XBOOLE_0:def 3; then
a = d1 & b = d2 by 04,05,TARSKI:def 1;
hence thesis by 05,07,TARSKI:def 1;
end;
end;
assume
08: f is one-to-one;
now
let D be Element of P;
assume
09: for d being Element of D holds x /\ D c/= {d};
consider d1 being Element of D;
x /\ D c/= {d1} by 09; then
consider d2 being set such that
010: d2 in x /\ D & d2 nin {d1} by TARSKI:def 3;
011: d2 in x & d2 in D & d1 <> d2 by 010,XBOOLE_0:def 3,TARSKI:def 1;
the carrier of ProdMatroid P = union P by Def4; then
ex y being set st d2 in y & y in P by 011,TARSKI:def 4; then
012: dom f = x & D in P by FUNCT_2:def 1; then
d2 in f.d2 & f.d2 in rng f by 01,011,FUNCT_1:def 5; then
f.d2 meets D & f.d2 in P by 011,XBOOLE_0:3; then
013: f.d2 = D by TAXONOM2:def 5;
x /\ D c= {d2}
proof
let a be set;
assume a in x /\ D; then
014: a in x & a in D by XBOOLE_0:def 3; then
a in f.a & f.a in rng f by 01,012,FUNCT_1:def 5; then
f.a meets D & f.a in P by 014,XBOOLE_0:3; then
f.a = D by TAXONOM2:def 5; then
a = d2 by 011,012,013,014,08,FUNCT_1:def 8;
hence thesis by TARSKI:def 1;
end;
hence contradiction by 09,011;
end;
hence x is independent by Th10;
end;
registration
let P be mutually-disjoint set;
cluster ProdMatroid P -> with_exchange_property;
coherence
proof set M = ProdMatroid P;
00: the_family_of M = {A where A is Subset of union P:
for D being set st D in P ex d being set st A /\ D c= {d}} by Def4;
let A,B be finite Subset of M;
defpred P[set,set] means $1 in $2;
assume
0A: A in the_family_of M & B in the_family_of M;
07: A is independent & B is independent by 0A,Def8;
consider f being Function of A,P such that
06: for a being set st a in A holds a in f.a by Th14;
consider g being Function of B,P such that
03: for a being set st a in B holds a in g.a by Th14;
the carrier of ProdMatroid P = union P by Def4; then
(P = {} implies A = {}) & (P = {} implies B = {}) by ZFMISC_1:2; then
02: dom f = A & f is one-to-one & rng f c= P &
dom g = B & g is one-to-one & rng g c= P
by 06,07,03,Th13,FUNCT_2:def 1;
reconsider A' = rng f, B' = rng g as finite set;
A, A' are_equipotent & B, B' are_equipotent by 02,WELLORD2:def 4; then
0A: card A = card A' & card B = card B' by CARD_1:21;
assume card B = (card A) + 1; then
card B > card A by NAT_1:13; then
consider a being set such that
08: a in B' \ A' by 0A,Th11;
05: a in B' & a nin A' by 08,XBOOLE_0:def 4; then
consider x' being set such that
09: x' in B & a = g.x' by 02,FUNCT_1:def 5;
reconsider x = x' as Element of M by 09;
take x;
now assume x in A; then
0B: x in f.x & x in g.x & f.x in rng f & g.x in rng g
by 02,06,03,09,FUNCT_1:def 5; then
f.x meets g.x & f.x in P & g.x in P by XBOOLE_0:3;
hence contradiction by 0B,09,05,TAXONOM2:def 5;
end;
hence x in B \ A by 09,XBOOLE_0:def 4;
reconsider xx = {x} as Subset of M by 09,ZFMISC_1:37;
reconsider Ax = A \/ xx as Subset of union P by Def4;
now let D be set; assume
0C: D in P; then
consider d being Element of D such that
0D: A /\ D c= {d} by 07,Th10;
0E: Ax /\ D = A /\ D \/ xx /\ D by XBOOLE_1:23;
per cases;
suppose
0F: D = a;
take x';
A /\ D c= {}
proof let z be set;
assume z in A /\ D; then
0G: z in A & z in D by XBOOLE_0:def 3; then
0H: z in f.z & f.z in rng f by 06,02,FUNCT_1:def 5; then
f.z in P & D meets f.z by 0G,XBOOLE_0:3;
hence z in {} by 0F,0H,05,TAXONOM2:def 5;
end; then
A /\ D = {};
hence Ax /\ D c= {x'} by 0E,XBOOLE_1:17;
end;
suppose
0I: D <> a;
reconsider d as set;
take d;
a in rng g by 09,02,FUNCT_1:def 5; then
a misses D & x in a by 03,09,0I,0C,TAXONOM2:def 5; then
x nin D by XBOOLE_0:3; then
xx c/= D by ZFMISC_1:37; then
xx /\ D <> xx & xx /\ D c= xx by XBOOLE_1:17; then
xx /\ D = {} by ZFMISC_1:39;
hence Ax /\ D c= {d} by 0D,0E;
end;
end;
hence A \/ {x} in the_family_of M by 00;
end;
end;
registration
let X be finite set;
let P be Subset of bool X;
cluster ProdMatroid P -> finite;
coherence
proof
union P is finite;
hence the carrier of ProdMatroid P is finite by Def4;
end;
end;
registration
let X be set;
cluster -> mutually-disjoint a_partition of X;
coherence
proof
let P be a_partition of X;
let x,y be set;
thus thesis by EQREL_1:def 6;
end;
end;
registration
cluster finite strict Matroid;
existence
proof
consider X being finite non empty set, P being a_partition of X;
take M = ProdMatroid P;
thus thesis;
end;
end;
registration
let M be finite-membered non void SubsetFamilyStr;
cluster -> finite (independent Subset of M);
coherence
proof
let A be independent Subset of M;
A in the_family_of M & the_family_of M is finite-membered
by Def7,Def8;
hence A is finite by Def6;
end;
end;
definition
let F be Field;
let V be VectSp of F;
func LinearlyIndependentSubsets V -> strict SubsetFamilyStr means:
Def5:
the carrier of it = the carrier of V &
the_family_of it = {A where A is Subset of V: A is linearly-independent};
existence
proof
set X = the carrier of V;
set F = {A where A is Subset of V: A is linearly-independent};
F c= bool X
proof
let x be set; assume x in F; then
ex A being Subset of X st x = A & A is linearly-independent;
hence thesis;
end; then
reconsider F as Subset-Family of X;
take M = TopStruct(#X,F#);
thus thesis;
end;
uniqueness;
end;
registration
let F be Field;
let V be VectSp of F;
cluster LinearlyIndependentSubsets V ->
non empty non void subset-closed;
coherence
proof set M = LinearlyIndependentSubsets V;
the carrier of M = the carrier of V by Def5;
hence the carrier of M is non empty;
A2: the_family_of M = {A where A is Subset of V: A is linearly-independent}
by Def5;
{} the carrier of V is linearly-independent by VECTSP_7:4; then
{} in the_family_of M by A2;
hence the topology of M is non empty;
let x,y be set;
assume x in the_family_of M; then
consider A being Subset of V such that
A3: x = A & A is linearly-independent by A2;
assume
A4: y c= x; then
reconsider B = y as Subset of V by A3,XBOOLE_1:1;
B is linearly-independent by A3,A4,VECTSP_7:2;
hence y in the_family_of M by A2;
end;
end;
registration
let F be Field;
let V be VectSp of F;
cluster linearly-independent empty Subset of V;
existence
proof
take {} the carrier of V;
thus thesis by VECTSP_7:4;
end;
end;
theorem Th21:
for F being Field, V being VectSp of F
for A being Subset of LinearlyIndependentSubsets V
holds A is independent iff A is linearly-independent Subset of V
proof
let F be Field;
let V be VectSp of F;
set M = LinearlyIndependentSubsets V;
let B be Subset of M;
the_family_of M = {A where A is Subset of V: A is linearly-independent}
by Def5; then
B in the_family_of M iff
ex A being Subset of V st B = A & A is linearly-independent;
hence thesis by Def8;
end;
theorem
for F being Field
for V being VectSp of F
for A, B being finite Subset of V st B c= A
for v being Vector of V st v in Lin(A) & not v in Lin(B)
holds
ex w being Vector of V st w in A\B & w in Lin(A \ {w} \/ {v})
proof
let F be Field;
let V be VectSp of F;
let A, B be finite Subset of V;
assume B c= A; then
A = B\/(A\B) by XBOOLE_1:45;
hence thesis by VECTSP_9:22;
end;
theorem ThI1:
for F being Field, V being VectSp of F
for A being Subset of V st A is linearly-independent
for a being Element of V st a nin the carrier of Lin A
holds A\/{a} is linearly-independent
proof
let F be Field;
let V be VectSp of F;
let A be Subset of V such that
Z0: A is linearly-independent;
let a be Element of V;
set B = A\/{a};
assume
Z1: a nin the carrier of Lin A & B is linearly-dependent; then
consider l being Linear_Combination of B such that
A0: Sum l = 0.V & Carrier l <> {} by VECTSP_7:def 1;
A1: {Sum s where s is Linear_Combination of A: not contradiction} =
the carrier of Lin A by VECTSP_7:def 2;
a in {a} by TARSKI:def 1; then
A2: (l!{a}).a = l.a by RANKNULL:25;
A c= the carrier of Lin A
proof
let x be set; assume
B0: x in A; then
reconsider x as Element of V;
x in Lin A by B0,VECTSP_7:13;
hence thesis by STRUCT_0:def 5;
end; then
a nin A by Z1; then
B\A={a} & A c= B by XBOOLE_1:7,88,ZFMISC_1:56; then
l = (l!A)+(l!{a}) by RANKNULL:27; then
0.V = Sum (l!A) + Sum (l!{a}) by A0,VECTSP_6:77
.= Sum (l!A) + (l.a)*a by A2,VECTSP_6:43; then
A3: (l.a)*a = - Sum (l!A) by ALGSTR_0:def 13;
A4: (-(l.a)")*(l!A) is Linear_Combination of A by VECTSP_6:61;
now assume
l.a <> 0.F; then
a = ((l.a)")*(-Sum(l!A)) by A3,VECTSP_1:67
.= -((l.a)" * Sum(l!A)) by VECTSP_1:69
.= (-(l.a)")*(Sum(l!A)) by VECTSP_1:68
.= Sum((-(l.a)")*(l!A)) by VECTSP_6:78;
hence contradiction by A1,Z1,A4;
end; then
A5: a nin Carrier l & Carrier l c= B by VECTSP_6:20,def 7;
Carrier l c= A
proof
let x be set;
thus thesis by A5,SETWISEO:6;
end; then
l is Linear_Combination of A by VECTSP_6:def 7;
hence contradiction by A0,Z0,VECTSP_7:def 1;
end;
registration
let F be Field;
let V be VectSp of F;
cluster LinearlyIndependentSubsets V -> with_exchange_property;
coherence
proof set M = LinearlyIndependentSubsets V;
A2: the_family_of M = {A where A is Subset of V: A is linearly-independent}
by Def5;
let A,B be finite Subset of M such that
A5: A in the_family_of M & B in the_family_of M & card B = (card A) + 1;
A is independent & B is independent by A5,Def8; then
reconsider A' = A, B' = B as
linearly-independent finite Subset of V by Th21;
set V' = Lin (A' \/ B');
A' c= the carrier of V'
proof
let a be set; assume a in A'; then
a in A' \/ B' by XBOOLE_0:def 2; then
a in V' by VECTSP_7:13;
hence thesis by STRUCT_0:def 5;
end; then
reconsider A'' = A' as linearly-independent finite Subset of V'
by VECTSP_9:16;
B' c= the carrier of V'
proof
let a be set; assume a in B'; then
a in A' \/ B' by XBOOLE_0:def 2; then
a in V' by VECTSP_7:13;
hence thesis by STRUCT_0:def 5;
end; then
reconsider B'' = B' as linearly-independent finite Subset of V'
by VECTSP_9:16;
A0: V' = Lin(A''\/ B'') by VECTSP_9:21; then
consider D being Basis of V' such that
A4: B' c= D by VECTSP_7:27;
consider C being Basis of V' such that
A3: C c= A'' \/ B'' by A0,VECTSP_7:28;
consider e being Element of C \ the carrier of Lin A';
reconsider c = C as finite set by A3;
A8: c is Basis of V' & A' is Basis of Lin A' by RANKNULL:20; then
BB: V' is finite-dimensional & Lin A' is finite-dimensional
by MATRLIN:def 3; then
card c = Card D by VECTSP_9:26; then
card B c= card c by A4,CARD_1:27; then
card B <= card c by NAT_1:40; then
A9: card A < card c by A5,NAT_1:13;
now assume
C c= the carrier of Lin A'; then
reconsider C' = C as Subset of Lin A';
the carrier of Lin A' c= the carrier of V by VECTSP_4:def 2; then
reconsider C'' = C' as Subset of V by XBOOLE_1:1;
C is linearly-independent by VECTSP_7:def 3; then
C'' is linearly-independent by VECTSP_9:15; then
consider E being Basis of Lin A' such that
B2: C' c= E by VECTSP_7:27,VECTSP_9:16;
B3: card A = Card E by A8,BB,VECTSP_9:26; then
A,E are_equipotent by CARD_1:21; then
E is finite by CARD_1:68;
hence contradiction by A9,B2,B3,NAT_1:44;
end; then
consider x being set such that
AA: x in C & x nin the carrier of Lin A' by TARSKI:def 3;
x in C \ the carrier of Lin A' by AA,XBOOLE_0:def 4; then
A6: e in C & e nin the carrier of Lin A' by XBOOLE_0:def 4; then
A7: e in A\/B by A3; then
reconsider e as Element of M;
take e;
A c= the carrier of Lin A'
proof
let x be set; assume x in A; then
x in Lin A' by VECTSP_7:13;
hence thesis by STRUCT_0:def 5;
end; then
B7: e nin A by A6; then
B8: e in B' by A7,XBOOLE_0:def 2;
hence e in B \ A by B7,XBOOLE_0:def 4;
reconsider a = e as Element of V by B8;
A'\/{a} is linearly-independent by A6,ThI1;
hence A \/ {e} in the_family_of M by A2;
end;
end;
registration
let F be Field;
let V be finite-dimensional VectSp of F;
cluster LinearlyIndependentSubsets V -> finite-membered;
coherence
proof set M = LinearlyIndependentSubsets V;
let A be set;
assume A in the_family_of M; then
A is independent Subset of M by Def8; then
A is linearly-independent Subset of V by Th21;
hence thesis by VECTSP_9:25;
end;
end;
begin :: Maximal Independent Subsets, Ranks, and Basis
definition
let M be SubsetFamilyStr;
let A,C be Subset of M;
pred A is_maximal_independent_in C means:
MAXIMAL:
A is independent & A c= C &
for B being Subset of M st B is independent & B c= C & A c= B holds A = B;
end;
theorem Th:
for M being non void finite-degree SubsetFamilyStr
for C,A being Subset of M st A c= C & A is independent
ex B being independent Subset of M st A c= B & B is_maximal_independent_in C
proof
let M be non void finite-degree SubsetFamilyStr;
let C,A0 be Subset of M; assume
A0: A0 c= C & A0 is independent; then
reconsider AA = A0 as independent Subset of M;
defpred P[Nat] means
for A being finite Subset of M st A0 c= A & A c= C & A is independent
holds card A <= $1;
consider n being Nat such that
A1: for A being finite Subset of M st A is independent holds card A <= n
by Def9;
reconsider n as Element of NAT by ORDINAL1:def 13;
P[n] by A1; then
A2: ex n being Nat st P[n];
consider n0 being Nat such that
A3: P[n0] & for m being Nat st P[m] holds n0 <= m from NAT_1:sch 5(A2);
now
assume
B1: for A being independent Subset of M st A0 c= A & A c= C
holds card A < n0;
card AA < n0 & 0 <= card AA by A0,B1,NAT_1:2; then
(card AA)+1 <= n0 & (card AA)+1 >= 0+1 by NAT_1:13,XREAL_1:8; then
consider n being Nat such that
B2: n0 = 1+n by NAT_1:10,XXREAL_0:2;
reconsider n as Element of NAT by ORDINAL1:def 13;
P[n]
proof let A be finite Subset of M;
assume A0 c= A & A c= C & A is independent; then
card A < n+1 by B1,B2;
hence card A <= n by NAT_1:13;
end; then
n+1 <= n by A3,B2;
hence contradiction by NAT_1:13;
end; then
consider A being independent Subset of M such that
A4: A0 c= A & A c= C & card A >= n0;
take A;
thus A0 c= A & A is independent & A c= C by A4;
let B be Subset of M; assume
A5: B is independent & B c= C & A c= B; then
reconsider B' = B as independent Subset of M;
A0 c= B & card A <= card B' by A4,A5,XBOOLE_1:1,NAT_1:44; then
n0 <= card B' & card B' <= n0 & card A <= n0 by A3,A4,A5,XXREAL_0:2; then
card B' = n0 & card A = n0 by A4,XXREAL_0:1;
hence A = B by A5,CARD_FIN:1;
end;
theorem
for M being non void finite-degree subset-closed SubsetFamilyStr
for C being Subset of M
ex A being independent Subset of M st A is_maximal_independent_in C
proof
let M be non void finite-degree subset-closed SubsetFamilyStr;
let C be Subset of M;
{} the carrier of M c= C & {} the carrier of M is independent
by XBOOLE_1:2; then
ex A being independent Subset of M st
{} the carrier of M c= A & A is_maximal_independent_in C by Th;
hence thesis;
end;
theorem M3:
for M being non empty non void subset-closed finite-degree SubsetFamilyStr
holds
M is Matroid iff
for C being Subset of M, A,B being independent Subset of M
st A is_maximal_independent_in C & B is_maximal_independent_in C
holds card A = card B
proof
let M be non empty non void subset-closed finite-degree SubsetFamilyStr;
hereby assume
A0: M is Matroid;
let C be Subset of M;
B0: now
let A,B be independent Subset of M such that
A1: A is_maximal_independent_in C & B is_maximal_independent_in C and
A2: card A < card B;
(card A)+1 <= card B by A2,NAT_1:13; then
(card A)+1 c= card B by NAT_1:40; then
consider D being set such that
A3: D c= B & Card D = (card A)+1 by CARD_FIL:36;
reconsider D as finite Subset of M by A3,XBOOLE_1:1;
D is independent by A3,M1; then
consider e being Element of M such that
A4: e in D \ A & A \/ {e} is independent by A0,A3,M2;
D \ A c= D by XBOOLE_1:36; then
A5: D \ A c= B & B c= C & A c= C by A1,A3,MAXIMAL,XBOOLE_1:1; then
D \ A c= C by XBOOLE_1:1; then
{e} c= C by A4,ZFMISC_1:37; then
A c= A \/ {e} & A \/ {e} c= C by A5,XBOOLE_1:7,8; then
A \/ {e} = A by A1,A4,MAXIMAL; then
{e} c= A by XBOOLE_1:7; then
e in A by ZFMISC_1:37;
hence contradiction by A4,XBOOLE_0:def 4;
end;
let A,B be independent Subset of M such that
A1: A is_maximal_independent_in C & B is_maximal_independent_in C;
card A < card B or card B < card A or card A = card B by XXREAL_0:1;
hence card A = card B by A1,B0;
end;
assume
A3: for C being Subset of M, A,B being independent Subset of M
st A is_maximal_independent_in C & B is_maximal_independent_in C
holds card A = card B;
M is with_exchange_property
proof
let A,B be finite Subset of M;
reconsider C = A \/ B as Subset of M;
assume
A4: A in the_family_of M & B in the_family_of M & card B = (card A)+1;
assume
A5: for e be Element of M st e in B \ A
holds not A \/ {e} in the_family_of M;
reconsider A as independent Subset of M by A4,Def8;
A6: A is_maximal_independent_in C
proof
thus A in the_family_of M by A4;
thus A c= C by XBOOLE_1:7;
let D be Subset of M; assume
A7: D is independent & D c= C & A c= D;
assume not (A c= D & D c= A); then
consider e being set such that
A8: e in D & not e in A by A7,TARSKI:def 3;
reconsider e as Element of M by A8;
e in B by A7,A8,XBOOLE_0:def 2; then
e in B \ A by A8,XBOOLE_0:def 4; then
{e} c= D & not A \/ {e} in the_family_of M by A5,A8,ZFMISC_1:37; then
A \/ {e} c= D & A \/ {e} is not independent by A7,Def8,XBOOLE_1:8;
hence contradiction by A7,M1;
end;
B c= C & B is independent by Def8,A4,XBOOLE_1:7; then
consider B' being independent Subset of M such that
B1: B c= B' & B' is_maximal_independent_in C by Th;
card A = card B' & card B <= card B' by A3,A6,B1,NAT_1:44;
hence contradiction by A4,NAT_1:13;
end;
hence M is Matroid;
end;
definition
let M be finite-degree Matroid;
let C be Subset of M;
func Rnk C -> Nat equals
union {card A where A is independent Subset of M: A c= C};
coherence
proof
consider n being Nat such that
A1: for A being finite Subset of M st A is independent holds card A <= n
by Def9;
defpred P[Nat] means
for A being independent Subset of M st A c= C holds card A <= $1;
defpred Q[Nat] means
ex A being independent Subset of M st A c= C & $1 = card A;
A2: ex ne being Nat st P[ne]
proof take n;
thus thesis by A1;
end;
consider n0 being Nat such that
A3: P[n0] & for m being Nat st P[m] holds n0 <= m from NAT_1:sch 5(A2);
set X = {card A where A is independent Subset of M: A c= C};
union X = n0
proof
now let a be set; assume a in X; then
consider A being independent Subset of M such that
A4: a = card A & A c= C;
card A <= n0 by A3,A4;
hence a c= n0 by A4,NAT_1:40;
end;
hence union X c= n0 by ZFMISC_1:94;
B1: for k being Nat st Q[k] holds k <= n0 by A3;
card {} = card {} & {} the carrier of M c= C by XBOOLE_1:2; then
B2: ex n being Nat st Q[n];
consider n being Nat such that
B3: Q[n] & for m being Nat st Q[m] holds m <= n from NAT_1:sch 6(B1,B2);
consider A being independent Subset of M such that
B4: A c= C & n = card A by B3;
P[n] by B3; then
n <= n0 & n0 <= n by A3,B3; then
n = n0 by XXREAL_0:1; then
n0 in X by B4;
hence thesis by ZFMISC_1:92;
end;
hence thesis;
end;
end;
theorem ThR0:
for M being finite-degree Matroid
for C being Subset of M
for A being independent Subset of M st A c= C
holds card A <= Rnk C
proof
let M be finite-degree Matroid;
let C be Subset of M;
let A be independent Subset of M;
assume A c= C; then
card A in {card B where B is independent Subset of M: B c= C}; then
card A c= Rnk C by ZFMISC_1:92;
hence card A <= Rnk C by NAT_1:40;
end;
theorem ThR1:
for M being finite-degree Matroid
for C being Subset of M
ex A being independent Subset of M st A c= C & card A = Rnk C
proof
let M be finite-degree Matroid;
let C be Subset of M;
consider n being Nat such that
A1: for A being finite Subset of M st A is independent holds card A <= n
by Def9;
defpred P[Nat] means
for A being independent Subset of M st A c= C holds card A <= $1;
defpred Q[Nat] means
ex A being independent Subset of M st A c= C & $1 = card A;
A2: ex ne being Nat st P[ne]
proof take n;
thus thesis by A1;
end;
consider n0 being Nat such that
A3: P[n0] & for m being Nat st P[m] holds n0 <= m from NAT_1:sch 5(A2);
set X = {card A where A is independent Subset of M: A c= C};
now let a be set; assume a in X; then
consider A being independent Subset of M such that
A4: a = card A & A c= C;
card A <= n0 by A3,A4;
hence a c= n0 by A4,NAT_1:40;
end; then
A5: Rnk C c= n0 by ZFMISC_1:94;
B1: for k being Nat st Q[k] holds k <= n0 by A3;
card {} = card {} & {} the carrier of M c= C by XBOOLE_1:2; then
B2: ex n being Nat st Q[n];
consider n being Nat such that
B3: Q[n] & for m being Nat st Q[m] holds m <= n from NAT_1:sch 6(B1,B2);
consider A being independent Subset of M such that
B4: A c= C & n = card A by B3;
P[n] by B3; then
n <= n0 & n0 <= n by A3,B3; then
B5: n = n0 by XXREAL_0:1; then
n0 in X by B4; then
B6: n0 c= Rnk C by ZFMISC_1:92;
take A; thus thesis by B4,B5,B6,A5,XBOOLE_0:def 10;
end;
theorem ThR2:
for M being finite-degree Matroid
for C being Subset of M
for A being independent Subset of M holds
A is_maximal_independent_in C iff A c= C & card A = Rnk C
proof
let M be finite-degree Matroid;
let C be Subset of M;
set X = {card A where A is independent Subset of M: A c= C};
L: now let A be independent Subset of M; assume
A1: A c= C & card A = Rnk C;
thus A is_maximal_independent_in C
proof thus A is independent & A c= C by A1;
let B be Subset of M; assume B is independent; then
reconsider B' = B as independent Subset of M;
assume B c= C; then
card B' in X; then
A2: card B' c= Rnk C by ZFMISC_1:92;
assume
A3: A c= B; then
card A c= card B' by CARD_1:27; then
card A = card B' by A1,A2,XBOOLE_0:def 10;
hence A = B by A3,CARD_FIN:1;
end;
end;
consider B being independent Subset of M such that
AA: B c= C & card B = Rnk C by ThR1;
let A be independent Subset of M;
hereby assume
A0: A is_maximal_independent_in C;
hence A c= C by MAXIMAL;
B is_maximal_independent_in C by L,AA;
hence card A = Rnk C by A0,AA,M3;
end;
thus thesis by L;
end;
theorem ThR3:
for M being finite-degree Matroid
for C being finite Subset of M
holds Rnk C <= card C
proof
let M be finite-degree Matroid;
let C be finite Subset of M;
ex A being independent Subset of M st A c= C & card A = Rnk C by ThR1;then
Rnk C c= card C by CARD_1:27;
hence Rnk C <= card C by NAT_1:40;
end;
theorem ThR4:
for M being finite-degree Matroid
for C being finite Subset of M holds
C is independent iff card C = Rnk C
proof
let M be finite-degree Matroid;
let C be finite Subset of M;
set X = {card A where A is independent Subset of M: A c= C};
hereby assume
C is independent; then
card C in X; then
card C c= Rnk C by ZFMISC_1:92; then
card C <= Rnk C & Rnk C <= card C by ThR3,NAT_1:40;
hence card C = Rnk C by XXREAL_0:1;
end;
ex A being independent Subset of M st A c= C & card A = Rnk C by ThR1;
hence thesis by CARD_FIN:1;
end;
definition
let M be finite-degree Matroid;
func Rnk M -> Nat equals Rnk [#]M;
coherence;
end;
definition
let M be non void finite-degree SubsetFamilyStr;
mode Basis of M -> independent Subset of M means:
BASIS:
it is_maximal_independent_in [#]M;
existence
proof set C = [#]M;
consider A being independent Subset of M;
consider B being independent Subset of M such that
A1: A c= B & B is_maximal_independent_in C by Th;
take B; thus thesis by A1;
end;
end;
theorem
for M being finite-degree Matroid
for B1,B2 being Basis of M holds card B1 = card B2
proof
let M be finite-degree Matroid;
let B1,B2 be Basis of M;
B1 is_maximal_independent_in [#]M &
B2 is_maximal_independent_in [#]M by BASIS;
hence card B1 = card B2 by M3;
end;
theorem
for M being finite-degree Matroid
for A being independent Subset of M
ex B being Basis of M st A c= B
proof
let M be finite-degree Matroid;
let A be independent Subset of M;
consider B being independent Subset of M such that
A1: A c= B & B is_maximal_independent_in [#]M by Th;
reconsider B as Basis of M by A1,BASIS;
take B;
thus A c= B by A1;
end;
reserve M for finite-degree Matroid,
A,B,C for Subset of M, e,f for Element of M;
theorem R2:
A c= B implies Rnk A <= Rnk B
proof
ex C being independent Subset of M st C c= A & card C = Rnk A by ThR1;
hence thesis by ThR0,XBOOLE_1:1;
end;
theorem R3:
Rnk (A\/B) + Rnk (A/\B) <= Rnk A + Rnk B
proof
consider C being independent Subset of M such that
A0: C c= A/\B & card C = Rnk (A/\B) by ThR1;
A/\B c= A & A/\B c= B by XBOOLE_1:17; then
A8: C c= A & C c= B by A0,XBOOLE_1:1; then
consider Ca being independent Subset of M such that
A2: C c= Ca & Ca is_maximal_independent_in A by Th;
A6: Ca c= A & A c= A\/B by A2,MAXIMAL,XBOOLE_1:7; then
Ca c= A\/B by XBOOLE_1:1; then
consider C' being independent Subset of M such that
A1: Ca c= C' & C' is_maximal_independent_in A\/B by Th;
C'/\B c= B by XBOOLE_1:17; then
consider Cb being independent Subset of M such that
A3: C'/\B c= Cb & Cb is_maximal_independent_in B by Th;
A4: card Ca = Rnk A & card Cb = Rnk B & C' c= A\/B &
card C' = Rnk (A\/B) by A1,A2,A3,ThR2;
A5: C' = Ca \/ (C'/\B)
proof
thus C' c= Ca \/ (C'/\B)
proof
let x be set; assume
B1: x in C';
B3: x in B implies x in C'/\B by B1,XBOOLE_0:def 3;
{x} c= C' by B1,ZFMISC_1:37; then
Ca\/{x} c= C' by A1,XBOOLE_1:8; then
reconsider Cax = Ca\/{x} as independent Subset of M by M1,XBOOLE_1:1;
now assume x in A; then
{x} c= A by ZFMISC_1:37; then
Cax c= A & Ca c= Cax by A6,XBOOLE_1:7,8; then
Ca = Cax by A2,MAXIMAL; then
{x} c= Ca by XBOOLE_1:7;
hence x in Ca by ZFMISC_1:37;
end;
hence thesis by B1,B3,A4,XBOOLE_0:def 2;
end;
let x be set; assume x in Ca \/ (C'/\B); then
x in Ca or x in C'/\B by XBOOLE_0:def 2;
hence x in C' by A1,XBOOLE_0:def 3;
end;
A7: Ca/\(C'/\B) = Ca/\C'/\B by XBOOLE_1:16 .= Ca/\B by A1,XBOOLE_1:28;
Ca/\B = C
proof
thus Ca/\B c= C
proof
let x be set; assume x in Ca/\B; then
B1: x in Ca & x in B by XBOOLE_0:def 3; then
{x} c= Ca by ZFMISC_1:37; then
C\/{x} c= Ca by A2,XBOOLE_1:8; then
reconsider Cx = C\/{x} as independent Subset of M by M1,XBOOLE_1:1;
x in A/\B by B1,A6,XBOOLE_0:def 3; then
{x} c= A/\B by ZFMISC_1:37; then
Cx c= A/\B & C c= Cx & C is_maximal_independent_in A/\B
by A0,ThR2,XBOOLE_1:7,8; then
C = Cx by MAXIMAL; then
{x} c= C by XBOOLE_1:7;
hence x in C by ZFMISC_1:37;
end;
thus thesis by A8,A2,XBOOLE_1:19;
end; then
Rnk (A\/B) = Rnk A + card (C'/\B) - Rnk (A/\B)
by A0,A4,A5,A7,CARD_2:64; then
Rnk (A\/B) + Rnk (A/\B) = Rnk A + card (C'/\B) & card (C'/\B) <= Rnk B
by A3,A4,NAT_1:44;
hence thesis by XREAL_1:8;
end;
theorem R4:
Rnk A <= Rnk (A\/B) & Rnk (A \/ {e}) <= Rnk A + 1
proof
thus Rnk A <= Rnk (A\/B) by R2,XBOOLE_1:7;
A1: Rnk(A\/{e}) + Rnk(A/\{e}) <= Rnk A + Rnk {e} by R3;
A2: Rnk(A\/{e}) <= Rnk(A\/{e}) + Rnk(A/\{e}) by NAT_1:11;
Rnk {e} <= card {e} & card {e} = 1 by ThR3,CARD_1:50; then
Rnk A + Rnk {e} <= Rnk A + 1 by XREAL_1:8; then
Rnk(A\/{e}) + Rnk(A/\{e}) <= Rnk A + 1 by A1,XXREAL_0:2;
hence thesis by A2,XXREAL_0:2;
end;
theorem
Rnk (A\/{e}) = Rnk (A\/{f}) & Rnk (A\/{f}) = Rnk A implies
Rnk (A \/ {e,f}) = Rnk A
proof
consider C being independent Subset of M such that
A0: C c= A & card C = Rnk A by ThR1;
A c= A\/{e,f} & A c= A\/{e} & A c= A\/{f} by XBOOLE_1:7; then
A6: C c= A\/{e,f} & C c= A\/{e} & C c= A\/{f} by A0,XBOOLE_1:1; then
consider C' being independent Subset of M such that
A1: C c= C' & C' is_maximal_independent_in A\/{e,f} by Th;
A2: card C' = Rnk (A \/ {e,f}) & C is_maximal_independent_in A &
C' c= A\/{e,f} by A0,A1,ThR2;
assume Rnk (A\/{e}) = Rnk (A\/{f}) & Rnk (A\/{f}) = Rnk A; then
A3: C is_maximal_independent_in A\/{e} & C is_maximal_independent_in A\/{f}
by A0,A6,ThR2;
now assume C' <> C; then
consider x being set such that
A4: not (x in C' iff x in C) by TARSKI:2;
{x} c= C' by A1,A4,ZFMISC_1:37; then
C\/{x} c= C' by A1,XBOOLE_1:8; then
reconsider Cx = C\/{x} as independent Subset of M by M1,XBOOLE_1:1;
now assume x in A; then
{x} c= A by ZFMISC_1:37; then
Cx c= A & C c= Cx by A0,XBOOLE_1:8,7; then
C = Cx by A2,MAXIMAL; then
{x} c= C by XBOOLE_1:7;
hence contradiction by A1,A4,ZFMISC_1:37;
end; then
x in {e,f} by A1,A2,A4,XBOOLE_0:def 2; then
x = e or x = f by TARSKI:def 2; then
{x} c= A\/{e} & C c= A\/{e} or {x} c= A\/{f} & C c= A\/{f}
by A0,XBOOLE_1:10; then
C c= Cx & (Cx c= A\/{e} or Cx c= A\/{f}) by XBOOLE_1:8,7; then
C = Cx by A3,MAXIMAL; then
{x} c= C by XBOOLE_1:7;
hence contradiction by A1,A4,ZFMISC_1:37;
end;
hence Rnk (A \/ {e,f}) = Rnk A by A0,A2;
end;
begin :: Dependence from a Set, Spans, and Cycles
definition
let M be finite-degree Matroid;
let e be Element of M;
let A be Subset of M;
pred e is_dependent_on A means:
DF:
Rnk (A \/ {e}) = Rnk A;
end;
theorem ThD1:
e in A implies e is_dependent_on A
proof
assume e in A; then
{e} c= A by ZFMISC_1:37;
hence Rnk(A\/{e}) = Rnk A by XBOOLE_1:12;
end;
theorem ThD2:
A c= B & e is_dependent_on A implies e is_dependent_on B
proof assume
A0: A c= B & Rnk (A \/ {e}) = Rnk A;
consider Ca being independent Subset of M such that
A1: Ca c= A & card Ca = Rnk A by ThR1;
B4: Ca c= B by A0,A1,XBOOLE_1:1;
A5: B c= B\/{e} by XBOOLE_1:7;
A4: Rnk B <= Rnk (B\/{e}) & Rnk (B\/{e}) <= Rnk B + 1 by R4;
Ca c= B\/{e} by B4,A5,XBOOLE_1:1; then
consider E being independent Subset of M such that
A6: Ca c= E & E is_maximal_independent_in B\/{e} by Th;
now assume
B1: Rnk (B\/{e}) = Rnk B + 1; then
C1: card E = Rnk B + 1 by A6,ThR2;
card (E/\B) <= Rnk B by ThR0,XBOOLE_1:17; then
C2: card (E/\B)+1 <= Rnk B + 1 by XREAL_1:8;
E c= B\/{e} by A6,ThR2; then
E = E/\(B\/{e}) by XBOOLE_1:28 .= E/\B\/E/\{e} by XBOOLE_1:23; then
Rnk B + 1 <= card (E/\B) + card (E/\{e}) by C1,CARD_2:62; then
card (E/\B)+1 <= card (E/\B) + card (E/\{e}) & E/\{e} c= {e}
by C2,XXREAL_0:2,XBOOLE_1:17; then
1 <= card (E/\{e}) & (E/\{e} = {} & card {} = 0 or
E/\{e} = {e} & card {e} = 1) by XREAL_1:8,ZFMISC_1:39,CARD_1:50; then
e in E/\{e} by TARSKI:def 1; then
e in E by XBOOLE_0:def 3; then
{e} c= E by ZFMISC_1:37; then
A3: Ca\/{e} c= E & Ca\/{e} c= A\/{e} & Ca c= A\/{e} & Ca c= Ca\/{e}
by A1,A6,XBOOLE_1:8,9,10;
Ca\/{e} is independent & Ca is_maximal_independent_in A\/{e}
by A0,A1,A3,M1,ThR2; then
Ca = Ca\/{e} by A3,MAXIMAL; then
{e} c= Ca by XBOOLE_1:7; then
B = B\/{e} by B4,XBOOLE_1:1,12;
hence contradiction by B1;
end;
hence Rnk (B\/{e}) = Rnk B by A4,NAT_1:9;
end;
definition
let M be finite-degree Matroid;
let A be Subset of M;
func Span A -> Subset of M equals
{e where e is Element of M: e is_dependent_on A};
coherence
proof
set X = {e where e is Element of M: e is_dependent_on A};
X c= the carrier of M
proof
let x be set; assume x in X; then
ex e being Element of M st x = e & e is_dependent_on A;
hence thesis;
end;
hence thesis;
end;
end;
theorem SPAN:
e in Span A iff Rnk (A \/ {e}) = Rnk A
proof
hereby assume e in Span A; then
ex x being Element of M st e = x & x is_dependent_on A;
hence Rnk (A \/ {e}) = Rnk A by DF;
end;
assume Rnk (A \/ {e}) = Rnk A; then
e is_dependent_on A by DF;
hence thesis;
end;
theorem S1:
A c= Span A
proof
let e be set; assume
A0: e in A; then
reconsider x = e as Element of M;
x is_dependent_on A by A0,ThD1;
hence thesis;
end;
theorem
A c= B implies Span A c= Span B
proof assume
A0: A c= B;
let x be set; assume x in Span A; then
ex e st x = e & e is_dependent_on A; then
ex e st x = e & e is_dependent_on B by A0,ThD2;
hence thesis;
end;
theorem S0:
Rnk Span A = Rnk A
proof
A0: A c= Span A by S1;
consider Ca being independent Subset of M such that
B2: Ca c= A & card Ca = Rnk A by ThR1;
Ca c= Span A by A0,B2,XBOOLE_1:1; then
consider C being independent Subset of M such that
A2: Ca c= C & C is_maximal_independent_in Span A by Th;
now assume C c/= Ca; then
consider x being set such that
A3: x in C & x nin Ca by TARSKI:def 3;
C c= Span A by A2,ThR2; then
x in Span A by A3; then
consider e being Element of M such that
A4: x = e & e is_dependent_on A;
{e} c= C by A3,A4,ZFMISC_1:37; then
Ca\/{e} c= C by A2,XBOOLE_1:8; then
reconsider Ce = Ca\/{e} as independent Subset of M by M1;
Ce c= A\/{e} by B2,XBOOLE_1:9; then
consider D being independent Subset of M such that
A6: Ce c= D & D is_maximal_independent_in A\/{e} by Th;
card Ca = Rnk (A\/{e}) by B2,A4,DF .= card D by A6,ThR2; then
card Ce <= card Ca & card Ca <= card Ce by A6,XBOOLE_1:7,NAT_1:44; then
card Ca = card Ce by XXREAL_0:1; then
Ca = Ce by XBOOLE_1:7,CARD_FIN:1; then
e nin {e} by A3,A4,XBOOLE_0:def 2;
hence contradiction by TARSKI:def 1;
end; then
C = Ca by A2,XBOOLE_0:def 10;
hence thesis by B2,A2,ThR2;
end;
theorem Sd:
e is_dependent_on Span A implies e is_dependent_on A
proof assume
Z0: Rnk ((Span A)\/{e}) = Rnk Span A;
consider Ca being independent Subset of M such that
B2: Ca c= A & card Ca = Rnk A by ThR1;
A0: A c= Span A by S1; then
Ca c= Span A by B2,XBOOLE_1:1; then
consider C being independent Subset of M such that
A2: Ca c= C & C is_maximal_independent_in Span A by Th;
A3: Rnk A = Rnk Span A & Rnk Span A = card C & C c= Span A
by A2,ThR2,S0;
Ca c= A\/{e} & A\/{e} c= (Span A)\/{e} by B2,A0,XBOOLE_1:9,10; then
Rnk A = Rnk Ca & Rnk Ca <= Rnk(A\/{e}) & Rnk(A\/{e}) <= Rnk A
by Z0,B2,R2,A3,ThR4;
hence Rnk (A\/{e}) = Rnk A by XXREAL_0:1;
end;
theorem
Span Span A = Span A
proof
thus Span Span A c= Span A
proof
let x be set; assume x in Span Span A; then
consider e being Element of M such that
A0: x = e & e is_dependent_on Span A;
e is_dependent_on A by A0,Sd;
hence thesis by A0;
end;
thus thesis by S1;
end;
theorem
f nin Span A & f in Span (A \/ {e}) implies e in Span (A \/ {f})
proof assume that
Z1: f nin Span A and
Z2: f in Span (A \/ {e});
A3: Rnk A <> Rnk (A\/{f}) & Rnk(A\/{e}\/{f}) = Rnk(A\/{e}) by Z1,Z2,SPAN;
Rnk A <= Rnk (A\/{f}) & Rnk (A\/{f}) <= Rnk A + 1 by R4; then
A4: Rnk (A\/{f}) = Rnk A + 1 by A3,NAT_1:9;
A5: A\/{f} c= A\/{f}\/{e} & A\/{f}\/{e} = A\/({f}\/{e}) &
A\/{e}\/{f} = A\/({e}\/{f}) by XBOOLE_1:4,7; then
Rnk(A\/{f}) <= Rnk(A\/{e}) & Rnk (A\/{e}) <= Rnk A + 1
by A3,R4; then
Rnk (A\/{f}) = Rnk (A\/{f}\/{e}) by A3,A4,A5,XXREAL_0:1;
hence e in Span (A \/ {f}) by SPAN;
end;
definition
let M be SubsetFamilyStr;
let A be Subset of M;
attr A is cycle means:
CYCLE:
A is dependent &
for e being Element of M st e in A holds A \ {e} is independent;
end;
theorem LemC:
A is cycle implies A is non empty finite
proof assume that
A0: A is dependent and
A1: for e being Element of M st e in A holds A \ {e} is independent;
{} the carrier of M is independent;
hence A is non empty by A0;
consider e being Element of A;
now assume A is non empty set; then
A2: e in A; then
reconsider e as Element of M;
reconsider Ae = A\{e} as independent Subset of M by A1,A2;
A = Ae\/{e} by A2,ZFMISC_1:140;
hence thesis;
end;
hence thesis;
end;
registration
let M;
cluster cycle -> non empty finite Subset of M;
coherence by LemC;
end;
theorem C5:
A is cycle iff
A is non empty & for e st e in A holds A\{e} is_maximal_independent_in A
proof
thus A is cycle implies A is non empty &
for e st e in A holds A\{e} is_maximal_independent_in A
proof assume that
Z0: A is dependent and
Z2: for e being Element of M st e in A holds A \ {e} is independent;
{} the carrier of M is independent;
hence A is non empty by Z0;
let e; assume
Z1: e in A;
set Ae = A\{e};
A1: A = Ae\/{e} by Z1,ZFMISC_1:140;
thus Ae is independent & Ae c= A by Z2,Z1,XBOOLE_1:36;
let B; assume B is independent & B c= A & Ae c= B;
hence Ae = B by Z0,A1,BORSUK_5:2;
end;
consider a being Element of A;
assume that
Z4: A is non empty and
Z3: for e st e in A holds A\{e} is_maximal_independent_in A;
a in A by Z4; then
reconsider a as Element of M;
set Ae = A\{a};
A2: Ae is_maximal_independent_in A by Z4,Z3;
A3: Ae c= A by XBOOLE_1:36;
hereby
assume A is independent; then
A = Ae by A2,A3,MAXIMAL; then
a nin {a} by Z4,XBOOLE_0:def 4;
hence contradiction by TARSKI:def 1;
end;
let e; assume e in A; then
A\{e} is_maximal_independent_in A by Z3;
hence thesis by MAXIMAL;
end;
theorem C4:
A is cycle implies Rnk A + 1 = Card A
proof assume
A0: A is cycle; then
reconsider A as non empty finite Subset of M;
consider a being Element of A;
A1: A\{a} is_maximal_independent_in A by A0,C5; then
A\{a} is independent by MAXIMAL; then
A2: Rnk A = card (A\{a}) by A1,ThR2;
a in {a} by TARSKI:def 1; then
a nin A\{a} & A = (A\{a})\/{a} by XBOOLE_0:def 4,ZFMISC_1:140;
hence thesis by A2,CARD_2:54;
end;
theorem
A is cycle & e in A implies e is_dependent_on A\{e}
proof assume
Z0: A is cycle & e in A; then
reconsider Ae = A\{e} as independent Subset of M by CYCLE;
Ae is_maximal_independent_in A by Z0,C5; then
Rnk A = card Ae by ThR2;
hence Rnk((A\{e})\/{e}) = card Ae by Z0,ZFMISC_1:140
.= Rnk (A\{e}) by ThR4;
end;
theorem C1:
A is cycle & B is cycle & A c= B implies A = B
proof assume that
A0: A is dependent and
for e st e in A holds A \ {e} is independent and
B is dependent and
AA: for e st e in B holds B \ {e} is independent;
assume
A1: A c= B & A <> B; then
consider x being set such that
A2: not (x in A iff x in B) by TARSKI:2;
reconsider x as Element of M by A2;
A c= B\{x} & B\{x} is independent by AA,A1,A2,ZFMISC_1:40;
hence contradiction by A0,M1;
end;
theorem C3:
(for B st B c= A holds B is not cycle) implies A is independent
proof assume
Z0: for B st B c= A holds B is not cycle;
consider C being independent Subset of M such that
Z1: C c= A & card C = Rnk A by ThR1;
per cases;
suppose A c= C; hence thesis by Z1,XBOOLE_0:def 10; end;
suppose A c/= C; then
consider x being set such that
Z2: x in A & x nin C by TARSKI:def 3;
reconsider x as Element of M by Z2;
A2: C\/{x} c= A & C c= C\/{x} by Z1,Z2,SETWISEO:8;
defpred P[Nat] means
ex B being independent Subset of M
st card B = $1 & B c= C & B\/{x} is dependent;
Z3: ex n being Nat st P[n]
proof take n = Rnk A, C;
thus card C = n & C c= C by Z1;
A1: C is_maximal_independent_in A by Z1,ThR2;
assume C\/{x} is independent; then
C = C\/{x} by A1,A2,MAXIMAL; then
{x} c= C by XBOOLE_1:7;
hence contradiction by Z2,ZFMISC_1:37;
end;
consider n being Nat such that
Z4: P[n] & for k being Nat st P[k] holds n <= k from NAT_1:sch 5(Z3);
consider B being independent Subset of M such that
Z5: card B = n & B c= C & B\/{x} is dependent by Z4;
B c= A by Z1,Z5,XBOOLE_1:1; then
Z6: B\/{x} c= A & x nin B by Z2,Z5,SETWISEO:8;
B\/{x} is cycle
proof
thus B\/{x} is dependent by Z5;
let e be Element of M;
set Be = B\{e};
A5: Be c= B by XBOOLE_1:36;
assume
A3: e in B\/{x};
per cases by A3,SETWISEO:6;
suppose
B1: e in B; then
B = Be\/{e} & e nin Be by ZFMISC_1:64,140; then
B3: n = card Be+1 by Z5,CARD_2:54;
assume
B2: (B\/{x}) \ {e} is dependent;
(B\/{x}) \ {e} = Be\/{x} by B1,Z6,ZFMISC_1:17,XBOOLE_1:87; then
n <= card Be by Z4,A5,B2,Z5,XBOOLE_1:1;
hence contradiction by B3,NAT_1:13;
end;
suppose e = x;
hence (B\/{x}) \ {e} is independent by Z6,ZFMISC_1:141;
end;
end;
hence A is independent by Z6,Z0;
end;
end;
theorem C2:
A is cycle & B is cycle & A <> B & e in A /\ B implies
ex C st C is cycle & C c= (A \/ B) \ {e}
proof assume that
Z0: A is cycle & B is cycle & A <> B & e in A /\ B and
Z1: for C st C is cycle holds C c/= (A \/ B) \ {e};
A0: e in A & e in B by Z0,XBOOLE_0:def 3; then
reconsider Ae = A\{e}, Be = B\{e} as independent Subset of M by Z0,CYCLE;
A1: A = Ae\/{e} & B = Be\/{e} by A0,ZFMISC_1:140;
reconsider A' = A, B' = B as finite Subset of M by Z0;
A3: Rnk(A\/B)+Rnk(A/\B) <= Rnk A + Rnk B by R3;
B2: e in {e} by TARSKI:def 1; then
e nin Ae & e nin Be by XBOOLE_0:def 4; then
A4: card A' = card Ae+1 & card B' = card Be+1 by A1,CARD_2:54; then
Rnk A + 1 = card Ae+1 & Rnk B + 1 = card Be+1 by Z0,C4; then
A5: card(A'\/B')+card(A'/\B') = Rnk A+1 + (Rnk B+1) by A4,HALLMAR1:1 .=
Rnk A + Rnk B+1+1;
Rnk(A\/B)+Rnk(A/\B)+1 <= Rnk A + Rnk B+1 by A3,XREAL_1:8; then
A7: Rnk(A\/B)+Rnk(A/\B)+1+1 <= card(A'\/B')+card(A'/\B') by A5,XREAL_1:8;
A9: A/\B c= A & A/\B c= B by XBOOLE_1:17;
A c/= A/\B by Z0,C1,A9,XBOOLE_1:1; then
consider a being set such that
B0: a in A & a nin A/\B by TARSKI:def 3;
reconsider a as Element of M by B0;
{a} misses A/\B by B0,ZFMISC_1:56; then
A/\B c= A\{a} & A\{a} is independent by Z0,A9,B0,CYCLE,XBOOLE_1:86; then
A/\B is independent by M1; then
card (A'/\B') = Rnk (A/\B) by ThR4; then
Z2: Rnk(A\/B)+Rnk(A/\B)+1+1 = Rnk(A\/B)+1+1+card(A'/\B');
for C st C c= (A \/ B) \ {e} holds C is not cycle by Z1; then
reconsider C = (A\/B)\{e} as independent Subset of M by C3;
B1: e nin C & e in A\/B by B2,A0,XBOOLE_0:def 2,def 4; then
B3: C\/{e} = A'\/B' by ZFMISC_1:140;
C is_maximal_independent_in A\/B
proof
thus C is independent & C c= A\/B by XBOOLE_1:36;
let D be Subset of M;
A is dependent & A c= A\/B by Z0,CYCLE,XBOOLE_1:7; then
A\/B is dependent by M1;
hence thesis by B3,BORSUK_5:2;
end; then
Rnk(A\/B)+1 = card C+1 by ThR2 .= card(A'\/B') by B1,B3,CARD_2:54;
hence contradiction by Z2,A7,NAT_1:13;
end;
theorem
A is independent & B is cycle & C is cycle & B c= A\/{e} & C c= A\/{e}
implies B = C
proof assume that
A0: A is independent & B is cycle & C is cycle and
A1: B c= A\/{e} & C c= A\/{e};
now assume B c= A; then
B is independent by A0,M1;
hence contradiction by A0,CYCLE;
end; then
consider b being set such that
A2: b in B & b nin A by TARSKI:def 3;
b in {e} by A1,A2,XBOOLE_0:def 2; then
A3: b = e by TARSKI:def 1;
now assume C c= A; then
C is independent by A0,M1;
hence contradiction by A0,CYCLE;
end; then
consider c being set such that
A4: c in C & c nin A by TARSKI:def 3;
c in {e} by A1,A4,XBOOLE_0:def 2; then
c = e by TARSKI:def 1; then
A5: e in B/\C by A2,A3,A4,XBOOLE_0:def 3;
assume B <> C; then
consider D being Subset of M such that
A6: D is cycle & D c= (B \/ C) \ {e} by A0,A5,C2;
D c= A
proof
let x be set; assume x in D; then
A7: x in B\/C & x nin {e} by A6,XBOOLE_0:def 4; then
x in B or x in C by XBOOLE_0:def 2;
hence thesis by A1,A7,XBOOLE_0:def 2;
end; then
D is independent by A0,M1;
hence thesis by A6,CYCLE;
end;