:: Introduction to Matroids
:: by Grzegorz Bancerek and Yasunari Shidama
::
:: Received July 30, 2008
:: Copyright (c) 2008-2019 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;
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
:: MATROID0:def 1
the topology of M;
end;
definition
let M be SubsetFamilyStr;
let A be Subset of M;
redefine attr A is independent means
:: MATROID0:def 2
A in the_family_of M;
end;
definition
let M be SubsetFamilyStr;
attr M is subset-closed means
:: MATROID0:def 3
the_family_of M is subset-closed;
attr M is with_exchange_property means
:: MATROID0:def 4
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;
end;
registration
let M be non void SubsetFamilyStr;
cluster independent for Subset of M;
end;
registration
let M be subset-closed SubsetFamilyStr;
cluster the_family_of M -> subset-closed;
end;
theorem :: MATROID0:1
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;
registration
let M be non void subset-closed SubsetFamilyStr;
cluster finite independent for Subset of M;
end;
definition
mode Matroid is non empty non void subset-closed with_exchange_property
SubsetFamilyStr;
end;
theorem :: MATROID0:2
for M being subset-closed SubsetFamilyStr holds M is non void iff
{} in the_family_of M;
registration
let M be non void subset-closed SubsetFamilyStr;
cluster empty -> independent for Subset of M;
end;
theorem :: MATROID0:3
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
;
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;
cluster B/\A -> independent for Subset of M;
cluster A\B -> independent for Subset of M;
end;
theorem :: MATROID0:4
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;
definition
::$CD
let M be SubsetFamilyStr;
attr M is finite-membered means
:: MATROID0:def 6
the_family_of M is finite-membered;
end;
definition
let M be SubsetFamilyStr;
attr M is finite-degree means
:: MATROID0:def 7
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;
cluster finite -> finite-degree for SubsetFamilyStr;
end;
begin :: Examples
registration
cluster mutually-disjoint non empty with_non-empty_elements for set;
end;
theorem :: MATROID0:5
for A,B being finite set st card A < card B ex x being set st x in B \ A;
theorem :: MATROID0:6
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;
registration
cluster -> non void subset-closed with_exchange_property for discrete
SubsetFamilyStr;
end;
theorem :: MATROID0:7
for T being non empty discrete TopStruct holds T is Matroid;
definition
let P be set;
func ProdMatroid P -> strict SubsetFamilyStr means
:: MATROID0:def 8
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}};
end;
registration
let P be non empty with_non-empty_elements set;
cluster ProdMatroid P -> non empty;
end;
theorem :: MATROID0:8
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};
registration
let P be set;
cluster ProdMatroid P -> non void subset-closed;
end;
theorem :: MATROID0:9
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;
theorem :: MATROID0:10
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;
registration
let P be mutually-disjoint set;
cluster ProdMatroid P -> with_exchange_property;
end;
registration
let X be finite set;
let P be Subset of bool X;
cluster ProdMatroid P -> finite;
end;
registration
let X be set;
cluster -> mutually-disjoint for a_partition of X;
end;
registration
cluster finite strict for Matroid;
end;
registration
let M be finite-membered non void SubsetFamilyStr;
cluster -> finite for independent Subset of M;
end;
definition
let F be Field;
let V be VectSp of F;
func LinearlyIndependentSubsets V -> strict SubsetFamilyStr means
:: MATROID0:def 9
the
carrier of it = the carrier of V & the_family_of it = {A where A is Subset of V
: A is linearly-independent};
end;
registration
let F be Field;
let V be VectSp of F;
cluster LinearlyIndependentSubsets V -> non empty non void subset-closed;
end;
theorem :: MATROID0:11
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;
theorem :: MATROID0:12
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});
theorem :: MATROID0:13
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;
registration
let F be Field;
let V be VectSp of F;
cluster LinearlyIndependentSubsets V -> with_exchange_property;
end;
registration
let F be Field;
let V be finite-dimensional VectSp of F;
cluster LinearlyIndependentSubsets V -> finite-membered;
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
:: MATROID0:def 10
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 :: MATROID0:14
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;
theorem :: MATROID0:15
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;
theorem :: MATROID0:16
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;
definition
let M be finite-degree Matroid;
let C be Subset of M;
func Rnk C -> Nat equals
:: MATROID0:def 11
union {card A where A is independent Subset of M: A
c= C};
end;
theorem :: MATROID0:17
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;
theorem :: MATROID0:18
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;
theorem :: MATROID0:19
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;
theorem :: MATROID0:20
for M being finite-degree Matroid for C being finite Subset of M
holds Rnk C <= card C;
theorem :: MATROID0:21
for M being finite-degree Matroid for C being finite Subset of M
holds C is independent iff card C = Rnk C;
definition
let M be finite-degree Matroid;
func Rnk M -> Nat equals
:: MATROID0:def 12
Rnk [#]M;
end;
definition
let M be non void finite-degree SubsetFamilyStr;
mode Basis of M -> independent Subset of M means
:: MATROID0:def 13
it is_maximal_independent_in [#]M;
end;
theorem :: MATROID0:22
for M being finite-degree Matroid for B1,B2 being Basis of M holds
card B1 = card B2;
theorem :: MATROID0:23
for M being finite-degree Matroid for A being independent Subset of M
ex B being Basis of M st A c= B;
reserve M for finite-degree Matroid,
A,B,C for Subset of M,
e,f for Element of M;
theorem :: MATROID0:24
A c= B implies Rnk A <= Rnk B;
theorem :: MATROID0:25
Rnk (A\/B) + Rnk (A/\B) <= Rnk A + Rnk B;
theorem :: MATROID0:26
Rnk A <= Rnk (A\/B) & Rnk (A \/ {e}) <= Rnk A + 1;
theorem :: MATROID0:27
Rnk (A\/{e}) = Rnk (A\/{f}) & Rnk (A\/{f}) = Rnk A implies Rnk (A \/ {
e,f}) = Rnk A;
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
:: MATROID0:def 14
Rnk (A \/ {e}) = Rnk A;
end;
theorem :: MATROID0:28
e in A implies e is_dependent_on A;
theorem :: MATROID0:29
A c= B & e is_dependent_on A implies e is_dependent_on B;
definition
let M be finite-degree Matroid;
let A be Subset of M;
func Span A -> Subset of M equals
:: MATROID0:def 15
{e where e is Element of M: e
is_dependent_on A};
end;
theorem :: MATROID0:30
e in Span A iff Rnk (A \/ {e}) = Rnk A;
theorem :: MATROID0:31
A c= Span A;
theorem :: MATROID0:32
A c= B implies Span A c= Span B;
theorem :: MATROID0:33
Rnk Span A = Rnk A;
theorem :: MATROID0:34
e is_dependent_on Span A implies e is_dependent_on A;
theorem :: MATROID0:35
Span Span A = Span A;
theorem :: MATROID0:36
f nin Span A & f in Span (A \/ {e}) implies e in Span (A \/ {f});
definition
let M be SubsetFamilyStr;
let A be Subset of M;
attr A is cycle means
:: MATROID0:def 16
A is dependent & for e being Element of M st e
in A holds A \ {e} is independent;
end;
theorem :: MATROID0:37
A is cycle implies A is non empty finite;
registration
let M;
cluster cycle -> non empty finite for Subset of M;
end;
theorem :: MATROID0:38
A is cycle iff A is non empty & for e st e in A holds A\{e}
is_maximal_independent_in A;
theorem :: MATROID0:39
A is cycle implies Rnk A + 1 = card A;
theorem :: MATROID0:40
A is cycle & e in A implies e is_dependent_on A\{e};
theorem :: MATROID0:41
A is cycle & B is cycle & A c= B implies A = B;
theorem :: MATROID0:42
(for B st B c= A holds B is not cycle) implies A is independent;
theorem :: MATROID0:43
A is cycle & B is cycle & A <> B & e in A /\ B implies ex C st C
is cycle & C c= (A \/ B) \ {e};
theorem :: MATROID0:44
A is independent & B is cycle & C is cycle & B c= A\/{e} & C c= A\/{e}
implies B = C;