:: Introduction to Matroids
:: by Grzegorz Bancerek and Yasunari Shidama
::
:: Received July 30, 2008
:: Copyright (c) 2008-2011 Association of Mizar Users


begin

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 independent A for open ;
antonym dependent A for open ;
end;

definition
let M be SubsetFamilyStr;
func the_family_of M -> Subset-Family of M equals :: MATROID0:def 1
the topology of M;
coherence
the topology of M is Subset-Family of M
;
end;

:: deftheorem defines the_family_of MATROID0:def 1 :
for M being SubsetFamilyStr holds the_family_of M = the topology of M;

definition
let M be SubsetFamilyStr;
let A be Subset of M;
redefine attr A is open means :Def2: :: MATROID0:def 2
A in the_family_of M;
compatibility
( A is independent iff A in the_family_of M )
by PRE_TOPC:def 5;
end;

:: deftheorem Def2 defines independent MATROID0:def 2 :
for M being SubsetFamilyStr
for A being Subset of M holds
( A is independent iff A in the_family_of M );

definition
let M be SubsetFamilyStr;
attr M is subset-closed means :Def3: :: 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 holds
ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M );
end;

:: deftheorem Def3 defines subset-closed MATROID0:def 3 :
for M being SubsetFamilyStr holds
( M is subset-closed iff the_family_of M is subset-closed );

:: deftheorem defines with_exchange_property MATROID0:def 4 :
for M being SubsetFamilyStr holds
( M is with_exchange_property iff 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 holds
ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M ) );

registration
cluster non empty finite strict non void subset-closed with_exchange_property TopStruct ;
existence
ex b1 being SubsetFamilyStr st
( b1 is strict & not b1 is empty & not b1 is void & b1 is finite & b1 is subset-closed & b1 is with_exchange_property )
proof end;
end;

registration
let M be non void SubsetFamilyStr;
cluster independent Element of bool the carrier of M;
existence
ex b1 being Subset of M st b1 is independent
proof end;
end;

registration
let M be subset-closed SubsetFamilyStr;
cluster the_family_of M -> subset-closed ;
coherence
the_family_of M is subset-closed
by Def3;
end;

theorem Th1: :: 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
proof end;

registration
let M be non void subset-closed SubsetFamilyStr;
cluster finite independent Element of bool the carrier of M;
existence
ex b1 being Subset of M st
( b1 is finite & b1 is independent )
proof end;
end;

definition
mode Matroid is non empty non void subset-closed with_exchange_property SubsetFamilyStr;
end;

theorem Th2: :: MATROID0:2
for M being subset-closed SubsetFamilyStr holds
( not M is void iff {} in the_family_of M )
proof end;

registration
let M be non void subset-closed SubsetFamilyStr;
cluster empty -> independent Element of bool the carrier of M;
coherence
for b1 being Subset of M st b1 is empty holds
b1 is independent
proof end;
end;

theorem Th3: :: 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 )
proof 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
for b1 being Subset of M st b1 = A /\ B holds
b1 is independent
proof end;
cluster B /\ A -> independent Subset of M;
coherence
for b1 being Subset of M st b1 = B /\ A holds
b1 is independent
;
cluster A \ B -> independent Subset of M;
coherence
for b1 being Subset of M st b1 = A \ B holds
b1 is independent
proof end;
end;

theorem Th4: :: MATROID0:4
for M being non empty non void 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 holds
ex e being Element of M st
( e in B \ A & A \/ {e} is independent ) )
proof end;

notation
let A be set ;
synonym finite-membered A for with_finite-elements ;
end;

definition
let A be set ;
redefine attr A is with_finite-elements means :Def5: :: MATROID0:def 5
for B being set st B in A holds
B is finite ;
compatibility
( A is finite-membered iff for B being set st B in A holds
B is finite )
proof end;
end;

:: deftheorem Def5 defines finite-membered MATROID0:def 5 :
for A being set holds
( A is finite-membered iff for B being set st B in A holds
B is finite );

definition
let M be SubsetFamilyStr;
attr M is finite-membered means :Def6: :: MATROID0:def 6
the_family_of M is finite-membered ;
end;

:: deftheorem Def6 defines finite-membered MATROID0:def 6 :
for M being SubsetFamilyStr holds
( M is finite-membered iff the_family_of M is finite-membered );

definition
let M be SubsetFamilyStr;
attr M is finite-degree means :Def7: :: 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;

:: deftheorem Def7 defines finite-degree MATROID0:def 7 :
for M being SubsetFamilyStr holds
( M is finite-degree iff ( M is finite-membered & ex n being Nat st
for A being finite Subset of M st A is independent holds
card A <= n ) );

