:: Introduction to Matroids
:: by Grzegorz Bancerek and Yasunari Shidama
::
:: Received July 30, 2008
:: Copyright (c) 2008-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, TARSKI, PRE_TOPC, SUBSET_1, BVFUNC_2, RCOMP_1, SETFAM_1,
CLASSES1, FINSET_1, CARD_1, ARYTM_3, XBOOLE_0, STRUCT_0, ZFMISC_1, NAT_1,
XXREAL_0, TAXONOM2, AOFA_000, ORDERS_1, FUNCT_1, RELAT_1, NATTRA_1,
EQREL_1, VECTSP_1, RLVECT_3, CARD_3, RLVECT_2, SUPINF_2, REALSET1,
ARYTM_1, RLVECT_5, JORDAN13, MATROID0;
notations TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, SETFAM_1, FINSET_1, ORDINAL1,
NUMBERS, FUNCT_1, RELSET_1, FUNCT_2, EQREL_1, ORDERS_1, TAXONOM2,
XCMPLX_0, XXREAL_0, NAT_1, CARD_1, CLASSES1, AOFA_000, STRUCT_0,
RLVECT_1, VECTSP_1, VECTSP_6, VECTSP_7, PRE_TOPC, TDLAT_3, MATRLIN,
PENCIL_1, RANKNULL;
constructors COH_SP, TDLAT_3, TAXONOM2, RANKNULL, VECTSP_7, PENCIL_1,
REALSET1, RELSET_1;
registrations FINSET_1, CARD_1, RELSET_1, STRUCT_0, SUBSET_1, PENCIL_1,
TDLAT_3, SETFAM_1, EQREL_1, MATRLIN, XREAL_0, ALGSTR_0, BINOM, RLVECT_1,
VECTSP_1, VECTSP_7, ORDINAL1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, FUNCT_1, CLASSES1, TAXONOM2, XBOOLE_0, STRUCT_0, PENCIL_1,
FINSET_1;
equalities XBOOLE_0, STRUCT_0, ORDINAL1;
expansions TARSKI, FUNCT_1, XBOOLE_0, STRUCT_0, 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, CARD_2,
VECTSP_4, ORDINAL1, CARD_FIL, RANKNULL, VECTSP_1, VECTSP_6, ALGSTR_0,
HALLMAR1;
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 :: redefines independent (MATROID0, synonym) → open (PRE_TOPC, definition)
: Def2:
A in the_family_of M;
compatibility by PRE_TOPC:def 2;
end;
definition
let M be SubsetFamilyStr;
attr M is subset-closed means
: Def3:
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 for SubsetFamilyStr;
existence
proof
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
A1: card B = (card A) + 1;
reconsider e = 0 as Element of M by TARSKI:def 1;
take e;
A2: bool {0} = {{},{0}} by ZFMISC_1:24;
then
A3: B = {} or B = {0} by TARSKI:def 2;
A4: A = {} or A = {0} by A2,TARSKI:def 2;
then card A = 0 or card A = 1 by CARD_1:30;
hence thesis by A1,A4,A3;
end;
end;
registration
let M be non void SubsetFamilyStr;
cluster independent for Subset of M;
existence
proof
set a = the 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 Def3;
end;
theorem Th1:
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
A1: B c= A;
A in the_family_of M by Def2;
then B in the_family_of M by A1,CLASSES1:def 1;
hence thesis by Def2;
end;
registration
let M be non void subset-closed SubsetFamilyStr;
cluster finite independent for Subset of M;
existence
proof
set a = the Element of the topology of M;
reconsider a as independent Subset of M by PRE_TOPC:def 2;
{} c= a;
then reconsider b = {} as independent Subset of M by Th1;
take b;
thus thesis;
end;
end;
definition
mode Matroid is non empty non void subset-closed with_exchange_property
SubsetFamilyStr;
end;
theorem Th2:
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 M9 = M as non void subset-closed SubsetFamilyStr;
set a = the independent Subset of M9;
{} c= a;
then {} is independent Subset of M9 by Th1;
hence {} in the_family_of M by Def2;
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 empty -> independent for Subset of M;
coherence
by Th2;
end;
theorem Th3:
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 Th1;
assume
A1: 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
A2: x is independent Subset of M by Def2;
assume y c= x;
then y is independent Subset of M by A1,A2,XBOOLE_1:1;
hence thesis by Def2;
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 for Subset of M;
coherence
by Th3,XBOOLE_1:17;
cluster B/\A -> independent for Subset of M;
coherence;
cluster A\B -> independent for Subset of M;
coherence
by Th3,XBOOLE_1:36;
end;
theorem Th4:
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;
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
A1: 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 that
A2: A in the_family_of M and
A3: B in the_family_of M and
A4: card B = (card A) + 1;
consider e being Element of M such that
A5: e in B \ A and
A6: A \/ {e} in the_family_of M by A1,A2,A3,A4;
take e;
thus e in B \ A & A \/ {e} in the_family_of M by A5,A6;
end;
assume
A7: 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 that
A8: A in the_family_of M and
A9: B in the_family_of M;
A10: B is independent by A9;
assume
A11: card B = (card A) + 1;
A is independent by A8;
then consider e being Element of M such that
A12: e in B \ A and
A13: A \/ {e} is independent by A7,A10,A11;
take e;
thus thesis by A12,A13;
end;
definition
::$CD
let M be SubsetFamilyStr;
attr M is finite-membered means
: Def5:
the_family_of M is finite-membered;
end;
definition
let M be SubsetFamilyStr;
attr M is finite-degree means
: Def6:
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 for SubsetFamilyStr;
coherence;
cluster finite -> finite-degree for 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 card X;
let A be finite Subset of M;
thus thesis by NAT_1:43;
end;
end;
begin :: Examples
registration
cluster mutually-disjoint non empty with_non-empty_elements for set;
existence
proof
take {{0}};
thus thesis by TAXONOM2:10;
end;
end;
theorem Th5:
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:43;
then consider x being object such that
A1: x in B and
A2: x nin A;
take x;
thus thesis by A1,A2,XBOOLE_0:def 5;
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 object;
assume that
A1: x1 in dom f and
A2: x2 in dom f and
A3: f.x1 = f.x2;
reconsider x1,x2 as set by TARSKI:1;
A4: not {} in P;
then
A5: f.x1 in x1 by A1,ORDERS_1:89;
f.x1 in x2 by A2,A3,A4,ORDERS_1:89;
then x1 meets x2 by A5,XBOOLE_0:3;
hence thesis by A1,A2,TAXONOM2:def 5;
end;
registration
cluster -> non void subset-closed with_exchange_property for discrete
SubsetFamilyStr;
coherence
proof
let T be discrete SubsetFamilyStr;
the topology of T is non empty by TDLAT_3:def 1;
hence
A1: T is non void;
for A,B being Subset of T st A is independent & B c= A holds B is
independent by TDLAT_3:15;
hence T is subset-closed by A1,Th3;
let A,B be finite Subset of T such that
A in the_family_of T and
B in the_family_of T and
A2: card B = card A + 1;
now
assume B c= A;
then Segm card B c= Segm card A by CARD_1:11;
then card B <= card A by NAT_1:39;
then card B + 0 < card A + 1 by XREAL_1:8;
hence contradiction by A2;
end;
then consider x being object such that
A3: x in B and
A4: not x in A;
reconsider x as Element of T by A3;
{x} c= the carrier of T by A3,ZFMISC_1:31;
then reconsider C = A \/ {x} as Subset of T by XBOOLE_1:8;
take x;
thus x in B \ A by A3,A4,XBOOLE_0:def 5;
C is independent by TDLAT_3:15;
hence thesis;
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
: Def7:
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 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}};
set X = union P;
F c= bool X
proof
let x be object;
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 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 Def7;
hence the carrier of M is non empty;
end;
end;
theorem Th8:
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;
A1: 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 Def7;
let A be Subset of ProdMatroid P;
A2: the carrier of M = union P by Def7;
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
A3: 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 A1;
let D be Element of P;
P = {} implies A = {} & {} /\ D = {} by A2,ZFMISC_1:2;
then P = {} implies A /\ D c= {1};
then consider d being set such that
A4: A /\ D c= {d} by A3;
set d0 = the Element of D;
now
assume d nin D;
then d nin A /\ D by XBOOLE_0:def 4;
then A /\ D <> {d} by TARSKI:def 1;
then A /\ D = {} by A4,ZFMISC_1:33;
hence A /\ D c= {d0};
end;
hence thesis by A4;
end;
assume
A5: for D being Element of P ex d being Element of D st A /\ D c= {d};
A6: now
let D be set;
assume D in P;
then ex d being Element of D st A /\ D c= {d} by A5;
hence ex d being set st A /\ D c= {d};
end;
the carrier of M = union P by Def7;
hence A in the_family_of M by A1,A6;
end;
registration
let P be set;
cluster ProdMatroid P -> non void subset-closed;
coherence
proof
set M = ProdMatroid P;
A1: 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 Def7;
set A = {} union P;
now
let D be set;
assume D in P;
take d={};
thus A /\ D c= {d};
end;
then A in the_family_of M by A1;
hence the topology of M is non empty;
thus the_family_of M is subset-closed
proof
let a,b be set;
assume that
A2: a in the_family_of M and
A3: b c= a;
A4: 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 A1,A2;
A5: now
let D be set;
assume D in P;
then consider d being set such that
A6: a /\ D c= {d} by A4;
take d;
b /\ D c= a /\ D by A3,XBOOLE_1:26;
hence b /\ D c= {d} by A6;
end;
b is Subset of union P by A3,A4,XBOOLE_1:1;
hence thesis by A1,A5;
end;
end;
end;
theorem Th9:
for P being mutually-disjoint set for x being Subset of
ProdMatroid P ex f being Function of x,P st
for a being object st a in x holds a in f.a
proof
defpred P[object,object] means ex D2 being set st D2 = $2 & $1 in D2;
let P be mutually-disjoint set;
let x be Subset of ProdMatroid P;
A1: now
let a be object;
assume a in x;
then a in the carrier of ProdMatroid P;
then a in union P by Def7;
then ex y being set st a in y & y in P by TARSKI:def 4;
hence ex y being object st y in P & P[a,y];
end;
consider f being Function of x,P such that
A2: for a being object st a in x holds P[a,f.a] from FUNCT_2:sch 1(A1);
take f;
let a be object;
assume a in x;
then P[a,f.a] by A2;
hence thesis;
end;
theorem Th10:
for P being mutually-disjoint set for x being Subset of
ProdMatroid P for f being Function of x,P st
for a being object 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
A1: for a being object st a in x holds a in f.a;
hereby
assume
A2: x is independent;
thus f is one-to-one
proof
let a,b be object;
assume that
A3: a in dom f and
A4: b in dom f;
A5: f.b in rng f by A4,FUNCT_1:def 3;
f.a in rng f by A3,FUNCT_1:def 3;
then reconsider D1 = f.a, D2 = f.b as Element of P by A5;
a in D1 by A1,A3;
then
A6: a in x /\ D1 by A3,XBOOLE_0:def 4;
consider d2 being Element of D2 such that
A7: x /\ D2 c= {d2} by A2,Th8;
b in D2 by A1,A4;
then b in x /\ D2 by A4,XBOOLE_0:def 4;
then b = d2 by A7,TARSKI:def 1;
hence thesis by A7,A6,TARSKI:def 1;
end;
end;
assume
A8: f is one-to-one;
now
let D be Element of P;
set d1 = the Element of D;
assume
A9: for d being Element of D holds x /\ D c/= {d};
then x /\ D c/= {d1};
then consider d2 being object such that
A10: d2 in x /\ D and
d2 nin {d1};
A11: d2 in D by A10,XBOOLE_0:def 4;
A12: d2 in x by A10,XBOOLE_0:def 4;
then d2 in f.d2 by A1;
then
A13: f.d2 meets D by A11,XBOOLE_0:3;
the carrier of ProdMatroid P = union P by Def7;
then ex y being set st d2 in y & y in P by A10,TARSKI:def 4;
then
A14: dom f = x by FUNCT_2:def 1;
then f.d2 in rng f by A12,FUNCT_1:def 3;
then
A15: f.d2 = D by A13,TAXONOM2:def 5;
x /\ D c= {d2}
proof
let a be object;
assume
A16: a in x /\ D;
then
A17: a in x by XBOOLE_0:def 4;
A18: a in D by A16,XBOOLE_0:def 4;
a in f.a by A1,A17;
then
A19: f.a meets D by A18,XBOOLE_0:3;
f.a in rng f by A14,A17,FUNCT_1:def 3;
then f.a = D by A19,TAXONOM2:def 5;
then a = d2 by A8,A12,A14,A15,A17;
hence thesis by TARSKI:def 1;
end;
hence contradiction by A9,A11;
end;
hence thesis by Th8;
end;
registration
let P be mutually-disjoint set;
cluster ProdMatroid P -> with_exchange_property;
coherence
proof
set M = ProdMatroid P;
A1: 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 Def7;
let A,B be finite Subset of M;
assume that
A2: A in the_family_of M and
A3: B in the_family_of M;
consider f being Function of A,P such that
A4: for a being object st a in A holds a in f.a by Th9;
assume card B = (card A) + 1;
then
A5: card B > card A by NAT_1:13;
consider g being Function of B,P such that
A6: for a being object st a in B holds a in g.a by Th9;
A7: the carrier of ProdMatroid P = union P by Def7;
then P = {} implies A = {} by ZFMISC_1:2;
then
A8: dom f = A by FUNCT_2:def 1;
reconsider A9 = rng f, B9 = rng g as finite set;
A9: A is independent by A2;
then f is one-to-one by A4,Th10;
then A, A9 are_equipotent by A8,WELLORD2:def 4;
then
A10: card A = card A9 by CARD_1:5;
P = {} implies B = {} by A7,ZFMISC_1:2;
then
A11: dom g = B by FUNCT_2:def 1;
B is independent by A3;
then g is one-to-one by A6,Th10;
then B, B9 are_equipotent by A11,WELLORD2:def 4;
then card B = card B9 by CARD_1:5;
then consider a being set such that
A12: a in B9 \ A9 by A10,A5,Th5;
consider x9 being object such that
A13: x9 in B and
A14: a = g.x9 by A11,A12,FUNCT_1:def 3;
reconsider x = x9 as Element of M by A13;
take x;
A15: a nin A9 by A12,XBOOLE_0:def 5;
now
A16: x in g.x by A6,A13;
assume
A17: x in A;
then x in f.x by A4;
then
A18: f.x meets g.x by A16,XBOOLE_0:3;
A19: g.x in rng g by A11,A13,FUNCT_1:def 3;
f.x in rng f by A8,A17,FUNCT_1:def 3;
hence contradiction by A15,A14,A19,A18,TAXONOM2:def 5;
end;
hence x in B \ A by A13,XBOOLE_0:def 5;
reconsider xx = {x} as Subset of M by A13,ZFMISC_1:31;
reconsider Ax = A \/ xx as Subset of union P by Def7;
A20: a in B9 by A12;
now
let D be set;
A21: Ax /\ D = A /\ D \/ xx /\ D by XBOOLE_1:23;
assume
A22: D in P;
then consider d being Element of D such that
A23: A /\ D c= {d} by A9,Th8;
per cases;
suppose
A24: D = a;
reconsider x9 as set by TARSKI:1;
take x9;
A /\ D c= {}
proof
let z be object;
assume
A25: z in A /\ D;
then
A26: z in D by XBOOLE_0:def 4;
A27: z in A by A25,XBOOLE_0:def 4;
then z in f.z by A4;
then
A28: D meets f.z by A26,XBOOLE_0:3;
f.z in rng f by A8,A27,FUNCT_1:def 3;
hence thesis by A20,A15,A24,A28,TAXONOM2:def 5;
end;
then A /\ D = {};
hence Ax /\ D c= {x9} by A21,XBOOLE_1:17;
end;
suppose
A29: D <> a;
a in rng g by A11,A13,A14,FUNCT_1:def 3;
then
A30: a misses D by A22,A29,TAXONOM2:def 5;
x in a by A6,A13,A14;
then x nin D by A30,XBOOLE_0:3;
then xx c/= D by ZFMISC_1:31;
then
A31: xx /\ D <> xx by XBOOLE_1:17;
reconsider d as set;
take d;
xx /\ D c= xx by XBOOLE_1:17;
then xx /\ D = {} by A31,ZFMISC_1:33;
hence Ax /\ D c= {d} by A23,A21;
end;
end;
hence thesis by A1;
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 Def7;
end;
end;
registration
let X be set;
cluster -> mutually-disjoint for a_partition of X;
coherence
proof
let P be a_partition of X;
let x,y be set;
thus thesis by EQREL_1:def 4;
end;
end;
registration
cluster finite strict for Matroid;
existence
proof
set X = the finite non empty set,P = the a_partition of X;
take ProdMatroid P;
thus thesis;
end;
end;
registration
let M be finite-membered non void SubsetFamilyStr;
cluster -> finite for independent Subset of M;
coherence
proof
let A be independent Subset of M;
A1: the_family_of M is finite-membered by Def5;
A in the_family_of M by Def2;
hence thesis by A1;
end;
end;
definition
let F be Field;
let V be VectSp of F;
func LinearlyIndependentSubsets V -> strict SubsetFamilyStr means
: Def8:
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 F = {A where A is Subset of V: A is linearly-independent};
set X = the carrier of V;
F c= bool X
proof
let x be object;
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 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;
A1: the_family_of M = {A where A is Subset of V: A is linearly-independent
} by Def8;
the carrier of M = the carrier of V by Def8;
hence the carrier of M is non empty;
{} V is linearly-independent;
then {} in the_family_of M by A1;
hence the topology of M is non empty;
let x,y be set;
assume x in the_family_of M;
then
A2: ex A being Subset of V st x = A & A is linearly-independent by A1;
assume
A3: y c= x;
then reconsider B = y as Subset of V by A2,XBOOLE_1:1;
B is linearly-independent by A2,A3,VECTSP_7:1;
hence thesis by A1;
end;
end;
theorem Th11:
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 Def8;
then B in the_family_of M iff ex A being Subset of V st B = A & A is
linearly-independent;
hence thesis;
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:18;
end;
theorem Th13:
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
A1: A is linearly-independent;
A2: the set of all Sum s where s is Linear_Combination of A = the
carrier of Lin A by VECTSP_7:def 2;
let a be Element of V;
set B = A\/{a};
assume that
A3: a nin the carrier of Lin A and
A4: B is linearly-dependent;
consider l being Linear_Combination of B such that
A5: Sum l = 0.V and
A6: Carrier l <> {} by A4,VECTSP_7:def 1;
a in {a} by TARSKI:def 1;
then
A7: (l!{a}).a = l.a by RANKNULL:25;
A c= the carrier of Lin A
proof
let x be object;
assume
A8: x in A;
then reconsider x as Element of V;
x in Lin A by A8,VECTSP_7:8;
hence thesis;
end;
then a nin A by A3;
then B\A={a} by XBOOLE_1:88,ZFMISC_1:50;
then l = (l!A)+(l!{a}) by RANKNULL:27,XBOOLE_1:7;
then 0.V = Sum (l!A) + Sum (l!{a}) by A5,VECTSP_6:44
.= Sum (l!A) + (l.a)*a by A7,VECTSP_6:17;
then
A9: (l.a)*a = - Sum (l!A) by ALGSTR_0:def 13;
A10: (-(l.a)")*(l!A) is Linear_Combination of A by VECTSP_6:31;
now
assume l.a <> 0.F;
then a = ((l.a)")*(-Sum(l!A)) by A9,VECTSP_1:20
.= -((l.a)" * Sum(l!A)) by VECTSP_1:22
.= (-(l.a)")*(Sum(l!A)) by VECTSP_1:21
.= Sum((-(l.a)")*(l!A)) by VECTSP_6:45;
hence contradiction by A3,A2,A10;
end;
then
A11: a nin Carrier l by VECTSP_6:2;
A12: Carrier l c= B by VECTSP_6:def 4;
Carrier l c= A
by A11,A12,ZFMISC_1:136;
then l is Linear_Combination of A by VECTSP_6:def 4;
hence contradiction by A1,A5,A6,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;
A1: the_family_of M = {A where A is Subset of V: A is linearly-independent
} by Def8;
let A,B be finite Subset of M such that
A2: A in the_family_of M and
A3: B in the_family_of M and
A4: card B = (card A) + 1;
A5: B is independent by A3;
A is independent by A2;
then reconsider
A9 = A, B9 = B as linearly-independent finite Subset of V by A5,Th11;
set V9 = Lin (A9 \/ B9);
A9 c= the carrier of V9
proof
let a be object;
assume a in A9;
then a in A9 \/ B9 by XBOOLE_0:def 3;
then a in V9 by VECTSP_7:8;
hence thesis;
end;
then reconsider A99 = A9 as linearly-independent finite Subset of V9 by
VECTSP_9:12;
B9 c= the carrier of V9
proof
let a be object;
assume a in B9;
then a in A9 \/ B9 by XBOOLE_0:def 3;
then a in V9 by VECTSP_7:8;
hence thesis;
end;
then reconsider B99 = B9 as linearly-independent finite Subset of V9 by
VECTSP_9:12;
A6: V9 = Lin(A99\/ B99) by VECTSP_9:17;
then consider D being Basis of V9 such that
A7: B9 c= D by VECTSP_7:19;
consider C being Basis of V9 such that
A8: C c= A99 \/ B99 by A6,VECTSP_7:20;
reconsider c = C as finite set by A8;
c is Basis of V9;
then V9 is finite-dimensional by MATRLIN:def 1;
then card c = card D by VECTSP_9:22;
then Segm card B c= Segm card c by A7,CARD_1:11;
then card B <= card c by NAT_1:39;
then
A9: card A < card c by A4,NAT_1:13;
set e = the Element of C \ the carrier of Lin A9;
A10: A9 is Basis of Lin A9 by RANKNULL:20;
then
A11: Lin A9 is finite-dimensional by MATRLIN:def 1;
now
assume C c= the carrier of Lin A9;
then reconsider C9 = C as Subset of Lin A9;
the carrier of Lin A9 c= the carrier of V by VECTSP_4:def 2;
then reconsider C99 = C9 as Subset of V by XBOOLE_1:1;
C is linearly-independent by VECTSP_7:def 3;
then C99 is linearly-independent by VECTSP_9:11;
then consider E being Basis of Lin A9 such that
A12: C9 c= E by VECTSP_7:19,VECTSP_9:12;
A13: card A = card E by A10,A11,VECTSP_9:22;
then E is finite;
hence contradiction by A9,A12,A13,NAT_1:43;
end;
then consider x being object such that
A14: x in C and
A15: x nin the carrier of Lin A9;
A16: x in C \ the carrier of Lin A9 by A14,A15,XBOOLE_0:def 5;
then
A17: e nin the carrier of Lin A9 by XBOOLE_0:def 5;
A18: e in C by A16,XBOOLE_0:def 5;
then e in A\/B by A8;
then reconsider e as Element of M;
take e;
A c= the carrier of Lin A9
proof
let x be object;
assume x in A;
then x in Lin A9 by VECTSP_7:8;
hence thesis;
end;
then
A19: e nin A by A16,XBOOLE_0:def 5;
then
A20: e in B9 by A8,A18,XBOOLE_0:def 3;
hence e in B \ A by A19,XBOOLE_0:def 5;
reconsider a = e as Element of V by A20;
A9\/{a} is linearly-independent by A17,Th13;
hence A \/ {e} in the_family_of M by A1;
end;
end;
registration
let F be Field;
let V be finite-dimensional VectSp of F;
cluster LinearlyIndependentSubsets V -> finite-membered;
coherence
proof
let A be set;
set M = LinearlyIndependentSubsets V;
assume A in the_family_of M;
then A is independent Subset of M by Def2;
then A is linearly-independent Subset of V by Th11;
hence thesis by VECTSP_9:21;
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
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 Th14:
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 that
A1: A0 c= C and
A2: A0 is independent;
reconsider AA = A0 as independent Subset of M by A2;
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
A3: for A being finite Subset of M st A is independent holds card A <= n
by Def6;
reconsider n as Element of NAT by ORDINAL1:def 12;
P[n] by A3;
then
A4: ex n being Nat st P[n];
consider n0 being Nat such that
A5: P[n0] & for m being Nat st P[m] holds n0 <= m from NAT_1:sch 5(A4);
now
0 <= card AA by NAT_1:2;
then
A6: (card AA)+1 >= 0+1 by XREAL_1:6;
assume
A7: for A being independent Subset of M st A0 c= A & A c= C holds card A < n0;
then card AA < n0 by A1;
then (card AA)+1 <= n0 by NAT_1:13;
then consider n being Nat such that
A8: n0 = 1+n by A6,NAT_1:10,XXREAL_0:2;
reconsider n as Element of NAT by ORDINAL1:def 12;
P[n]
proof
let A be finite Subset of M;
assume that
A9: A0 c= A and
A10: A c= C and
A11: A is independent;
card A < n+1 by A7,A8,A9,A10,A11;
hence thesis by NAT_1:13;
end;
then n+1 <= n by A5,A8;
hence contradiction by NAT_1:13;
end;
then consider A being independent Subset of M such that
A12: A0 c= A and
A13: A c= C and
A14: card A >= n0;
A15: card A <= n0 by A5,A12,A13;
take A;
thus A0 c= A & A is independent & A c= C by A12,A13;
let B be Subset of M;
assume that
A16: B is independent and
A17: B c= C and
A18: A c= B;
reconsider B9 = B as independent Subset of M by A16;
card A <= card B9 by A18,NAT_1:43;
then
A19: n0 <= card B9 by A14,XXREAL_0:2;
A0 c= B by A12,A18;
then card B9 <= n0 by A5,A17;
then card B9 = n0 by A19,XXREAL_0:1;
hence thesis by A14,A18,A15,CARD_2:102,XXREAL_0: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;
{} M c= C;
then ex A being independent Subset of M st {} M c= A & A
is_maximal_independent_in C by Th14;
hence thesis;
end;
theorem Th16:
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
A1: M is Matroid;
let C be Subset of M;
A2: now
let A,B be independent Subset of M such that
A3: A is_maximal_independent_in C and
A4: B is_maximal_independent_in C and
A5: card A < card B;
A6: A c= C by A3;
(card A)+1 <= card B by A5,NAT_1:13;
then Segm((card A)+1) c= Segm card B by NAT_1:39;
then consider D being set such that
A7: D c= B and
A8: card D = (card A)+1 by CARD_FIL:36;
reconsider D as finite Subset of M by A7,XBOOLE_1:1;
D is independent by A7,Th3;
then consider e being Element of M such that
A9: e in D \ A and
A10: A \/ {e} is independent by A1,A8,Th4;
D \ A c= D by XBOOLE_1:36;
then
A11: D \ A c= B by A7;
B c= C by A4;
then D \ A c= C by A11;
then {e} c= C by A9,ZFMISC_1:31;
then
A12: A \/ {e} c= C by A6,XBOOLE_1:8;
A c= A \/ {e} by XBOOLE_1:7;
then A \/ {e} = A by A3,A10,A12;
then {e} c= A by XBOOLE_1:7;
then e in A by ZFMISC_1:31;
hence contradiction by A9,XBOOLE_0:def 5;
end;
let A,B be independent Subset of M such that
A13: A is_maximal_independent_in C and
A14: 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 A2,A13,A14;
end;
assume
A15: 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 that
A16: A in the_family_of M and
A17: B in the_family_of M and
A18: card B = (card A)+1;
B is independent by A17;
then consider B9 being independent Subset of M such that
A19: B c= B9 and
A20: B9 is_maximal_independent_in C by Th14,XBOOLE_1:7;
A21: card B <= card B9 by A19,NAT_1:43;
assume
A22: 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 A16,Def2;
A is_maximal_independent_in C
proof
thus A in the_family_of M by A16;
thus A c= C by XBOOLE_1:7;
let D be Subset of M;
assume that
A23: D is independent and
A24: D c= C and
A25: A c= D;
assume not (A c= D & D c= A);
then consider e being object such that
A26: e in D and
A27: not e in A by A25;
reconsider e as Element of M by A26;
e in B by A24,A26,A27,XBOOLE_0:def 3;
then e in B \ A by A27,XBOOLE_0:def 5;
then not A \/ {e} in the_family_of M by A22;
then
A28: A \/ {e} is not independent;
{e} c= D by A26,ZFMISC_1:31;
then A \/ {e} c= D by A25,XBOOLE_1:8;
hence contradiction by A23,A28,Th3;
end;
then card A = card B9 by A15,A20;
hence contradiction by A18,A21,NAT_1:13;
end;
hence thesis;
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
set X = {card A where A is independent Subset of M: A c= C};
defpred Q[Nat] means ex A being independent Subset of M st A c= C & $1 =
card A;
defpred P[Nat] means for A being independent Subset of M st A c= C 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 Def6;
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);
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 and
A5: A c= C;
card A <= n0 by A3,A5;
then Segm card A c= Segm n0 by NAT_1:39;
hence a c= Segm n0 by A4;
end;
hence union X c= n0 by ZFMISC_1:76;
A6: {} M c= C;
A7: for k being Nat st Q[k] holds k <= n0 by A3;
card {} = card {};
then
A8: ex n being Nat st Q[n] by A6;
consider n being Nat such that
A9: Q[n] & for m being Nat st Q[m] holds m <= n from NAT_1:sch 6(
A7,A8 );
P[n] by A9;
then
A10: n0 <= n by A3;
n <= n0 by A3,A9;
then n = n0 by A10,XXREAL_0:1;
then n0 in X by A9;
hence thesis by ZFMISC_1:74;
end;
hence thesis;
end;
end;
theorem Th17:
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 Segm card A c= Segm Rnk C by ZFMISC_1:74;
hence thesis by NAT_1:39;
end;
theorem Th18:
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;
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;
set X = {card A where A is independent Subset of M: A c= C};
A1: {} M c= C;
card {} = card {};
then
A2: ex n being Nat st Q[n] by A1;
consider n being Nat such that
A3: for A being finite Subset of M st A is independent holds card A <= n
by Def6;
A4: ex ne being Nat st P[ne]
proof
take n;
thus thesis by A3;
end;
consider n0 being Nat such that
A5: P[n0] & for m being Nat st P[m] holds n0 <= m from NAT_1:sch 5(A4);
now
let a be set;
assume a in X;
then consider A being independent Subset of M such that
A6: a = card A and
A7: A c= C;
card A <= n0 by A5,A7;
then Segm card A c= Segm n0 by NAT_1:39;
hence a c= Segm n0 by A6;
end;
then
A8: Rnk C c= n0 by ZFMISC_1:76;
A9: for k being Nat st Q[k] holds k <= n0 by A5;
consider n being Nat such that
A10: Q[n] & for m being Nat st Q[m] holds m <= n from NAT_1:sch 6(A9,
A2);
P[n] by A10;
then
A11: n0 <= n by A5;
consider A being independent Subset of M such that
A12: A c= C and
A13: n = card A by A10;
take A;
n <= n0 by A5,A10;
then
A14: n = n0 by A11,XXREAL_0:1;
then n0 in X by A12,A13;
then n0 c= Rnk C by ZFMISC_1:74;
hence thesis by A8,A12,A13,A14;
end;
theorem Th19:
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};
let A be independent Subset of M;
consider B being independent Subset of M such that
A1: B c= C and
A2: card B = Rnk C by Th18;
A3: now
let A be independent Subset of M;
assume that
A4: A c= C and
A5: card A = Rnk C;
thus A is_maximal_independent_in C
proof
thus A is independent & A c= C by A4;
let B be Subset of M;
assume B is independent;
then reconsider B9 = B as independent Subset of M;
assume B c= C;
then card B9 in X;
then
A6: card B9 c= Rnk C by ZFMISC_1:74;
assume
A7: A c= B;
then card A c= card B9 by CARD_1:11;
then card A = card B9 by A5,A6;
hence thesis by A7,CARD_2:102;
end;
end;
hereby
assume
A8: A is_maximal_independent_in C;
hence A c= C;
B is_maximal_independent_in C by A3,A1,A2;
hence card A = Rnk C by A2,A8,Th16;
end;
thus thesis by A3;
end;
theorem Th20:
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 Th18;
then Segm Rnk C c= Segm card C by CARD_1:11;
hence thesis by NAT_1:39;
end;
theorem Th21:
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 Segm card C c= Segm Rnk C by ZFMISC_1:74;
then
A1: card C <= Rnk C by NAT_1:39;
Rnk C <= card C by Th20;
hence card C = Rnk C by A1,XXREAL_0:1;
end;
ex A being independent Subset of M st A c= C & card A = Rnk C by Th18;
hence thesis by CARD_2:102;
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
: Def12:
it is_maximal_independent_in [#]M;
existence
proof
set A = the independent Subset of M;
set C = [#]M;
consider B being independent Subset of M such that
A c= B and
A1: B is_maximal_independent_in C by Th14;
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;
A1: B2 is_maximal_independent_in [#]M by Def12;
B1 is_maximal_independent_in [#]M by Def12;
hence thesis by A1,Th16;
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 and
A2: B is_maximal_independent_in [#]M by Th14;
reconsider B as Basis of M by A2,Def12;
take B;
thus thesis by A1;
end;
reserve M for finite-degree Matroid,
A,B,C for Subset of M,
e,f for Element of M;
theorem Th24:
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 Th18;
hence thesis by Th17,XBOOLE_1:1;
end;
theorem Th25:
Rnk (A\/B) + Rnk (A/\B) <= Rnk A + Rnk B
proof
consider C being independent Subset of M such that
A1: C c= A/\B and
A2: card C = Rnk (A/\B) by Th18;
A/\B c= A by XBOOLE_1:17;
then C c= A by A1;
then consider Ca being independent Subset of M such that
A3: C c= Ca and
A4: Ca is_maximal_independent_in A by Th14;
A5: Ca c= A by A4;
A6: Ca/\B c= C
proof
let x be object;
assume
A7: x in Ca/\B;
then
A8: x in Ca by XBOOLE_0:def 4;
then {x} c= Ca by ZFMISC_1:31;
then C\/{x} c= Ca by A3,XBOOLE_1:8;
then reconsider Cx = C\/{x} as independent Subset of M by Th3,XBOOLE_1:1;
x in B by A7,XBOOLE_0:def 4;
then x in A/\B by A5,A8,XBOOLE_0:def 4;
then {x} c= A/\B by ZFMISC_1:31;
then
A9: Cx c= A/\B by A1,XBOOLE_1:8;
A10: C c= Cx by XBOOLE_1:7;
C is_maximal_independent_in A/\B by A1,A2,Th19;
then C = Cx by A9,A10;
then {x} c= C by XBOOLE_1:7;
hence thesis by ZFMISC_1:31;
end;
A/\B c= B by XBOOLE_1:17;
then C c= B by A1;
then C c= Ca /\B by A3,XBOOLE_1:19;
then
A11: Ca/\B = C by A6;
A c= A\/B by XBOOLE_1:7;
then Ca c= A\/B by A5;
then consider C9 being independent Subset of M such that
A12: Ca c= C9 and
A13: C9 is_maximal_independent_in A\/B by Th14;
A14: Ca/\(C9/\B) = Ca/\C9/\B by XBOOLE_1:16
.= Ca/\B by A12,XBOOLE_1:28;
A15: C9 c= A\/B by A13;
A16: C9 = Ca \/ (C9/\B)
proof
thus C9 c= Ca \/ (C9/\B)
proof
let x be object;
assume
A17: x in C9;
then {x} c= C9 by ZFMISC_1:31;
then Ca\/{x} c= C9 by A12,XBOOLE_1:8;
then reconsider Cax = Ca\/{x} as independent Subset of M by Th3,
XBOOLE_1:1;
A18: now
assume x in A;
then {x} c= A by ZFMISC_1:31;
then
A19: Cax c= A by A5,XBOOLE_1:8;
Ca c= Cax by XBOOLE_1:7;
then Ca = Cax by A4,A19;
then {x} c= Ca by XBOOLE_1:7;
hence x in Ca by ZFMISC_1:31;
end;
x in B implies x in C9/\B by A17,XBOOLE_0:def 4;
hence thesis by A15,A17,A18,XBOOLE_0:def 3;
end;
let x be object;
assume x in Ca \/ (C9/\B);
then x in Ca or x in C9/\B by XBOOLE_0:def 3;
hence thesis by A12,XBOOLE_0:def 4;
end;
C9/\B c= B by XBOOLE_1:17;
then consider Cb being independent Subset of M such that
A20: C9/\B c= Cb and
A21: Cb is_maximal_independent_in B by Th14;
card Cb = Rnk B by A21,Th19;
then
A22: card (C9/\B) <= Rnk B by A20,NAT_1:43;
A23: card C9 = Rnk (A\/B) by A13,Th19;
card Ca = Rnk A by A4,Th19;
then Rnk (A\/B) = Rnk A + card (C9/\B) - Rnk (A/\B) by A2,A23,A16,A14,A11,
CARD_2:45;
hence thesis by A22,XREAL_1:6;
end;
theorem Th26:
Rnk A <= Rnk (A\/B) & Rnk (A \/ {e}) <= Rnk A + 1
proof
A1: card {e} = 1 by CARD_1:30;
thus Rnk A <= Rnk (A\/B) by Th24,XBOOLE_1:7;
A2: Rnk(A\/{e}) + Rnk(A/\{e}) <= Rnk A + Rnk {e} by Th25;
Rnk {e} <= card {e} by Th20;
then Rnk A + Rnk {e} <= Rnk A + 1 by A1,XREAL_1:6;
then
A3: Rnk(A\/{e}) + Rnk(A/\{e}) <= Rnk A + 1 by A2,XXREAL_0:2;
Rnk(A\/{e}) <= Rnk(A\/{e}) + Rnk(A/\{e}) by NAT_1:11;
hence thesis by A3,XXREAL_0:2;
end;
theorem
Rnk (A\/{e}) = Rnk (A\/{f}) & Rnk (A\/{f}) = Rnk A implies Rnk (A \/ {
e,f}) = Rnk A
proof
assume that
A1: Rnk (A\/{e}) = Rnk (A\/{f}) and
A2: Rnk (A\/{f}) = Rnk A;
consider C being independent Subset of M such that
A3: C c= A and
A4: card C = Rnk A by Th18;
A5: C is_maximal_independent_in A by A3,A4,Th19;
A c= A\/{f} by XBOOLE_1:7;
then C c= A\/{f} by A3;
then
A6: C is_maximal_independent_in A\/{f} by A4,A2,Th19;
A c= A\/{e} by XBOOLE_1:7;
then C c= A\/{e} by A3;
then
A7: C is_maximal_independent_in A\/{e} by A4,A1,A2,Th19;
A c= A\/{e,f} by XBOOLE_1:7;
then C c= A\/{e,f} by A3;
then consider C9 being independent Subset of M such that
A8: C c= C9 and
A9: C9 is_maximal_independent_in A\/{e,f} by Th14;
A10: C9 c= A\/{e,f} by A9;
now
assume C9 <> C;
then consider x being object such that
A11: not (x in C9 iff x in C) by TARSKI:2;
{x} c= C9 by A8,A11,ZFMISC_1:31;
then C\/{x} c= C9 by A8,XBOOLE_1:8;
then reconsider Cx = C\/{x} as independent Subset of M by Th3,XBOOLE_1:1;
now
assume x in A;
then {x} c= A by ZFMISC_1:31;
then
A12: Cx c= A by A3,XBOOLE_1:8;
C c= Cx by XBOOLE_1:7;
then C = Cx by A5,A12;
then {x} c= C by XBOOLE_1:7;
hence contradiction by A8,A11,ZFMISC_1:31;
end;
then x in {e,f} by A8,A10,A11,XBOOLE_0:def 3;
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 A3,
XBOOLE_1:10;
then
A13: Cx c= A\/{e} or Cx c= A\/{f} by XBOOLE_1:8;
C c= Cx by XBOOLE_1:7;
then C = Cx by A7,A6,A13;
then {x} c= C by XBOOLE_1:7;
hence contradiction by A8,A11,ZFMISC_1:31;
end;
hence thesis by A4,A9,Th19;
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
Rnk (A \/ {e}) = Rnk A;
end;
theorem Th28:
e in A implies e is_dependent_on A
by ZFMISC_1:31,XBOOLE_1:12;
theorem Th29:
A c= B & e is_dependent_on A implies e is_dependent_on B
proof
assume that
A1: A c= B and
A2: Rnk (A \/ {e}) = Rnk A;
consider Ca being independent Subset of M such that
A3: Ca c= A and
A4: card Ca = Rnk A by Th18;
A5: Ca c= B by A1,A3;
B c= B\/{e} by XBOOLE_1:7;
then Ca c= B\/{e} by A5;
then consider E being independent Subset of M such that
A6: Ca c= E and
A7: E is_maximal_independent_in B\/{e} by Th14;
A8: now
E c= B\/{e} by A7;
then
A9: E = E/\(B\/{e}) by XBOOLE_1:28
.= E/\B\/E/\{e} by XBOOLE_1:23;
E/\{e} c= {e} by XBOOLE_1:17;
then
A10: E/\{e} = {} & card {} = 0 or E/\{e} = {e} & card {e} = 1 by CARD_1:30
,ZFMISC_1:33;
card (E/\B) <= Rnk B by Th17,XBOOLE_1:17;
then
A11: card (E/\B)+1 <= Rnk B + 1 by XREAL_1:6;
Ca c= A\/{e} by A3,XBOOLE_1:10;
then
A12: Ca is_maximal_independent_in A\/{e} by A2,A4,Th19;
A13: Ca c= Ca\/{e} by XBOOLE_1:10;
assume
A14: Rnk (B\/{e}) = Rnk B + 1;
then card E = Rnk B + 1 by A7,Th19;
then Rnk B + 1 <= card (E/\B) + card (E/\{e}) by A9,CARD_2:43;
then card (E/\B)+1 <= card (E/\B) + card (E/\{e}) by A11,XXREAL_0:2;
then e in E/\{e} by A10,TARSKI:def 1,XREAL_1:6;
then e in E by XBOOLE_0:def 4;
then {e} c= E by ZFMISC_1:31;
then Ca\/{e} c= E by A6,XBOOLE_1:8;
then
A15: Ca\/{e} is independent by Th3;
Ca\/{e} c= A\/{e} by A3,XBOOLE_1:9;
then Ca = Ca\/{e} by A13,A15,A12;
then {e} c= Ca by XBOOLE_1:7;
then B = B\/{e} by A5,XBOOLE_1:1,12;
hence contradiction by A14;
end;
A16: Rnk (B\/{e}) <= Rnk B + 1 by Th26;
Rnk B <= Rnk (B\/{e}) by Th26;
hence Rnk (B\/{e}) = Rnk B by A16,A8,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 object;
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 Th30:
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;
end;
assume Rnk (A \/ {e}) = Rnk A;
then e is_dependent_on A;
hence thesis;
end;
theorem Th31:
A c= Span A
proof
let e be object;
assume
A1: e in A;
then reconsider x = e as Element of M;
x is_dependent_on A by A1,Th28;
hence thesis;
end;
theorem
A c= B implies Span A c= Span B
proof
assume
A1: A c= B;
let x be object;
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 A1,Th29;
hence thesis;
end;
theorem Th33:
Rnk Span A = Rnk A
proof
consider Ca being independent Subset of M such that
A1: Ca c= A and
A2: card Ca = Rnk A by Th18;
A c= Span A by Th31;
then Ca c= Span A by A1;
then consider C being independent Subset of M such that
A3: Ca c= C and
A4: C is_maximal_independent_in Span A by Th14;
now
assume C c/= Ca;
then consider x being object such that
A5: x in C and
A6: x nin Ca;
C c= Span A by A4;
then x in Span A by A5;
then consider e being Element of M such that
A7: x = e and
A8: e is_dependent_on A;
{e} c= C by A5,A7,ZFMISC_1:31;
then Ca\/{e} c= C by A3,XBOOLE_1:8;
then reconsider Ce = Ca\/{e} as independent Subset of M by Th3;
Ce c= A\/{e} by A1,XBOOLE_1:9;
then consider D being independent Subset of M such that
A9: Ce c= D and
A10: D is_maximal_independent_in A\/{e} by Th14;
card Ca = Rnk (A\/{e}) by A2,A8
.= card D by A10,Th19;
then
A11: card Ce <= card Ca by A9,NAT_1:43;
card Ca <= card Ce by NAT_1:43,XBOOLE_1:7;
then card Ca = card Ce by A11,XXREAL_0:1;
then Ca = Ce by CARD_2:102,XBOOLE_1:7;
then e nin {e} by A6,A7,XBOOLE_0:def 3;
hence contradiction by TARSKI:def 1;
end;
then C = Ca by A3;
hence thesis by A2,A4,Th19;
end;
theorem Th34:
e is_dependent_on Span A implies e is_dependent_on A
proof
assume
A1: Rnk ((Span A)\/{e}) = Rnk Span A;
A2: Rnk A = Rnk Span A by Th33;
consider Ca being independent Subset of M such that
A3: Ca c= A and
A4: card Ca = Rnk A by Th18;
A5: Rnk A = Rnk Ca by A4,Th21;
A6: Rnk Ca <= Rnk(A\/{e}) by A3,Th24,XBOOLE_1:10;
A c= Span A by Th31;
then Rnk(A\/{e}) <= Rnk A by A1,A2,Th24,XBOOLE_1:9;
hence Rnk (A\/{e}) = Rnk A by A5,A6,XXREAL_0:1;
end;
theorem
Span Span A = Span A
proof
thus Span Span A c= Span A
proof
let x be object;
assume x in Span Span A;
then consider e being Element of M such that
A1: x = e and
A2: e is_dependent_on Span A;
e is_dependent_on A by A2,Th34;
hence thesis by A1;
end;
thus thesis by Th31;
end;
theorem
f nin Span A & f in Span (A \/ {e}) implies e in Span (A \/ {f})
proof
assume that
A1: f nin Span A and
A2: f in Span (A \/ {e});
A3: Rnk A <= Rnk (A\/{f}) by Th26;
A4: Rnk (A\/{f}) <= Rnk A + 1 by Th26;
Rnk A <> Rnk (A\/{f}) by A1,Th30;
then
A5: Rnk (A\/{f}) = Rnk A + 1 by A3,A4,NAT_1:9;
A6: A\/{f}\/{e} = A\/({f}\/{e}) by XBOOLE_1:4;
A7: Rnk (A\/{e}) <= Rnk A + 1 by Th26;
A8: A\/{e}\/{f} = A\/({e}\/{f}) by XBOOLE_1:4;
A9: Rnk(A\/{e}\/{f}) = Rnk(A\/{e}) by A2,Th30;
then Rnk(A\/{f}) <= Rnk(A\/{e}) by A6,A8,Th26;
then Rnk (A\/{f}) = Rnk (A\/{f}\/{e}) by A9,A5,A6,A8,A7,XXREAL_0:1;
hence thesis by Th30;
end;
definition
let M be SubsetFamilyStr;
let A be Subset of M;
attr A is cycle means
A is dependent & for e being Element of M st e
in A holds A \ {e} is independent;
end;
theorem Th37:
A is cycle implies A is non empty finite
proof
assume that
A1: A is dependent and
A2: for e being Element of M st e in A holds A \ {e} is independent;
thus A is non empty by A1;
set e = the Element of A;
now
assume
A3: A is non empty set;
then e in A;
then reconsider e as Element of M;
reconsider Ae = A\{e} as independent Subset of M by A2,A3;
A = Ae\/{e} by A3,ZFMISC_1:116;
hence thesis;
end;
hence thesis;
end;
registration
let M;
cluster cycle -> non empty finite for Subset of M;
coherence by Th37;
end;
theorem Th38:
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
A1: A is dependent and
A2: for e being Element of M st e in A holds A \ {e} is independent;
thus A is non empty by A1;
let e;
set Ae = A\{e};
assume
A3: e in A;
hence Ae is independent & Ae c= A by A2,XBOOLE_1:36;
let B;
assume that
A4: B is independent and
A5: B c= A and
A6: Ae c= B;
A = Ae\/{e} by A3,ZFMISC_1:116;
hence thesis by A1,A4,A5,A6,ZFMISC_1:138;
end;
set a = the Element of A;
assume that
A7: A is non empty and
A8: for e st e in A holds A\{e} is_maximal_independent_in A;
a in A by A7;
then reconsider a as Element of M;
set Ae = A\{a};
A9: Ae is_maximal_independent_in A by A7,A8;
hereby
assume A is independent;
then A = Ae by A9;
then a nin {a} by A7,XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
let e;
assume e in A;
then A\{e} is_maximal_independent_in A by A8;
hence thesis;
end;
theorem Th39:
A is cycle implies Rnk A + 1 = card A
proof
assume
A1: A is cycle;
then reconsider A as non empty finite Subset of M;
set a = the Element of A;
A2: A\{a} is_maximal_independent_in A by A1,Th38;
A3: Rnk A = card (A\{a}) by A2,Th19;
a in {a} by TARSKI:def 1;
then
A4: a nin A\{a} by XBOOLE_0:def 5;
A = (A\{a})\/{a} by ZFMISC_1:116;
hence thesis by A3,A4,CARD_2:41;
end;
theorem
A is cycle & e in A implies e is_dependent_on A\{e}
proof
assume that
A1: A is cycle and
A2: e in A;
reconsider Ae = A\{e} as independent Subset of M by A1,A2;
Ae is_maximal_independent_in A by A1,A2,Th38;
then Rnk A = card Ae by Th19;
hence Rnk((A\{e})\/{e}) = card Ae by A2,ZFMISC_1:116
.= Rnk (A\{e}) by Th21;
end;
theorem Th41:
A is cycle & B is cycle & A c= B implies A = B
proof
assume that
A1: A is dependent and
for e st e in A holds A \ {e} is independent and
B is dependent and
A2: for e st e in B holds B \ {e} is independent;
assume that
A3: A c= B and
A4: A <> B;
consider x being object such that
A5: not (x in A iff x in B) by A4,TARSKI:2;
reconsider x as Element of M by A5;
A6: A c= B\{x} by A3,A5,ZFMISC_1:34;
B\{x} is independent by A2,A3,A5;
hence contradiction by A1,A6,Th3;
end;
theorem Th42:
(for B st B c= A holds B is not cycle) implies A is independent
proof
assume
A1: for B st B c= A holds B is not cycle;
consider C being independent Subset of M such that
A2: C c= A and
A3: card C = Rnk A by Th18;
per cases;
suppose
A c= C;
hence thesis by A2,XBOOLE_0:def 10;
end;
suppose
A c/= C;
then consider x being object such that
A4: x in A and
A5: x nin C;
reconsider x as Element of M by A4;
A6: C c= C\/{x} by ZFMISC_1:137;
defpred P[Nat] means ex B being independent Subset of M st card B = $1 & B
c= C & B\/{x} is dependent;
A7: C\/{x} c= A by A2,A4,ZFMISC_1:137;
A8: ex n being Nat st P[n]
proof
take n = Rnk A, C;
thus card C = n & C c= C by A3;
assume
A9: C\/{x} is independent;
C is_maximal_independent_in A by A2,A3,Th19;
then C = C\/{x} by A7,A6,A9;
then {x} c= C by XBOOLE_1:7;
hence contradiction by A5,ZFMISC_1:31;
end;
consider n being Nat such that
A10: P[n] & for k being Nat st P[k] holds n <= k from NAT_1:sch 5(A8);
consider B being independent Subset of M such that
A11: card B = n and
A12: B c= C and
A13: B\/{x} is dependent by A10;
A14: x nin B by A5,A12;
A15: B\/{x} is cycle
proof
thus B\/{x} is dependent by A13;
let e be Element of M;
set Be = B\{e};
A16: Be c= B by XBOOLE_1:36;
assume
A17: e in B\/{x};
per cases by A17,ZFMISC_1:136;
suppose
A18: e in B;
A19: e nin Be by ZFMISC_1:56;
B = Be\/{e} by A18,ZFMISC_1:116;
then
A20: n = card Be+1 by A11,A19,CARD_2:41;
assume
A21: (B\/{x}) \ {e} is dependent;
(B\/{x}) \ {e} = Be\/{x} by A14,A18,XBOOLE_1:87,ZFMISC_1:11;
then n <= card Be by A10,A12,A16,A21,XBOOLE_1:1;
hence contradiction by A20,NAT_1:13;
end;
suppose
e = x;
hence (B\/{x}) \ {e} is independent by A14,ZFMISC_1:117;
end;
end;
B c= A by A2,A12;
then B\/{x} c= A by A4,ZFMISC_1:137;
hence thesis by A1,A15;
end;
end;
theorem Th43:
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
A1: A is cycle and
A2: B is cycle and
A3: A <> B and
A4: e in A /\ B and
A5: for C st C is cycle holds C c/= (A \/ B) \ {e};
A6: e in A by A4,XBOOLE_0:def 4;
A/\B c= B by XBOOLE_1:17;
then A c/= A/\B by A1,A2,A3,Th41,XBOOLE_1:1;
then consider a being object such that
A7: a in A and
A8: a nin A/\B;
reconsider a as Element of M by A7;
{a} misses A/\B by A8,ZFMISC_1:50;
then
A9: A/\B c= A\{a} by XBOOLE_1:17,86;
reconsider A9 = A, B9 = B as finite Subset of M by A1,A2;
Rnk(A\/B)+Rnk(A/\B) <= Rnk A + Rnk B by Th25;
then
A10: Rnk(A\/B)+Rnk(A/\B)+1 <= Rnk A + Rnk B+1 by XREAL_1:6;
A\{a} is independent by A1,A7;
then A/\B is independent by A9,Th3;
then
A11: card (A9/\B9) = Rnk (A/\B) by Th21;
for C st C c= (A \/ B) \ {e} holds C is not cycle by A5;
then reconsider C = (A\/B)\{e} as independent Subset of M by Th42;
A12: e in {e} by TARSKI:def 1;
then
A13: e nin C by XBOOLE_0:def 5;
A14: e in B by A4,XBOOLE_0:def 4;
then reconsider
Ae = A\{e}, Be = B\{e} as independent Subset of M by A1,A2,A6;
A15: e nin Be by A12,XBOOLE_0:def 5;
B = Be\/{e} by A14,ZFMISC_1:116;
then
A16: card B9 = card Be+1 by A15,CARD_2:41;
then
A17: Rnk B + 1 = card Be+1 by A2,Th39;
A18: e nin Ae by A12,XBOOLE_0:def 5;
A = Ae\/{e} by A6,ZFMISC_1:116;
then
A19: card A9 = card Ae+1 by A18,CARD_2:41;
then Rnk A + 1 = card Ae+1 by A1,Th39;
then card(A9\/B9)+card(A9/\B9) = Rnk A+1 + (Rnk B+1) by A19,A16,A17,
HALLMAR1:1
.= Rnk A + Rnk B+1+1;
then
A20: Rnk(A\/B)+Rnk(A/\B)+1+1 <= card(A9\/B9)+card(A9/\B9) by A10,XREAL_1:6;
e in A\/B by A6,XBOOLE_0:def 3;
then
A21: C\/{e} = A9\/B9 by ZFMISC_1:116;
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;
A22: A c= A\/B by XBOOLE_1:7;
A is dependent by A1;
then A\/B is dependent by A22,Th3;
hence thesis by A21,ZFMISC_1:138;
end;
then Rnk(A\/B)+1 = card C+1 by Th19
.= card(A9\/B9) by A13,A21,CARD_2:41;
hence contradiction by A20,A11,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
A1: A is independent and
A2: B is cycle and
A3: C is cycle and
A4: B c= A\/{e} and
A5: C c= A\/{e};
not C c= A by A1,Th3,A3;
then consider c being object such that
A6: c in C and
A7: c nin A;
c in {e} by A5,A6,A7,XBOOLE_0:def 3;
then
A8: c = e by TARSKI:def 1;
not B c= A by A1,Th3,A2;
then consider b being object such that
A9: b in B and
A10: b nin A;
assume
A11: B <> C;
b in {e} by A4,A9,A10,XBOOLE_0:def 3;
then b = e by TARSKI:def 1;
then e in B/\C by A9,A6,A8,XBOOLE_0:def 4;
then consider D being Subset of M such that
A12: D is cycle and
A13: D c= (B \/ C) \ {e} by A2,A3,A11,Th43;
D c= A
proof
let x be object;
assume
A14: x in D;
then x in B\/C by A13,XBOOLE_0:def 5;
then
A15: x in B or x in C by XBOOLE_0:def 3;
x nin {e} by A13,A14,XBOOLE_0:def 5;
hence thesis by A4,A5,A15,XBOOLE_0:def 3;
end;
then D is independent by A1,Th3;
hence thesis by A12;
end;