:: 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 b₁ being SubsetFamilyStr st
( b₁ is strict & not b₁ is empty & not b₁ is void & b₁ is finite & b₁ is subset-closed & b₁ 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 b₁ being Subset of M st b₁ 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 b₁ being Subset of M st
( b₁ is finite & b₁ 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 b₁ being Subset of M st b₁ is empty holds
b₁ 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 b₁ being Subset of M st b₁ = A /\ B holds
b₁ is independent

proof end;

cluster B /\ A -> independent Subset of M;
coherence
for b₁ being Subset of M st b₁ = B /\ A holds
b₁ is independent ;
cluster A \ B -> independent Subset of M;
coherence
for b₁ being Subset of M st b₁ = A \ B holds
b₁ 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 b₁ being SubsetFamilyStr st b₁ is finite-degree holds
b₁ is finite-membered

proof end;

cluster finite -> finite-degree TopStruct ;
coherence
for b₁ being SubsetFamilyStr st b₁ is finite holds
b₁ is finite-degree

proof end;

end;

begin

registration

cluster non empty with_non-empty_elements mutually-disjoint set ;
existence
ex b₁ being set st
( b₁ is mutually-disjoint & not b₁ is empty & b₁ 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 b₁ being discrete SubsetFamilyStr holds
( not b₁ is void & b₁ is subset-closed & b₁ 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 b₁ being strict SubsetFamilyStr st
( the carrier of b₁ = union P & the_family_of b₁ = { 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 b₁, b₂ being strict SubsetFamilyStr st the carrier of b₁ = union P & the_family_of b₁ = { 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 b₂ = union P & the_family_of b₂ = { 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
b₁ = b₂ ;

end;

:: deftheorem Def8 defines ProdMatroid MATROID0:def 8 :
for P being set
for b₂ being strict SubsetFamilyStr holds
( b₂ = ProdMatroid P iff ( the carrier of b₂ = union P & the_family_of b₂ = { 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 b₁ being a_partition of X holds b₁ is mutually-disjoint

proof end;

end;

registration

cluster non empty finite strict non void subset-closed with_exchange_property TopStruct ;
existence
ex b₁ being Matroid st
( b₁ is finite & b₁ 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 b₁ being independent Subset of M holds b₁ 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 b₁ being strict SubsetFamilyStr st
( the carrier of b₁ = the carrier of V & the_family_of b₁ = { A where A is Subset of V : A is linearly-independent } )

proof end;

uniqueness
for b₁, b₂ being strict SubsetFamilyStr st the carrier of b₁ = the carrier of V & the_family_of b₁ = { A where A is Subset of V : A is linearly-independent } & the carrier of b₂ = the carrier of V & the_family_of b₂ = { A where A is Subset of V : A is linearly-independent } holds
b₁ = b₂ ;

end;

:: deftheorem Def9 defines LinearlyIndependentSubsets MATROID0:def 9 :
for F being Field
for V being VectSp of F
for b₃ being strict SubsetFamilyStr holds
( b₃ = LinearlyIndependentSubsets V iff ( the carrier of b₃ = the carrier of V & the_family_of b₃ = { 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 b₁ being independent Subset of M st b₁ is_maximal_independent_in [#] M

proof end;

end;

:: deftheorem Def13 defines Basis MATROID0:def 13 :
for M being non void finite-degree SubsetFamilyStr
for b₂ being independent Subset of M holds
( b₂ is Basis of M iff b₂ 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 b₁ being Subset of M st b₁ is cycle holds
( not b₁ is empty & b₁ 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;