registration
cluster finite-degree -> finite-membered TopStruct ;
coherence
for b1 being SubsetFamilyStr st b1 is finite-degree holds
b1 is finite-membered
proof end;
cluster finite -> finite-degree TopStruct ;
coherence
for b1 being SubsetFamilyStr st b1 is finite holds
b1 is finite-degree
proof end;
end;

begin

registration
cluster non empty with_non-empty_elements mutually-disjoint set ;
existence
ex b1 being set st
( b1 is mutually-disjoint & not b1 is empty & b1 is with_non-empty_elements )
proof end;
end;

theorem Th5: :: MATROID0:5
for A, B being finite set st card A < card B holds
ex x being set st x in B \ A
proof end;

theorem :: MATROID0:6
for P being non empty with_non-empty_elements mutually-disjoint set
for f being Choice_Function of P holds f is one-to-one
proof end;

registration
cluster discrete -> discrete non void subset-closed with_exchange_property TopStruct ;
coherence
for b1 being discrete SubsetFamilyStr holds
( not b1 is void & b1 is subset-closed & b1 is with_exchange_property )
proof end;
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 :Def8: :: 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 holds
ex d being set st A /\ D c= {d}
}
);
existence
ex b1 being strict SubsetFamilyStr st
( the carrier of b1 = union P & the_family_of b1 = { A where A is Subset of (union P) : for D being set st D in P holds
ex d being set st A /\ D c= {d}
}
)
proof end;
uniqueness
for b1, b2 being strict SubsetFamilyStr st the carrier of b1 = union P & the_family_of b1 = { A where A is Subset of (union P) : for D being set st D in P holds
ex d being set st A /\ D c= {d}
}
& the carrier of b2 = union P & the_family_of b2 = { A where A is Subset of (union P) : for D being set st D in P holds
ex d being set st A /\ D c= {d}
}
holds
b1 = b2
;
end;

:: deftheorem Def8 defines ProdMatroid MATROID0:def 8 :
for P being set
for b2 being strict SubsetFamilyStr holds
( b2 = ProdMatroid P iff ( the carrier of b2 = union P & the_family_of b2 = { A where A is Subset of (union P) : for D being set st D in P holds
ex d being set st A /\ D c= {d}
}
) );

registration
let P be non empty with_non-empty_elements set ;
cluster ProdMatroid P -> non empty strict ;
coherence
not ProdMatroid P is empty
proof end;
end;

theorem Th8: :: 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} )
proof end;

registration
let P be set ;
cluster ProdMatroid P -> strict non void subset-closed ;
coherence
( not ProdMatroid P is void & ProdMatroid P is subset-closed )
proof end;
end;

theorem Th9: :: 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 set st a in x holds
a in f . a
proof end;

theorem Th10: :: 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 set st a in x holds
a in f . a ) holds
( x is independent iff f is one-to-one )
proof end;

registration
let P be mutually-disjoint set ;
cluster ProdMatroid P -> strict with_exchange_property ;
coherence
ProdMatroid P is with_exchange_property
proof end;
end;

registration
let X be finite set ;
let P be Subset of (bool X);
cluster ProdMatroid P -> finite strict ;
coherence
ProdMatroid P is finite
proof end;
end;

registration
let X be set ;
cluster -> mutually-disjoint a_partition of X;
coherence
for b1 being a_partition of X holds b1 is mutually-disjoint
proof end;
end;

registration
cluster non empty finite strict non void subset-closed with_exchange_property TopStruct ;
existence
ex b1 being Matroid st
( b1 is finite & b1 is strict )
proof end;
end;

registration
let M be non void finite-membered SubsetFamilyStr;
cluster independent -> finite independent Element of bool the carrier of M;
coherence
for b1 being independent Subset of M holds b1 is finite
proof end;
end;

definition
let F be Field;
let V be VectSp of F;
func LinearlyIndependentSubsets V -> strict SubsetFamilyStr means :Def9: :: 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 } );
existence
ex b1 being strict SubsetFamilyStr st
( the carrier of b1 = the carrier of V & the_family_of b1 = { A where A is Subset of V : A is linearly-independent } )
proof end;
uniqueness
for b1, b2 being strict SubsetFamilyStr st the carrier of b1 = the carrier of V & the_family_of b1 = { A where A is Subset of V : A is linearly-independent } & the carrier of b2 = the carrier of V & the_family_of b2 = { A where A is Subset of V : A is linearly-independent } holds
b1 = b2
;
end;

:: deftheorem Def9 defines LinearlyIndependentSubsets MATROID0:def 9 :
for F being Field
for V being VectSp of F
for b3 being strict SubsetFamilyStr holds
( b3 = LinearlyIndependentSubsets V iff ( the carrier of b3 = the carrier of V & the_family_of b3 = { A where A is Subset of V : A is linearly-independent } ) );

registration
let F be Field;
let V be VectSp of F;
cluster LinearlyIndependentSubsets V -> non empty strict non void subset-closed ;
coherence
( not LinearlyIndependentSubsets V is empty & not LinearlyIndependentSubsets V is void & LinearlyIndependentSubsets V is subset-closed )
proof end;
end;

theorem Th11: :: MATROID0:11
for F being Field
for 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 end;

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 holds
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 end;

theorem Th13: :: MATROID0:13
for F being Field
for V being VectSp of F
for A being Subset of V st A is linearly-independent holds
for a being Element of V st a nin the carrier of (Lin A) holds
A \/ {a} is linearly-independent
proof end;

registration
let F be Field;
let V be VectSp of F;
cluster LinearlyIndependentSubsets V -> strict with_exchange_property ;
coherence
LinearlyIndependentSubsets V is with_exchange_property
proof end;
end;

registration
let F be Field;
let V be finite-dimensional VectSp of F;
cluster LinearlyIndependentSubsets V -> strict finite-membered ;
coherence
LinearlyIndependentSubsets V is finite-membered
proof end;
end;

begin

definition
let M be SubsetFamilyStr;
let A, C be Subset of M;
pred A is_maximal_independent_in C means :Def10: :: 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;

:: deftheorem Def10 defines is_maximal_independent_in MATROID0:def 10 :
for M being SubsetFamilyStr
for A, C being Subset of M holds
( A is_maximal_independent_in C iff ( 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 ) ) );

theorem Th14: :: MATROID0:14
for M being non void finite-degree SubsetFamilyStr
for C, A being Subset of M st A c= C & A is independent holds
ex B being independent Subset of M st
( A c= B & B is_maximal_independent_in C )
proof end;

theorem :: MATROID0:15
for M being non void subset-closed finite-degree SubsetFamilyStr
for C being Subset of M ex A being independent Subset of M st A is_maximal_independent_in C
proof end;

theorem Th16: :: 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
for 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 end;

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 } ;
coherence
union { (card A) where A is independent Subset of M : A c= C } is Nat
proof end;
end;

:: deftheorem defines Rnk MATROID0:def 11 :
for M being finite-degree Matroid
for C being Subset of M holds Rnk C = union { (card A) where A is independent Subset of M : A c= C } ;

theorem Th17: :: 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
proof end;

theorem Th18: :: 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 )
proof end;

theorem Th19: :: 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 ) )
proof end;

theorem Th20: :: MATROID0:20
for M being finite-degree Matroid
for C being finite Subset of M holds Rnk C <= card C
proof end;

theorem Th21: :: MATROID0:21
for M being finite-degree Matroid
for C being finite Subset of M holds
( C is independent iff card C = Rnk C )
proof end;

definition
let M be finite-degree Matroid;
func Rnk M -> Nat equals :: MATROID0:def 12
Rnk ([#] M);
coherence
Rnk ([#] M) is Nat
;
end;

:: deftheorem defines Rnk MATROID0:def 12 :
for M being finite-degree Matroid holds Rnk M = Rnk ([#] M);

definition
let M be non void finite-degree SubsetFamilyStr;
mode Basis of M -> independent Subset of M means :Def13: :: MATROID0:def 13
it is_maximal_independent_in [#] M;
existence
ex b1 being independent Subset of M st b1 is_maximal_independent_in [#] M
proof end;
end;

:: deftheorem Def13 defines Basis MATROID0:def 13 :
for M being non void finite-degree SubsetFamilyStr
for b2 being independent Subset of M holds
( b2 is Basis of M iff b2 is_maximal_independent_in [#] M );

theorem :: MATROID0:22
for M being finite-degree Matroid
for B1, B2 being Basis of M holds card B1 = card B2
proof end;

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
proof end;

theorem Th24: :: MATROID0:24
for M being finite-degree Matroid
for A, B being Subset of M st A c= B holds
Rnk A <= Rnk B
proof end;

theorem Th25: :: MATROID0:25
for M being finite-degree Matroid
for A, B being Subset of M holds (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B)
proof end;

theorem Th26: :: MATROID0:26
for M being finite-degree Matroid
for A, B being Subset of M
for e being Element of M holds
( Rnk A <= Rnk (A \/ B) & Rnk (A \/ {e}) <= (Rnk A) + 1 )
proof end;

theorem :: MATROID0:27
for M being finite-degree Matroid
for A being Subset of M
for e, f being Element of M st Rnk (A \/ {e}) = Rnk (A \/ {f}) & Rnk (A \/ {f}) = Rnk A holds
Rnk (A \/ {e,f}) = Rnk A
proof end;

begin

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 :Def14: :: MATROID0:def 14
Rnk (A \/ {e}) = Rnk A;
end;

:: deftheorem Def14 defines is_dependent_on MATROID0:def 14 :
for M being finite-degree Matroid
for e being Element of M
for A being Subset of M holds
( e is_dependent_on A iff Rnk (A \/ {e}) = Rnk A );

theorem Th28: :: MATROID0:28
for M being finite-degree Matroid
for A being Subset of M
for e being Element of M st e in A holds
e is_dependent_on A
proof end;

theorem Th29: :: MATROID0:29
for M being finite-degree Matroid
for A, B being Subset of M
for e being Element of M st A c= B & e is_dependent_on A holds
e is_dependent_on B
proof end;

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 } ;
coherence
{ e where e is Element of M : e is_dependent_on A } is Subset of M
proof end;
end;

:: deftheorem defines Span MATROID0:def 15 :
for M being finite-degree Matroid
for A being Subset of M holds Span A = { e where e is Element of M : e is_dependent_on A } ;

theorem Th30: :: MATROID0:30
for M being finite-degree Matroid
for A being Subset of M
for e being Element of M holds
( e in Span A iff Rnk (A \/ {e}) = Rnk A )
proof end;

theorem Th31: :: MATROID0:31
for M being finite-degree Matroid
for A being Subset of M holds A c= Span A
proof end;

theorem :: MATROID0:32
for M being finite-degree Matroid
for A, B being Subset of M st A c= B holds
Span A c= Span B
proof end;

theorem Th33: :: MATROID0:33
for M being finite-degree Matroid
for A being Subset of M holds Rnk (Span A) = Rnk A
proof end;

theorem Th34: :: MATROID0:34
for M being finite-degree Matroid
for A being Subset of M
for e being Element of M st e is_dependent_on Span A holds
e is_dependent_on A
proof end;

theorem :: MATROID0:35
for M being finite-degree Matroid
for A being Subset of M holds Span (Span A) = Span A
proof end;

theorem :: MATROID0:36
for M being finite-degree Matroid
for A being Subset of M
for f, e being Element of M st f nin Span A & f in Span (A \/ {e}) holds
e in Span (A \/ {f})
proof end;

definition
let M be SubsetFamilyStr;
let A be Subset of M;
attr A is cycle means :Def16: :: MATROID0:def 16
( not A is independent & ( for e being Element of M st e in A holds
A \ {e} is independent ) );
end;

:: deftheorem Def16 defines cycle MATROID0:def 16 :
for M being SubsetFamilyStr
for A being Subset of M holds
( A is cycle iff ( not A is independent & ( for e being Element of M st e in A holds
A \ {e} is independent ) ) );

theorem Th37: :: MATROID0:37
for M being finite-degree Matroid
for A being Subset of M st A is cycle holds
( not A is empty & A is finite )
proof end;

registration
let M be finite-degree Matroid;
cluster cycle -> non empty finite Element of bool the carrier of M;
coherence
for b1 being Subset of M st b1 is cycle holds
( not b1 is empty & b1 is finite )
by Th37;
end;

theorem Th38: :: MATROID0:38
for M being finite-degree Matroid
for A being Subset of M holds
( A is cycle iff ( not A is empty & ( for e being Element of M st e in A holds
A \ {e} is_maximal_independent_in A ) ) )
proof end;

theorem Th39: :: MATROID0:39
for M being finite-degree Matroid
for A being Subset of M st A is cycle holds
(Rnk A) + 1 = card A
proof end;

theorem :: MATROID0:40
for M being finite-degree Matroid
for A being Subset of M
for e being Element of M st A is cycle & e in A holds
e is_dependent_on A \ {e}
proof end;

theorem Th41: :: MATROID0:41
for M being finite-degree Matroid
for A, B being Subset of M st A is cycle & B is cycle & A c= B holds
A = B
proof end;

theorem Th42: :: MATROID0:42
for M being finite-degree Matroid
for A being Subset of M st ( for B being Subset of M st B c= A holds
not B is cycle ) holds
A is independent
proof end;

theorem Th43: :: MATROID0:43
for M being finite-degree Matroid
for A, B being Subset of M
for e being Element of M st A is cycle & B is cycle & A <> B & e in A /\ B holds
ex C being Subset of M st
( C is cycle & C c= (A \/ B) \ {e} )
proof end;

theorem :: MATROID0:44
for M being finite-degree Matroid
for A, B, C being Subset of M
for e being Element of M st A is independent & B is cycle & C is cycle & B c= A \/ {e} & C c= A \/ {e} holds
B = C
proof end;