:: MATROID0 semantic presentation
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_2;
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;
attrM is subset-closed means :Def3: :: MATROID0:def 3
the_family_of M is subset-closed ;
attrM 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 for 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
reconsider S = bool {0} as Subset-Family of {0} ;
take M = TopStruct(# {0},S #); ::_thesis: ( M is strict & not M is empty & not M is void & M is finite & M is subset-closed & M is with_exchange_property )
thus M is strict ; ::_thesis: ( not M is empty & not M is void & M is finite & M is subset-closed & M is with_exchange_property )
thus not the carrier of M is empty ; :: according to STRUCT_0:def_1 ::_thesis: ( not M is void & M is finite & M is subset-closed & M is with_exchange_property )
thus not the topology of M is empty ; :: according to PENCIL_1:def_4 ::_thesis: ( M is finite & M is subset-closed & M is with_exchange_property )
thus the carrier of M is finite ; :: according to STRUCT_0:def_11 ::_thesis: ( M is subset-closed & M is with_exchange_property )
thus the_family_of M is subset-closed by COH_SP:2; :: according to MATROID0:def_3 ::_thesis: M is with_exchange_property
let A, B be finite Subset of M; :: according to MATROID0:def_4 ::_thesis: ( A in the_family_of M & B in the_family_of M & card B = (card A) + 1 implies ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M ) )
assume A in the_family_of M ; ::_thesis: ( not B in the_family_of M or not card B = (card A) + 1 or ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M ) )
assume B in the_family_of M ; ::_thesis: ( not card B = (card A) + 1 or ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M ) )
assume A1: card B = (card A) + 1 ; ::_thesis: ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M )
reconsider e = 0 as Element of M by TARSKI:def_1;
take e ; ::_thesis: ( e in B \ A & A \/ {e} in the_family_of M )
A2: bool {0} = {{},{0}} by ZFMISC_1:24;
then A3: ( B = {} or B = {0} ) by TARSKI:def_2;
then A4: ( card B = 0 or card B = 1 ) by CARD_1:30;
A5: ( A = {} or A = {0} ) by A2, TARSKI:def_2;
then ( card A = 0 or card A = 1 ) by CARD_1:30;
hence ( e in B \ A & A \/ {e} in the_family_of M ) by A1, A5, A3, A4; ::_thesis: verum
end;
end;
registration
let M be non void SubsetFamilyStr;
cluster independent for Element of K19( the carrier of M);
existence
ex b1 being Subset of M st b1 is independent
proof
set a = the Element of the topology of M;
reconsider a = the Element of the topology of M as Subset of M ;
take a ; ::_thesis: a is independent
thus a in the_family_of M ; :: according to MATROID0:def_2 ::_thesis: verum
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
let M be non void subset-closed SubsetFamilyStr; ::_thesis: for A being independent Subset of M
for B being set st B c= A holds
B is independent Subset of M
let A be independent Subset of M; ::_thesis: for B being set st B c= A holds
B is independent Subset of M
let B be set ; ::_thesis: ( B c= A implies B is independent Subset of M )
assume A1: B c= A ; ::_thesis: B is independent Subset of M
A in the_family_of M by Def2;
then B in the_family_of M by A1, CLASSES1:def_1;
hence B is independent Subset of M by Def2; ::_thesis: verum
end;
registration
let M be non void subset-closed SubsetFamilyStr;
cluster finite independent for Element of K19( the carrier of M);
existence
ex b1 being Subset of M st
( b1 is finite & b1 is independent )
proof
set a = the Element of the topology of M;
reconsider a = the Element of the topology of M as independent Subset of M by PRE_TOPC:def_2;
{} c= a by XBOOLE_1:2;
then reconsider b = {} as independent Subset of M by Th1;
take b ; ::_thesis: ( b is finite & b is independent )
thus ( b is finite & b is independent ) ; ::_thesis: verum
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
let M be subset-closed SubsetFamilyStr; ::_thesis: ( not M is void iff {} in the_family_of M )
hereby ::_thesis: ( {} in the_family_of M implies not M is void )
assume not M is void ; ::_thesis: {} in the_family_of M
then reconsider M9 = M as non void subset-closed SubsetFamilyStr ;
set a = the independent Subset of M9;
{} c= the independent Subset of M9 by XBOOLE_1:2;
then {} is independent Subset of M9 by Th1;
hence {} in the_family_of M by Def2; ::_thesis: verum
end;
assume {} in the_family_of M ; ::_thesis: not M is void
hence not the topology of M is empty ; :: according to PENCIL_1:def_4 ::_thesis: verum
end;
registration
let M be non void subset-closed SubsetFamilyStr;
cluster empty -> independent for Element of K19( the carrier of M);
coherence
for b1 being Subset of M st b1 is empty holds
b1 is independent
proof
let S be Subset of M; ::_thesis: ( S is empty implies S is independent )
assume S is empty ; ::_thesis: S is independent
hence S in the_family_of M by Th2; :: according to MATROID0:def_2 ::_thesis: verum
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
let M be non void SubsetFamilyStr; ::_thesis: ( M is subset-closed iff for A, B being Subset of M st A is independent & B c= A holds
B is independent )
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; ::_thesis: ( ( for A, B being Subset of M st A is independent & B c= A holds
B is independent ) implies M is subset-closed )
assume A1: for A, B being Subset of M st A is independent & B c= A holds
B is independent ; ::_thesis: M is subset-closed
let x, y be set ; :: according to CLASSES1:def_1,MATROID0:def_3 ::_thesis: ( not x in the_family_of M or y c/= x or y in the_family_of M )
assume x in the_family_of M ; ::_thesis: ( y c/= x or y in the_family_of M )
then A2: x is independent Subset of M by Def2;
assume y c= x ; ::_thesis: y in the_family_of M
then y is independent Subset of M by A1, A2, XBOOLE_1:1;
hence y in the_family_of M by Def2; ::_thesis: verum
end;
registration
let M be non void subset-closed SubsetFamilyStr;
let A be independent Subset of M;
let B be set ;
clusterA /\ B -> independent for Subset of M;
coherence
for b1 being Subset of M st b1 = A /\ B holds
b1 is independent
proof
A /\ B c= A by XBOOLE_1:17;
hence for b1 being Subset of M st b1 = A /\ B holds
b1 is independent by Th3; ::_thesis: verum
end;
clusterB /\ A -> independent for Subset of M;
coherence
for b1 being Subset of M st b1 = B /\ A holds
b1 is independent ;
clusterA \ B -> independent for Subset of M;
coherence
for b1 being Subset of M st b1 = A \ B holds
b1 is independent
proof
A \ B c= A by XBOOLE_1:36;
hence for b1 being Subset of M st b1 = A \ B holds
b1 is independent by Th3; ::_thesis: verum
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
let M be non empty non void SubsetFamilyStr; ::_thesis: ( 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 ) )
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 holds
ex e being Element of M st
( e in B \ A & A \/ {e} is independent ) ) ::_thesis: ( ( 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 ) ) implies M is with_exchange_property )
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 holds
ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M ) ; :: according to MATROID0:def_4 ::_thesis: 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 )
let A, B be finite Subset of M; ::_thesis: ( A is independent & B is independent & card B = (card A) + 1 implies ex e being Element of M st
( e in B \ A & A \/ {e} is independent ) )
assume that
A2: A in the_family_of M and
A3: B in the_family_of M and
A4: card B = (card A) + 1 ; :: according to MATROID0:def_2 ::_thesis: ex e being Element of M st
( e in B \ A & A \/ {e} is independent )
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 ; ::_thesis: ( e in B \ A & A \/ {e} is independent )
thus ( e in B \ A & A \/ {e} in the_family_of M ) by A5, A6; :: according to MATROID0:def_2 ::_thesis: verum
end;
assume A7: 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 ) ; ::_thesis: M is with_exchange_property
let A, B be finite Subset of M; :: according to MATROID0:def_4 ::_thesis: ( A in the_family_of M & B in the_family_of M & card B = (card A) + 1 implies ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M ) )
assume that
A8: A in the_family_of M and
A9: B in the_family_of M ; ::_thesis: ( not card B = (card A) + 1 or ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M ) )
A10: B is independent by A9, Def2;
assume A11: card B = (card A) + 1 ; ::_thesis: ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M )
A is independent by A8, Def2;
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 ; ::_thesis: ( e in B \ A & A \/ {e} in the_family_of M )
thus ( e in B \ A & A \/ {e} in the_family_of M ) by A12, A13, Def2; ::_thesis: verum
end;
definition
canceled;
let M be SubsetFamilyStr;
attrM is finite-membered means :Def6: :: MATROID0:def 6
the_family_of M is finite-membered ;
end;
:: deftheorem MATROID0:def_5_:_
canceled;
:: 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;
attrM 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 for TopStruct ;
coherence
for b1 being SubsetFamilyStr st b1 is finite-degree holds
b1 is finite-membered
proof
let M be SubsetFamilyStr; ::_thesis: ( M is finite-degree implies M is finite-membered )
assume M is finite-membered ; :: according to MATROID0:def_7 ::_thesis: ( for n being Nat ex A being finite Subset of M st
( A is independent & not card A <= n ) or M is finite-membered )
hence ( for n being Nat ex A being finite Subset of M st
( A is independent & not card A <= n ) or M is finite-membered ) ; ::_thesis: verum
end;
cluster finite -> finite-degree for TopStruct ;
coherence
for b1 being SubsetFamilyStr st b1 is finite holds
b1 is finite-degree
proof
let M be SubsetFamilyStr; ::_thesis: ( M is finite implies M is finite-degree )
assume the carrier of M is finite ; :: according to STRUCT_0:def_11 ::_thesis: M is finite-degree
then reconsider X = the carrier of M as finite set ;
thus M is finite-membered :: according to MATROID0:def_7 ::_thesis: ex n being Nat st
for A being finite Subset of M st A is independent holds
card A <= n
proof
let x be set ; :: according to FINSET_1:def_6,MATROID0:def_6 ::_thesis: ( not x in the_family_of M or x is finite )
assume x in the_family_of M ; ::_thesis: x is finite
then x c= X ;
hence x is finite ; ::_thesis: verum
end;
take card X ; ::_thesis: for A being finite Subset of M st A is independent holds
card A <= card X
let A be finite Subset of M; ::_thesis: ( A is independent implies card A <= card X )
thus ( A is independent implies card A <= card X ) by NAT_1:43; ::_thesis: verum
end;
end;
begin
registration
cluster non empty mutually-disjoint with_non-empty_elements for set ;
existence
ex b1 being set st
( b1 is mutually-disjoint & not b1 is empty & b1 is with_non-empty_elements )
proof
take {{0}} ; ::_thesis: ( {{0}} is mutually-disjoint & not {{0}} is empty & {{0}} is with_non-empty_elements )
thus ( {{0}} is mutually-disjoint & not {{0}} is empty & {{0}} is with_non-empty_elements ) by TAXONOM2:10; ::_thesis: verum
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
let A, B be finite set ; ::_thesis: ( card A < card B implies ex x being set st x in B \ A )
assume card A < card B ; ::_thesis: ex x being set st x in B \ A
then not B c= A by NAT_1:43;
then consider x being set such that
A1: x in B and
A2: x nin A by TARSKI:def_3;
take x ; ::_thesis: x in B \ A
thus x in B \ A by A1, A2, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem :: MATROID0:6
for P being non empty mutually-disjoint with_non-empty_elements set
for f being Choice_Function of P holds f is one-to-one
proof
let P be non empty mutually-disjoint with_non-empty_elements set ; ::_thesis: for f being Choice_Function of P holds f is one-to-one
let f be Choice_Function of P; ::_thesis: f is one-to-one
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in K48(f) or not x2 in K48(f) or not f . x1 = f . x2 or x1 = x2 )
assume that
A1: x1 in dom f and
A2: x2 in dom f and
A3: f . x1 = f . x2 ; ::_thesis: x1 = x2
A4: not {} in P ;
then A5: f . x1 in x1 by A1, ORDERS_1:def_1;
f . x1 in x2 by A2, A3, A4, ORDERS_1:def_1;
then x1 meets x2 by A5, XBOOLE_0:3;
hence x1 = x2 by A1, A2, TAXONOM2:def_5; ::_thesis: verum
end;
registration
cluster discrete -> discrete non void subset-closed with_exchange_property for TopStruct ;
coherence
for b1 being discrete SubsetFamilyStr holds
( not b1 is void & b1 is subset-closed & b1 is with_exchange_property )
proof
let T be discrete SubsetFamilyStr; ::_thesis: ( not T is void & T is subset-closed & T is with_exchange_property )
not the topology of T is empty by TDLAT_3:def_1;
hence A1: not T is void by PENCIL_1:def_4; ::_thesis: ( T is subset-closed & T is with_exchange_property )
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; ::_thesis: T is with_exchange_property
let A, B be finite Subset of T; :: according to MATROID0:def_4 ::_thesis: ( A in the_family_of T & B in the_family_of T & card B = (card A) + 1 implies ex e being Element of T st
( e in B \ A & A \/ {e} in the_family_of T ) )
assume that
A in the_family_of T and
B in the_family_of T and
A2: card B = (card A) + 1 ; ::_thesis: ex e being Element of T st
( e in B \ A & A \/ {e} in the_family_of T )
now__::_thesis:_not_B_c=_A
assume B c= A ; ::_thesis: contradiction
then card B c= 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; ::_thesis: verum
end;
then consider x being set such that
A3: x in B and
A4: not x in A by TARSKI:def_3;
reconsider x = 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 ; ::_thesis: ( x in B \ A & A \/ {x} in the_family_of T )
thus x in B \ A by A3, A4, XBOOLE_0:def_5; ::_thesis: A \/ {x} in the_family_of T
C is independent by TDLAT_3:15;
hence A \/ {x} in the_family_of T by Def2; ::_thesis: verum
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
set F = { 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} } ;
set X = union P;
{ 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} } c= bool (union P)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { 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} } or x in bool (union P) )
assume x in { 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} } ; ::_thesis: x in bool (union P)
then ex A being Subset of (union P) st
( x = A & ( for D being set st D in P holds
ex d being set st A /\ D c= {d} ) ) ;
hence x in bool (union P) ; ::_thesis: verum
end;
then reconsider F = { 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} } as Subset-Family of (union P) ;
take TopStruct(# (union P),F #) ; ::_thesis: ( the carrier of TopStruct(# (union P),F #) = union P & the_family_of TopStruct(# (union P),F #) = { 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} } )
thus ( the carrier of TopStruct(# (union P),F #) = union P & the_family_of TopStruct(# (union P),F #) = { 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} } ) ; ::_thesis: verum
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
set M = ProdMatroid P;
the carrier of (ProdMatroid P) = union P by Def8;
hence not the carrier of (ProdMatroid P) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
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
let P be set ; ::_thesis: 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} )
set M = ProdMatroid P;
A1: the_family_of (ProdMatroid P) = { 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} } by Def8;
let A be Subset of (ProdMatroid P); ::_thesis: ( A is independent iff for D being Element of P ex d being Element of D st A /\ D c= {d} )
A2: the carrier of (ProdMatroid P) = union P by Def8;
thus ( A is independent implies for D being Element of P ex d being Element of D st A /\ D c= {d} ) ::_thesis: ( ( for D being Element of P ex d being Element of D st A /\ D c= {d} ) implies A is independent )
proof
assume A in the_family_of (ProdMatroid P) ; :: according to MATROID0:def_2 ::_thesis: for D being Element of P ex d being Element of D st A /\ D c= {d}
then A3: ex B being Subset of (union P) st
( A = B & ( for D being set st D in P holds
ex d being set st B /\ D c= {d} ) ) by A1;
let D be Element of P; ::_thesis: ex d being Element of D st A /\ D c= {d}
( P = {} implies ( A = {} & {} /\ D = {} ) ) by A2, ZFMISC_1:2;
then ( P = {} implies A /\ D c= {1} ) by XBOOLE_1:2;
then consider d being set such that
A4: A /\ D c= {d} by A3;
set d0 = the Element of D;
now__::_thesis:_(_d_nin_D_implies_A_/\_D_c=_{_the_Element_of_D}_)
assume d nin D ; ::_thesis: A /\ D c= { the Element of 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= { the Element of D} by XBOOLE_1:2; ::_thesis: verum
end;
hence ex d being Element of D st A /\ D c= {d} by A4; ::_thesis: verum
end;
assume A5: for D being Element of P ex d being Element of D st A /\ D c= {d} ; ::_thesis: A is independent
A6: now__::_thesis:_for_D_being_set_st_D_in_P_holds_
ex_d_being_set_st_A_/\_D_c=_{d}
let D be set ; ::_thesis: ( D in P implies ex d being set st A /\ D c= {d} )
assume D in P ; ::_thesis: ex d being set st A /\ D c= {d}
then ex d being Element of D st A /\ D c= {d} by A5;
hence ex d being set st A /\ D c= {d} ; ::_thesis: verum
end;
the carrier of (ProdMatroid P) = union P by Def8;
hence A in the_family_of (ProdMatroid P) by A1, A6; :: according to MATROID0:def_2 ::_thesis: verum
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
set M = ProdMatroid P;
A1: the_family_of (ProdMatroid P) = { 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} } by Def8;
set A = {} (union P);
now__::_thesis:_for_D_being_set_st_D_in_P_holds_
ex_d_being_set_st_({}_(union_P))_/\_D_c=_{d}
let D be set ; ::_thesis: ( D in P implies ex d being set st ({} (union P)) /\ D c= {d} )
assume D in P ; ::_thesis: ex d being set st ({} (union P)) /\ D c= {d}
take d = {} ; ::_thesis: ({} (union P)) /\ D c= {d}
thus ({} (union P)) /\ D c= {d} by XBOOLE_1:2; ::_thesis: verum
end;
then {} (union P) in the_family_of (ProdMatroid P) by A1;
hence not the topology of (ProdMatroid P) is empty ; :: according to PENCIL_1:def_4 ::_thesis: ProdMatroid P is subset-closed
thus the_family_of (ProdMatroid P) is subset-closed :: according to MATROID0:def_3 ::_thesis: verum
proof
let a, b be set ; :: according to CLASSES1:def_1 ::_thesis: ( not a in the_family_of (ProdMatroid P) or b c/= a or b in the_family_of (ProdMatroid P) )
assume that
A2: a in the_family_of (ProdMatroid P) and
A3: b c= a ; ::_thesis: b in the_family_of (ProdMatroid P)
A4: ex B being Subset of (union P) st
( a = B & ( for D being set st D in P holds
ex d being set st B /\ D c= {d} ) ) by A1, A2;
A5: now__::_thesis:_for_D_being_set_st_D_in_P_holds_
ex_d_being_set_st_b_/\_D_c=_{d}
let D be set ; ::_thesis: ( D in P implies ex d being set st b /\ D c= {d} )
assume D in P ; ::_thesis: ex d being set st b /\ D c= {d}
then consider d being set such that
A6: a /\ D c= {d} by A4;
take d = d; ::_thesis: b /\ D c= {d}
b /\ D c= a /\ D by A3, XBOOLE_1:26;
hence b /\ D c= {d} by A6, XBOOLE_1:1; ::_thesis: verum
end;
b is Subset of (union P) by A3, A4, XBOOLE_1:1;
hence b in the_family_of (ProdMatroid P) by A1, A5; ::_thesis: verum
end;
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
defpred S1[ set , set ] means $1 in $2;
let P be mutually-disjoint set ; ::_thesis: 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
let x be Subset of (ProdMatroid P); ::_thesis: ex f being Function of x,P st
for a being set st a in x holds
a in f . a
A1: now__::_thesis:_for_a_being_set_st_a_in_x_holds_
ex_y_being_set_st_
(_y_in_P_&_S1[a,y]_)
let a be set ; ::_thesis: ( a in x implies ex y being set st
( y in P & S1[a,y] ) )
assume a in x ; ::_thesis: ex y being set st
( y in P & S1[a,y] )
then a in the carrier of (ProdMatroid P) ;
then a in union P by Def8;
then ex y being set st
( a in y & y in P ) by TARSKI:def_4;
hence ex y being set st
( y in P & S1[a,y] ) ; ::_thesis: verum
end;
consider f being Function of x,P such that
A2: for a being set st a in x holds
S1[a,f . a] from FUNCT_2:sch_1(A1);
take f ; ::_thesis: for a being set st a in x holds
a in f . a
thus for a being set st a in x holds
a in f . a by A2; ::_thesis: verum
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
let P be mutually-disjoint set ; ::_thesis: 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 )
let x be Subset of (ProdMatroid P); ::_thesis: 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 )
let f be Function of x,P; ::_thesis: ( ( for a being set st a in x holds
a in f . a ) implies ( x is independent iff f is one-to-one ) )
assume A1: for a being set st a in x holds
a in f . a ; ::_thesis: ( x is independent iff f is one-to-one )
hereby ::_thesis: ( f is one-to-one implies x is independent )
assume A2: x is independent ; ::_thesis: f is one-to-one
thus f is one-to-one ::_thesis: verum
proof
let a, b be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not a in K48(f) or not b in K48(f) or not f . a = f . b or a = b )
assume that
A3: a in dom f and
A4: b in dom f ; ::_thesis: ( not f . a = f . b or a = b )
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 ( not f . a = f . b or a = b ) by A7, A6, TARSKI:def_1; ::_thesis: verum
end;
end;
assume A8: f is one-to-one ; ::_thesis: x is independent
now__::_thesis:_for_D_being_Element_of_P_holds_
not__for_d_being_Element_of_D_holds_x_/\_D_c/=_{d}
let D be Element of P; ::_thesis: not for d being Element of D holds x /\ D c/= {d}
set d1 = the Element of D;
assume A9: for d being Element of D holds x /\ D c/= {d} ; ::_thesis: contradiction
then x /\ D c/= { the Element of D} ;
then consider d2 being set such that
A10: d2 in x /\ D and
d2 nin { the Element of D} by TARSKI:def_3;
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 Def8;
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not a in x /\ D or a in {d2} )
assume A16: a in x /\ D ; ::_thesis: a in {d2}
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, FUNCT_1:def_4;
hence a in {d2} by TARSKI:def_1; ::_thesis: verum
end;
hence contradiction by A9, A11; ::_thesis: verum
end;
hence x is independent by Th8; ::_thesis: verum
end;
registration
let P be mutually-disjoint set ;
cluster ProdMatroid P -> strict with_exchange_property ;
coherence
ProdMatroid P is with_exchange_property
proof
set M = ProdMatroid P;
A1: the_family_of (ProdMatroid P) = { 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} } by Def8;
let A, B be finite Subset of (ProdMatroid P); :: according to MATROID0:def_4 ::_thesis: ( A in the_family_of (ProdMatroid P) & B in the_family_of (ProdMatroid P) & card B = (card A) + 1 implies ex e being Element of (ProdMatroid P) st
( e in B \ A & A \/ {e} in the_family_of (ProdMatroid P) ) )
assume that
A2: A in the_family_of (ProdMatroid P) and
A3: B in the_family_of (ProdMatroid P) ; ::_thesis: ( not card B = (card A) + 1 or ex e being Element of (ProdMatroid P) st
( e in B \ A & A \/ {e} in the_family_of (ProdMatroid P) ) )
consider f being Function of A,P such that
A4: for a being set st a in A holds
a in f . a by Th9;
assume card B = (card A) + 1 ; ::_thesis: ex e being Element of (ProdMatroid P) st
( e in B \ A & A \/ {e} in the_family_of (ProdMatroid P) )
then A5: card B > card A by NAT_1:13;
consider g being Function of B,P such that
A6: for a being set st a in B holds
a in g . a by Th9;
A7: the carrier of (ProdMatroid P) = union P by Def8;
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, Def2;
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, Def2;
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 set such that
A13: x9 in B and
A14: a = g . x9 by A11, A12, FUNCT_1:def_3;
reconsider x = x9 as Element of (ProdMatroid P) by A13;
take x ; ::_thesis: ( x in B \ A & A \/ {x} in the_family_of (ProdMatroid P) )
A15: a nin A9 by A12, XBOOLE_0:def_5;
now__::_thesis:_not_x_in_A
A16: x in g . x by A6, A13;
assume A17: x in A ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence x in B \ A by A13, XBOOLE_0:def_5; ::_thesis: A \/ {x} in the_family_of (ProdMatroid P)
reconsider xx = {x} as Subset of (ProdMatroid P) by A13, ZFMISC_1:31;
reconsider Ax = A \/ xx as Subset of (union P) by Def8;
A20: a in B9 by A12;
now__::_thesis:_for_D_being_set_st_D_in_P_holds_
ex_x9_being_set_st_Ax_/\_D_c=_{x9}
let D be set ; ::_thesis: ( D in P implies ex x9 being set st Ax /\ x9 c= {b2} )
A21: Ax /\ D = (A /\ D) \/ (xx /\ D) by XBOOLE_1:23;
assume A22: D in P ; ::_thesis: ex x9 being set st Ax /\ x9 c= {b2}
then consider d being Element of D such that
A23: A /\ D c= {d} by A9, Th8;
percases ( D = a or D <> a ) ;
supposeA24: D = a ; ::_thesis: ex x9 being set st Ax /\ x9 c= {b2}
take x9 = x9; ::_thesis: Ax /\ D c= {x9}
A /\ D c= {}
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in A /\ D or z in {} )
assume A25: z in A /\ D ; ::_thesis: z in {}
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 z in {} by A20, A15, A24, A28, TAXONOM2:def_5; ::_thesis: verum
end;
then A /\ D = {} ;
hence Ax /\ D c= {x9} by A21, XBOOLE_1:17; ::_thesis: verum
end;
supposeA29: D <> a ; ::_thesis: ex d being set st Ax /\ d c= {b2}
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 = d as set ;
take d = d; ::_thesis: Ax /\ D c= {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; ::_thesis: verum
end;
end;
end;
hence A \/ {x} in the_family_of (ProdMatroid P) by A1; ::_thesis: verum
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
union P is finite ;
hence the carrier of (ProdMatroid P) is finite by Def8; :: according to STRUCT_0:def_11 ::_thesis: verum
end;
end;
registration
let X be set ;
cluster -> mutually-disjoint for a_partition of X;
coherence
for b1 being a_partition of X holds b1 is mutually-disjoint
proof
let P be a_partition of X; ::_thesis: P is mutually-disjoint
let x, y be set ; :: according to TAXONOM2:def_5 ::_thesis: ( not x in P or not y in P or x = y or x misses y )
thus ( not x in P or not y in P or x = y or x misses y ) by EQREL_1:def_4; ::_thesis: verum
end;
end;
registration
cluster non empty finite strict non void subset-closed with_exchange_property for TopStruct ;
existence
ex b1 being Matroid st
( b1 is finite & b1 is strict )
proof
set X = the non empty finite set ;
set P = the a_partition of the non empty finite set ;
take ProdMatroid the a_partition of the non empty finite set ; ::_thesis: ( ProdMatroid the a_partition of the non empty finite set is finite & ProdMatroid the a_partition of the non empty finite set is strict )
thus ( ProdMatroid the a_partition of the non empty finite set is finite & ProdMatroid the a_partition of the non empty finite set is strict ) ; ::_thesis: verum
end;
end;
registration
let M be non void finite-membered SubsetFamilyStr;
cluster independent -> finite independent for Element of K19( the carrier of M);
coherence
for b1 being independent Subset of M holds b1 is finite
proof
let A be independent Subset of M; ::_thesis: A is finite
A1: the_family_of M is finite-membered by Def6;
A in the_family_of M by Def2;
hence A is finite by A1; ::_thesis: verum
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
set F = { A where A is Subset of V : A is linearly-independent } ;
set X = the carrier of V;
{ A where A is Subset of V : A is linearly-independent } c= bool the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { A where A is Subset of V : A is linearly-independent } or x in bool the carrier of V )
assume x in { A where A is Subset of V : A is linearly-independent } ; ::_thesis: x in bool the carrier of V
then ex A being Subset of the carrier of V st
( x = A & A is linearly-independent ) ;
hence x in bool the carrier of V ; ::_thesis: verum
end;
then reconsider F = { A where A is Subset of V : A is linearly-independent } as Subset-Family of the carrier of V ;
take TopStruct(# the carrier of V,F #) ; ::_thesis: ( the carrier of TopStruct(# the carrier of V,F #) = the carrier of V & the_family_of TopStruct(# the carrier of V,F #) = { A where A is Subset of V : A is linearly-independent } )
thus ( the carrier of TopStruct(# the carrier of V,F #) = the carrier of V & the_family_of TopStruct(# the carrier of V,F #) = { A where A is Subset of V : A is linearly-independent } ) ; ::_thesis: verum
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
set M = LinearlyIndependentSubsets V;
A1: the_family_of (LinearlyIndependentSubsets V) = { A where A is Subset of V : A is linearly-independent } by Def9;
the carrier of (LinearlyIndependentSubsets V) = the carrier of V by Def9;
hence not the carrier of (LinearlyIndependentSubsets V) is empty ; :: according to STRUCT_0:def_1 ::_thesis: ( not LinearlyIndependentSubsets V is void & LinearlyIndependentSubsets V is subset-closed )
{} V is linearly-independent ;
then {} in the_family_of (LinearlyIndependentSubsets V) by A1;
hence not the topology of (LinearlyIndependentSubsets V) is empty ; :: according to PENCIL_1:def_4 ::_thesis: LinearlyIndependentSubsets V is subset-closed
let x, y be set ; :: according to CLASSES1:def_1,MATROID0:def_3 ::_thesis: ( not x in the_family_of (LinearlyIndependentSubsets V) or y c/= x or y in the_family_of (LinearlyIndependentSubsets V) )
assume x in the_family_of (LinearlyIndependentSubsets V) ; ::_thesis: ( y c/= x or y in the_family_of (LinearlyIndependentSubsets V) )
then A2: ex A being Subset of V st
( x = A & A is linearly-independent ) by A1;
assume A3: y c= x ; ::_thesis: y in the_family_of (LinearlyIndependentSubsets V)
then reconsider B = y as Subset of V by A2, XBOOLE_1:1;
B is linearly-independent by A2, A3, VECTSP_7:1;
hence y in the_family_of (LinearlyIndependentSubsets V) by A1; ::_thesis: verum
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
let F be Field; ::_thesis: 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 )
let V be VectSp of F; ::_thesis: for A being Subset of (LinearlyIndependentSubsets V) holds
( A is independent iff A is linearly-independent Subset of V )
set M = LinearlyIndependentSubsets V;
let B be Subset of (LinearlyIndependentSubsets V); ::_thesis: ( B is independent iff B is linearly-independent Subset of V )
the_family_of (LinearlyIndependentSubsets V) = { A where A is Subset of V : A is linearly-independent } by Def9;
then ( B in the_family_of (LinearlyIndependentSubsets V) iff ex A being Subset of V st
( B = A & A is linearly-independent ) ) ;
hence ( B is independent iff B is linearly-independent Subset of V ) by Def2; ::_thesis: verum
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
let F be Field; ::_thesis: 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}) )
let V be VectSp of F; ::_thesis: 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}) )
let A, B be finite Subset of V; ::_thesis: ( B c= A implies 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}) ) )
assume B c= A ; ::_thesis: 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}) )
then A = B \/ (A \ B) by XBOOLE_1:45;
hence 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}) ) by VECTSP_9:18; ::_thesis: verum
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
let F be Field; ::_thesis: 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
let V be VectSp of F; ::_thesis: 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
let A be Subset of V; ::_thesis: ( A is linearly-independent implies for a being Element of V st a nin the carrier of (Lin A) holds
A \/ {a} is linearly-independent )
assume A1: A is linearly-independent ; ::_thesis: for a being Element of V st a nin the carrier of (Lin A) holds
A \/ {a} is linearly-independent
A2: { (Sum s) where s is Linear_Combination of A : verum } = the carrier of (Lin A) by VECTSP_7:def_2;
let a be Element of V; ::_thesis: ( a nin the carrier of (Lin A) implies A \/ {a} is linearly-independent )
set B = A \/ {a};
assume that
A3: a nin the carrier of (Lin A) and
A4: A \/ {a} is linearly-dependent ; ::_thesis: contradiction
consider l being Linear_Combination of A \/ {a} 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in the carrier of (Lin A) )
assume A8: x in A ; ::_thesis: x in the carrier of (Lin A)
then reconsider x = x as Element of V ;
x in Lin A by A8, VECTSP_7:8;
hence x in the carrier of (Lin A) by STRUCT_0:def_5; ::_thesis: verum
end;
then a nin A by A3;
then (A \/ {a}) \ 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__::_thesis:_not_l_._a_<>_0._F
assume l . a <> 0. F ; ::_thesis: contradiction
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; ::_thesis: verum
end;
then A11: a nin Carrier l by VECTSP_6:2;
A12: Carrier l c= A \/ {a} by VECTSP_6:def_4;
Carrier l c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in A )
thus ( not x in Carrier l or x in A ) by A11, A12, ZFMISC_1:136; ::_thesis: verum
end;
then l is Linear_Combination of A by VECTSP_6:def_4;
hence contradiction by A1, A5, A6, VECTSP_7:def_1; ::_thesis: verum
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
set M = LinearlyIndependentSubsets V;
A1: the_family_of (LinearlyIndependentSubsets V) = { A where A is Subset of V : A is linearly-independent } by Def9;
let A, B be finite Subset of (LinearlyIndependentSubsets V); :: according to MATROID0:def_4 ::_thesis: ( A in the_family_of (LinearlyIndependentSubsets V) & B in the_family_of (LinearlyIndependentSubsets V) & card B = (card A) + 1 implies ex e being Element of (LinearlyIndependentSubsets V) st
( e in B \ A & A \/ {e} in the_family_of (LinearlyIndependentSubsets V) ) )
assume that
A2: A in the_family_of (LinearlyIndependentSubsets V) and
A3: B in the_family_of (LinearlyIndependentSubsets V) and
A4: card B = (card A) + 1 ; ::_thesis: ex e being Element of (LinearlyIndependentSubsets V) st
( e in B \ A & A \/ {e} in the_family_of (LinearlyIndependentSubsets V) )
A5: B is independent by A3, Def2;
A is independent by A2, Def2;
then reconsider A9 = A, B9 = B as finite linearly-independent Subset of V by A5, Th11;
set V9 = Lin (A9 \/ B9);
A9 c= the carrier of (Lin (A9 \/ B9))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A9 or a in the carrier of (Lin (A9 \/ B9)) )
assume a in A9 ; ::_thesis: a in the carrier of (Lin (A9 \/ B9))
then a in A9 \/ B9 by XBOOLE_0:def_3;
then a in Lin (A9 \/ B9) by VECTSP_7:8;
hence a in the carrier of (Lin (A9 \/ B9)) by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider A99 = A9 as finite linearly-independent Subset of (Lin (A9 \/ B9)) by VECTSP_9:12;
B9 c= the carrier of (Lin (A9 \/ B9))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B9 or a in the carrier of (Lin (A9 \/ B9)) )
assume a in B9 ; ::_thesis: a in the carrier of (Lin (A9 \/ B9))
then a in A9 \/ B9 by XBOOLE_0:def_3;
then a in Lin (A9 \/ B9) by VECTSP_7:8;
hence a in the carrier of (Lin (A9 \/ B9)) by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider B99 = B9 as finite linearly-independent Subset of (Lin (A9 \/ B9)) by VECTSP_9:12;
A6: Lin (A9 \/ B9) = Lin (A99 \/ B99) by VECTSP_9:17;
then consider D being Basis of Lin (A9 \/ B9) such that
A7: B9 c= D by VECTSP_7:19;
consider C being Basis of Lin (A9 \/ B9) such that
A8: C c= A99 \/ B99 by A6, VECTSP_7:20;
reconsider c = C as finite set by A8;
c is Basis of Lin (A9 \/ B9) ;
then Lin (A9 \/ B9) is finite-dimensional by MATRLIN:def_1;
then card c = card D by VECTSP_9:22;
then card B c= 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__::_thesis:_not_C_c=_the_carrier_of_(Lin_A9)
assume C c= the carrier of (Lin A9) ; ::_thesis: contradiction
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; ::_thesis: verum
end;
then consider x being set such that
A14: x in C and
A15: x nin the carrier of (Lin A9) by TARSKI:def_3;
A16: x in C \ the carrier of (Lin A9) by A14, A15, XBOOLE_0:def_5;
then A17: the Element of C \ the carrier of (Lin A9) nin the carrier of (Lin A9) by XBOOLE_0:def_5;
A18: the Element of C \ the carrier of (Lin A9) in C by A16, XBOOLE_0:def_5;
then the Element of C \ the carrier of (Lin A9) in A \/ B by A8;
then reconsider e = the Element of C \ the carrier of (Lin A9) as Element of (LinearlyIndependentSubsets V) ;
take e ; ::_thesis: ( e in B \ A & A \/ {e} in the_family_of (LinearlyIndependentSubsets V) )
A c= the carrier of (Lin A9)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in the carrier of (Lin A9) )
assume x in A ; ::_thesis: x in the carrier of (Lin A9)
then x in Lin A9 by VECTSP_7:8;
hence x in the carrier of (Lin A9) by STRUCT_0:def_5; ::_thesis: verum
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; ::_thesis: A \/ {e} in the_family_of (LinearlyIndependentSubsets V)
reconsider a = e as Element of V by A20;
A9 \/ {a} is linearly-independent by A17, Th13;
hence A \/ {e} in the_family_of (LinearlyIndependentSubsets V) by A1; ::_thesis: verum
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
let A be set ; :: according to FINSET_1:def_6,MATROID0:def_6 ::_thesis: ( not A in the_family_of (LinearlyIndependentSubsets V) or A is finite )
set M = LinearlyIndependentSubsets V;
assume A in the_family_of (LinearlyIndependentSubsets V) ; ::_thesis: A is finite
then A is independent Subset of (LinearlyIndependentSubsets V) by Def2;
then A is linearly-independent Subset of V by Th11;
hence A is finite by VECTSP_9:21; ::_thesis: verum
end;
end;
begin
definition
let M be SubsetFamilyStr;
let A, C be Subset of M;
predA 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
let M be non void finite-degree SubsetFamilyStr; ::_thesis: 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 )
let C, A0 be Subset of M; ::_thesis: ( A0 c= C & A0 is independent implies ex B being independent Subset of M st
( A0 c= B & B is_maximal_independent_in C ) )
assume that
A1: A0 c= C and
A2: A0 is independent ; ::_thesis: ex B being independent Subset of M st
( A0 c= B & B is_maximal_independent_in C )
reconsider AA = A0 as independent Subset of M by A2;
defpred S1[ 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 Def7;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
S1[n] by A3;
then A4: ex n being Nat st S1[n] ;
consider n0 being Nat such that
A5: ( S1[n0] & ( for m being Nat st S1[m] holds
n0 <= m ) ) from NAT_1:sch_5(A4);
now__::_thesis:_ex_A_being_independent_Subset_of_M_st_
(_A0_c=_A_&_A_c=_C_&_not_card_A_<_n0_)
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 ; ::_thesis: contradiction
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 = n as Element of NAT by ORDINAL1:def_12;
S1[n]
proof
let A be finite Subset of M; ::_thesis: ( A0 c= A & A c= C & A is independent implies card A <= n )
assume that
A9: A0 c= A and
A10: A c= C and
A11: A is independent ; ::_thesis: card A <= n
card A < n + 1 by A7, A8, A9, A10, A11;
hence card A <= n by NAT_1:13; ::_thesis: verum
end;
then n + 1 <= n by A5, A8;
hence contradiction by NAT_1:13; ::_thesis: verum
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 ; ::_thesis: ( A0 c= A & A is_maximal_independent_in C )
thus ( A0 c= A & A is independent & A c= C ) by A12, A13; :: according to MATROID0:def_10 ::_thesis: for B being Subset of M st B is independent & B c= C & A c= B holds
A = B
let B be Subset of M; ::_thesis: ( B is independent & B c= C & A c= B implies A = B )
assume that
A16: B is independent and
A17: B c= C and
A18: A c= B ; ::_thesis: A = 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, XBOOLE_1:1;
then card B9 <= n0 by A5, A17;
then card B9 = n0 by A19, XXREAL_0:1;
hence A = B by A14, A18, A15, CARD_FIN:1, XXREAL_0:1; ::_thesis: verum
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
let M be non void subset-closed finite-degree SubsetFamilyStr; ::_thesis: for C being Subset of M ex A being independent Subset of M st A is_maximal_independent_in C
let C be Subset of M; ::_thesis: ex A being independent Subset of M st A is_maximal_independent_in C
{} M c= C by XBOOLE_1:2;
then ex A being independent Subset of M st
( {} M c= A & A is_maximal_independent_in C ) by Th14;
hence ex A being independent Subset of M st A is_maximal_independent_in C ; ::_thesis: verum
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
let M be non empty non void subset-closed finite-degree SubsetFamilyStr; ::_thesis: ( 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 )
hereby ::_thesis: ( ( 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 ) implies M is Matroid )
assume A1: M is Matroid ; ::_thesis: 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
let C be Subset of M; ::_thesis: 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
A2: now__::_thesis:_for_A,_B_being_independent_Subset_of_M_st_A_is_maximal_independent_in_C_&_B_is_maximal_independent_in_C_holds_
not_card_A_<_card_B
let A, B be independent Subset of M; ::_thesis: ( A is_maximal_independent_in C & B is_maximal_independent_in C implies not card A < card B )
assume that
A3: A is_maximal_independent_in C and
A4: B is_maximal_independent_in C and
A5: card A < card B ; ::_thesis: contradiction
A6: A c= C by A3, Def10;
(card A) + 1 <= card B by A5, NAT_1:13;
then (card A) + 1 c= 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 = 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, XBOOLE_1:1;
B c= C by A4, Def10;
then D \ A c= C by A11, XBOOLE_1:1;
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, Def10;
then {e} c= A by XBOOLE_1:7;
then e in A by ZFMISC_1:31;
hence contradiction by A9, XBOOLE_0:def_5; ::_thesis: verum
end;
let A, B be independent Subset of M; ::_thesis: ( A is_maximal_independent_in C & B is_maximal_independent_in C implies card A = card B )
assume that
A13: A is_maximal_independent_in C and
A14: B is_maximal_independent_in C ; ::_thesis: card A = card B
( 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; ::_thesis: verum
end;
assume A15: 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 ; ::_thesis: M is Matroid
M is with_exchange_property
proof
let A, B be finite Subset of M; :: according to MATROID0:def_4 ::_thesis: ( A in the_family_of M & B in the_family_of M & card B = (card A) + 1 implies ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_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 ; ::_thesis: ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M )
B is independent by A17, Def2;
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 being Element of M st e in B \ A holds
not A \/ {e} in the_family_of M ; ::_thesis: contradiction
reconsider A = 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; :: according to MATROID0:def_2,MATROID0:def_10 ::_thesis: ( A c= C & ( for B being Subset of M st B is independent & B c= C & A c= B holds
A = B ) )
thus A c= C by XBOOLE_1:7; ::_thesis: for B being Subset of M st B is independent & B c= C & A c= B holds
A = B
let D be Subset of M; ::_thesis: ( D is independent & D c= C & A c= D implies A = D )
assume that
A23: D is independent and
A24: D c= C and
A25: A c= D ; ::_thesis: A = D
assume ( not A c= D or not D c= A ) ; :: according to XBOOLE_0:def_10 ::_thesis: contradiction
then consider e being set such that
A26: e in D and
A27: not e in A by A25, TARSKI:def_3;
reconsider e = 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: not A \/ {e} is independent by Def2;
{e} c= D by A26, ZFMISC_1:31;
then A \/ {e} c= D by A25, XBOOLE_1:8;
hence contradiction by A23, A28, Th3; ::_thesis: verum
end;
then card A = card B9 by A15, A20;
hence contradiction by A18, A21, NAT_1:13; ::_thesis: verum
end;
hence M is Matroid ; ::_thesis: verum
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
set X = { (card A) where A is independent Subset of M : A c= C } ;
defpred S1[ Nat] means ex A being independent Subset of M st
( A c= C & $1 = card A );
defpred S2[ 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 Def7;
A2: ex ne being Nat st S2[ne]
proof
take n ; ::_thesis: S2[n]
thus S2[n] by A1; ::_thesis: verum
end;
consider n0 being Nat such that
A3: ( S2[n0] & ( for m being Nat st S2[m] holds
n0 <= m ) ) from NAT_1:sch_5(A2);
union { (card A) where A is independent Subset of M : A c= C } = n0
proof
now__::_thesis:_for_a_being_set_st_a_in__{__(card_A)_where_A_is_independent_Subset_of_M_:_A_c=_C__}__holds_
a_c=_n0
let a be set ; ::_thesis: ( a in { (card A) where A is independent Subset of M : A c= C } implies a c= n0 )
assume a in { (card A) where A is independent Subset of M : A c= C } ; ::_thesis: a c= n0
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;
hence a c= n0 by A4, NAT_1:39; ::_thesis: verum
end;
hence union { (card A) where A is independent Subset of M : A c= C } c= n0 by ZFMISC_1:76; :: according to XBOOLE_0:def_10 ::_thesis: not n0 c/= union { (card A) where A is independent Subset of M : A c= C }
A6: {} M c= C by XBOOLE_1:2;
A7: for k being Nat st S1[k] holds
k <= n0 by A3;
card {} = card {} ;
then A8: ex n being Nat st S1[n] by A6;
consider n being Nat such that
A9: ( S1[n] & ( for m being Nat st S1[m] holds
m <= n ) ) from NAT_1:sch_6(A7, A8);
S2[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 { (card A) where A is independent Subset of M : A c= C } by A9;
hence not n0 c/= union { (card A) where A is independent Subset of M : A c= C } by ZFMISC_1:74; ::_thesis: verum
end;
hence union { (card A) where A is independent Subset of M : A c= C } is Nat ; ::_thesis: verum
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
let M be finite-degree Matroid; ::_thesis: for C being Subset of M
for A being independent Subset of M st A c= C holds
card A <= Rnk C
let C be Subset of M; ::_thesis: for A being independent Subset of M st A c= C holds
card A <= Rnk C
let A be independent Subset of M; ::_thesis: ( A c= C implies card A <= Rnk C )
assume A c= C ; ::_thesis: card A <= Rnk C
then card A in { (card B) where B is independent Subset of M : B c= C } ;
then card A c= Rnk C by ZFMISC_1:74;
hence card A <= Rnk C by NAT_1:39; ::_thesis: verum
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
let M be finite-degree Matroid; ::_thesis: for C being Subset of M ex A being independent Subset of M st
( A c= C & card A = Rnk C )
let C be Subset of M; ::_thesis: ex A being independent Subset of M st
( A c= C & card A = Rnk C )
defpred S1[ Nat] means for A being independent Subset of M st A c= C holds
card A <= $1;
defpred S2[ 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 by XBOOLE_1:2;
card {} = card {} ;
then A2: ex n being Nat st S2[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 Def7;
A4: ex ne being Nat st S1[ne]
proof
take n ; ::_thesis: S1[n]
thus S1[n] by A3; ::_thesis: verum
end;
consider n0 being Nat such that
A5: ( S1[n0] & ( for m being Nat st S1[m] holds
n0 <= m ) ) from NAT_1:sch_5(A4);
now__::_thesis:_for_a_being_set_st_a_in__{__(card_A)_where_A_is_independent_Subset_of_M_:_A_c=_C__}__holds_
a_c=_n0
let a be set ; ::_thesis: ( a in { (card A) where A is independent Subset of M : A c= C } implies a c= n0 )
assume a in { (card A) where A is independent Subset of M : A c= C } ; ::_thesis: a c= n0
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;
hence a c= n0 by A6, NAT_1:39; ::_thesis: verum
end;
then A8: Rnk C c= n0 by ZFMISC_1:76;
A9: for k being Nat st S2[k] holds
k <= n0 by A5;
consider n being Nat such that
A10: ( S2[n] & ( for m being Nat st S2[m] holds
m <= n ) ) from NAT_1:sch_6(A9, A2);
S1[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 ; ::_thesis: ( A c= C & card A = Rnk C )
n <= n0 by A5, A10;
then A14: n = n0 by A11, XXREAL_0:1;
then n0 in { (card A) where A is independent Subset of M : A c= C } by A12, A13;
then n0 c= Rnk C by ZFMISC_1:74;
hence ( A c= C & card A = Rnk C ) by A8, A12, A13, A14, XBOOLE_0:def_10; ::_thesis: verum
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
let M be finite-degree Matroid; ::_thesis: 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 ) )
let C be Subset of M; ::_thesis: for A being independent Subset of M holds
( A is_maximal_independent_in C iff ( A c= C & card A = Rnk C ) )
set X = { (card A) where A is independent Subset of M : A c= C } ;
let A be independent Subset of M; ::_thesis: ( A is_maximal_independent_in C iff ( A c= C & card A = Rnk C ) )
consider B being independent Subset of M such that
A1: B c= C and
A2: card B = Rnk C by Th18;
A3: now__::_thesis:_for_A_being_independent_Subset_of_M_st_A_c=_C_&_card_A_=_Rnk_C_holds_
A_is_maximal_independent_in_C
let A be independent Subset of M; ::_thesis: ( A c= C & card A = Rnk C implies A is_maximal_independent_in C )
assume that
A4: A c= C and
A5: card A = Rnk C ; ::_thesis: A is_maximal_independent_in C
thus A is_maximal_independent_in C ::_thesis: verum
proof
thus ( A is independent & A c= C ) by A4; :: according to MATROID0:def_10 ::_thesis: for B being Subset of M st B is independent & B c= C & A c= B holds
A = B
let B be Subset of M; ::_thesis: ( B is independent & B c= C & A c= B implies A = B )
assume B is independent ; ::_thesis: ( not B c= C or not A c= B or A = B )
then reconsider B9 = B as independent Subset of M ;
assume B c= C ; ::_thesis: ( not A c= B or A = B )
then card B9 in { (card A) where A is independent Subset of M : A c= C } ;
then A6: card B9 c= Rnk C by ZFMISC_1:74;
assume A7: A c= B ; ::_thesis: A = B
then card A c= card B9 by CARD_1:11;
then card A = card B9 by A5, A6, XBOOLE_0:def_10;
hence A = B by A7, CARD_FIN:1; ::_thesis: verum
end;
end;
hereby ::_thesis: ( A c= C & card A = Rnk C implies A is_maximal_independent_in C )
assume A8: A is_maximal_independent_in C ; ::_thesis: ( A c= C & card A = Rnk C )
hence A c= C by Def10; ::_thesis: card A = Rnk C
B is_maximal_independent_in C by A3, A1, A2;
hence card A = Rnk C by A2, A8, Th16; ::_thesis: verum
end;
thus ( A c= C & card A = Rnk C implies A is_maximal_independent_in C ) by A3; ::_thesis: verum
end;
theorem Th20: :: MATROID0:20
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; ::_thesis: for C being finite Subset of M holds Rnk C <= card C
let C be finite Subset of M; ::_thesis: Rnk C <= card C
ex A being independent Subset of M st
( A c= C & card A = Rnk C ) by Th18;
then Rnk C c= card C by CARD_1:11;
hence Rnk C <= card C by NAT_1:39; ::_thesis: verum
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
let M be finite-degree Matroid; ::_thesis: for C being finite Subset of M holds
( C is independent iff card C = Rnk C )
let C be finite Subset of M; ::_thesis: ( C is independent iff card C = Rnk C )
set X = { (card A) where A is independent Subset of M : A c= C } ;
hereby ::_thesis: ( card C = Rnk C implies C is independent )
assume C is independent ; ::_thesis: card C = Rnk C
then card C in { (card A) where A is independent Subset of M : A c= C } ;
then card C c= 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; ::_thesis: verum
end;
ex A being independent Subset of M st
( A c= C & card A = Rnk C ) by Th18;
hence ( card C = Rnk C implies C is independent ) by CARD_FIN:1; ::_thesis: verum
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
set A = the independent Subset of M;
set C = [#] M;
consider B being independent Subset of M such that
the independent Subset of M c= B and
A1: B is_maximal_independent_in [#] M by Th14;
take B ; ::_thesis: B is_maximal_independent_in [#] M
thus B is_maximal_independent_in [#] M by A1; ::_thesis: verum
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
let M be finite-degree Matroid; ::_thesis: for B1, B2 being Basis of M holds card B1 = card B2
let B1, B2 be Basis of M; ::_thesis: card B1 = card B2
A1: B2 is_maximal_independent_in [#] M by Def13;
B1 is_maximal_independent_in [#] M by Def13;
hence card B1 = card B2 by A1, Th16; ::_thesis: verum
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
let M be finite-degree Matroid; ::_thesis: for A being independent Subset of M ex B being Basis of M st A c= B
let A be independent Subset of M; ::_thesis: ex B being Basis of M st A c= B
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 = B as Basis of M by A2, Def13;
take B ; ::_thesis: A c= B
thus A c= B by A1; ::_thesis: verum
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
let M be finite-degree Matroid; ::_thesis: for A, B being Subset of M st A c= B holds
Rnk A <= Rnk B
let A, B be Subset of M; ::_thesis: ( A c= B implies Rnk A <= Rnk B )
ex C being independent Subset of M st
( C c= A & card C = Rnk A ) by Th18;
hence ( A c= B implies Rnk A <= Rnk B ) by Th17, XBOOLE_1:1; ::_thesis: verum
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
let M be finite-degree Matroid; ::_thesis: for A, B being Subset of M holds (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B)
let A, B be Subset of M; ::_thesis: (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B)
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, XBOOLE_1:1;
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, Def10;
A6: Ca /\ B c= C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ca /\ B or x in C )
assume A7: x in Ca /\ B ; ::_thesis: x in C
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, Def10;
then {x} c= C by XBOOLE_1:7;
hence x in C by ZFMISC_1:31; ::_thesis: verum
end;
A /\ B c= B by XBOOLE_1:17;
then C c= B by A1, XBOOLE_1:1;
then C c= Ca /\ B by A3, XBOOLE_1:19;
then A11: Ca /\ B = C by A6, XBOOLE_0:def_10;
A c= A \/ B by XBOOLE_1:7;
then Ca c= A \/ B by A5, XBOOLE_1:1;
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, Th19;
A16: C9 = Ca \/ (C9 /\ B)
proof
thus C9 c= Ca \/ (C9 /\ B) :: according to XBOOLE_0:def_10 ::_thesis: not Ca \/ (C9 /\ B) c/= C9
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C9 or x in Ca \/ (C9 /\ B) )
assume A17: x in C9 ; ::_thesis: x in Ca \/ (C9 /\ B)
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__::_thesis:_(_x_in_A_implies_x_in_Ca_)
assume x in A ; ::_thesis: x in Ca
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, Def10;
then {x} c= Ca by XBOOLE_1:7;
hence x in Ca by ZFMISC_1:31; ::_thesis: verum
end;
( x in B implies x in C9 /\ B ) by A17, XBOOLE_0:def_4;
hence x in Ca \/ (C9 /\ B) by A15, A17, A18, XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ca \/ (C9 /\ B) or x in C9 )
assume x in Ca \/ (C9 /\ B) ; ::_thesis: x in C9
then ( x in Ca or x in C9 /\ B ) by XBOOLE_0:def_3;
hence x in C9 by A12, XBOOLE_0:def_4; ::_thesis: verum
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 (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B) by A22, XREAL_1:6; ::_thesis: verum
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
let M be finite-degree Matroid; ::_thesis: 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 )
let A, B be Subset of M; ::_thesis: for e being Element of M holds
( Rnk A <= Rnk (A \/ B) & Rnk (A \/ {e}) <= (Rnk A) + 1 )
let e be Element of M; ::_thesis: ( Rnk A <= Rnk (A \/ B) & Rnk (A \/ {e}) <= (Rnk A) + 1 )
A1: card {e} = 1 by CARD_1:30;
thus Rnk A <= Rnk (A \/ B) by Th24, XBOOLE_1:7; ::_thesis: Rnk (A \/ {e}) <= (Rnk A) + 1
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 Rnk (A \/ {e}) <= (Rnk A) + 1 by A3, XXREAL_0:2; ::_thesis: verum
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
let M be finite-degree Matroid; ::_thesis: 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
let A be Subset of M; ::_thesis: 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
let e, f be Element of M; ::_thesis: ( Rnk (A \/ {e}) = Rnk (A \/ {f}) & Rnk (A \/ {f}) = Rnk A implies Rnk (A \/ {e,f}) = Rnk A )
assume that
A1: Rnk (A \/ {e}) = Rnk (A \/ {f}) and
A2: Rnk (A \/ {f}) = Rnk A ; ::_thesis: Rnk (A \/ {e,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, XBOOLE_1:1;
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, XBOOLE_1:1;
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, XBOOLE_1:1;
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, Th19;
now__::_thesis:_not_C9_<>_C
assume C9 <> C ; ::_thesis: contradiction
then consider x being set such that
A11: ( ( x in C9 & not x in C ) or ( x in C & not x in C9 ) ) by TARSKI:1;
{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__::_thesis:_not_x_in_A
assume x in A ; ::_thesis: contradiction
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, Def10;
then {x} c= C by XBOOLE_1:7;
hence contradiction by A8, A11, ZFMISC_1:31; ::_thesis: verum
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, Def10;
then {x} c= C by XBOOLE_1:7;
hence contradiction by A8, A11, ZFMISC_1:31; ::_thesis: verum
end;
hence Rnk (A \/ {e,f}) = Rnk A by A4, A9, Th19; ::_thesis: verum
end;
begin
definition
let M be finite-degree Matroid;
let e be Element of M;
let A be Subset of M;
prede 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
let M be finite-degree Matroid; ::_thesis: for A being Subset of M
for e being Element of M st e in A holds
e is_dependent_on A
let A be Subset of M; ::_thesis: for e being Element of M st e in A holds
e is_dependent_on A
let e be Element of M; ::_thesis: ( e in A implies e is_dependent_on A )
assume e in A ; ::_thesis: e is_dependent_on A
then {e} c= A by ZFMISC_1:31;
hence Rnk (A \/ {e}) = Rnk A by XBOOLE_1:12; :: according to MATROID0:def_14 ::_thesis: verum
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
let M be finite-degree Matroid; ::_thesis: 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
let A, B be Subset of M; ::_thesis: for e being Element of M st A c= B & e is_dependent_on A holds
e is_dependent_on B
let e be Element of M; ::_thesis: ( A c= B & e is_dependent_on A implies e is_dependent_on B )
assume that
A1: A c= B and
A2: Rnk (A \/ {e}) = Rnk A ; :: according to MATROID0:def_14 ::_thesis: e is_dependent_on B
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, XBOOLE_1:1;
B c= B \/ {e} by XBOOLE_1:7;
then Ca c= B \/ {e} by A5, XBOOLE_1:1;
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__::_thesis:_not_Rnk_(B_\/_{e})_=_(Rnk_B)_+_1
E c= B \/ {e} by A7, Th19;
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 ; ::_thesis: contradiction
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, Def10;
then {e} c= Ca by XBOOLE_1:7;
then B = B \/ {e} by A5, XBOOLE_1:1, XBOOLE_1:12;
hence contradiction by A14; ::_thesis: verum
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; :: according to MATROID0:def_14 ::_thesis: verum
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
set X = { e where e is Element of M : e is_dependent_on A } ;
{ e where e is Element of M : e is_dependent_on A } c= the carrier of M
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { e where e is Element of M : e is_dependent_on A } or x in the carrier of M )
assume x in { e where e is Element of M : e is_dependent_on A } ; ::_thesis: x in the carrier of M
then ex e being Element of M st
( x = e & e is_dependent_on A ) ;
hence x in the carrier of M ; ::_thesis: verum
end;
hence { e where e is Element of M : e is_dependent_on A } is Subset of M ; ::_thesis: verum
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
let M be finite-degree Matroid; ::_thesis: for A being Subset of M
for e being Element of M holds
( e in Span A iff Rnk (A \/ {e}) = Rnk A )
let A be Subset of M; ::_thesis: for e being Element of M holds
( e in Span A iff Rnk (A \/ {e}) = Rnk A )
let e be Element of M; ::_thesis: ( e in Span A iff Rnk (A \/ {e}) = Rnk A )
hereby ::_thesis: ( Rnk (A \/ {e}) = Rnk A implies e in Span A )
assume e in Span A ; ::_thesis: Rnk (A \/ {e}) = Rnk A
then ex x being Element of M st
( e = x & x is_dependent_on A ) ;
hence Rnk (A \/ {e}) = Rnk A by Def14; ::_thesis: verum
end;
assume Rnk (A \/ {e}) = Rnk A ; ::_thesis: e in Span A
then e is_dependent_on A by Def14;
hence e in Span A ; ::_thesis: verum
end;
theorem Th31: :: MATROID0:31
for M being finite-degree Matroid
for A being Subset of M holds A c= Span A
proof
let M be finite-degree Matroid; ::_thesis: for A being Subset of M holds A c= Span A
let A be Subset of M; ::_thesis: A c= Span A
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A or e in Span A )
assume A1: e in A ; ::_thesis: e in Span A
then reconsider x = e as Element of M ;
x is_dependent_on A by A1, Th28;
hence e in Span A ; ::_thesis: verum
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
let M be finite-degree Matroid; ::_thesis: for A, B being Subset of M st A c= B holds
Span A c= Span B
let A, B be Subset of M; ::_thesis: ( A c= B implies Span A c= Span B )
assume A1: A c= B ; ::_thesis: Span A c= Span B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Span A or x in Span B )
assume x in Span A ; ::_thesis: x in Span B
then ex e being Element of M st
( x = e & e is_dependent_on A ) ;
then ex e being Element of M st
( x = e & e is_dependent_on B ) by A1, Th29;
hence x in Span B ; ::_thesis: verum
end;
theorem Th33: :: MATROID0:33
for M being finite-degree Matroid
for A being Subset of M holds Rnk (Span A) = Rnk A
proof
let M be finite-degree Matroid; ::_thesis: for A being Subset of M holds Rnk (Span A) = Rnk A
let A be Subset of M; ::_thesis: Rnk (Span A) = Rnk A
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, XBOOLE_1:1;
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__::_thesis:_not_C_c/=_Ca
assume C c/= Ca ; ::_thesis: contradiction
then consider x being set such that
A5: x in C and
A6: x nin Ca by TARSKI:def_3;
C c= Span A by A4, Th19;
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, Def14
.= 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_FIN:1, XBOOLE_1:7;
then e nin {e} by A6, A7, XBOOLE_0:def_3;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
then C = Ca by A3, XBOOLE_0:def_10;
hence Rnk (Span A) = Rnk A by A2, A4, Th19; ::_thesis: verum
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
let M be finite-degree Matroid; ::_thesis: 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
let A be Subset of M; ::_thesis: for e being Element of M st e is_dependent_on Span A holds
e is_dependent_on A
let e be Element of M; ::_thesis: ( e is_dependent_on Span A implies e is_dependent_on A )
assume A1: Rnk ((Span A) \/ {e}) = Rnk (Span A) ; :: according to MATROID0:def_14 ::_thesis: e is_dependent_on 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; :: according to MATROID0:def_14 ::_thesis: verum
end;
theorem :: MATROID0:35
for M being finite-degree Matroid
for A being Subset of M holds Span (Span A) = Span A
proof
let M be finite-degree Matroid; ::_thesis: for A being Subset of M holds Span (Span A) = Span A
let A be Subset of M; ::_thesis: Span (Span A) = Span A
thus Span (Span A) c= Span A :: according to XBOOLE_0:def_10 ::_thesis: not Span A c/= Span (Span A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Span (Span A) or x in Span A )
assume x in Span (Span A) ; ::_thesis: x in 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 x in Span A by A1; ::_thesis: verum
end;
thus not Span A c/= Span (Span A) by Th31; ::_thesis: verum
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
let M be finite-degree Matroid; ::_thesis: 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})
let A be Subset of M; ::_thesis: for f, e being Element of M st f nin Span A & f in Span (A \/ {e}) holds
e in Span (A \/ {f})
let f, e be Element of M; ::_thesis: ( f nin Span A & f in Span (A \/ {e}) implies e in Span (A \/ {f}) )
assume that
A1: f nin Span A and
A2: f in Span (A \/ {e}) ; ::_thesis: e in Span (A \/ {f})
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 e in Span (A \/ {f}) by Th30; ::_thesis: verum
end;
definition
let M be SubsetFamilyStr;
let A be Subset of M;
attrA is cycle means :Def16: :: MATROID0:def 16
( A is dependent & ( 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 ( A is dependent & ( 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
let M be finite-degree Matroid; ::_thesis: for A being Subset of M st A is cycle holds
( not A is empty & A is finite )
let A be Subset of M; ::_thesis: ( A is cycle implies ( not A is empty & A is finite ) )
assume that
A1: A is dependent and
A2: for e being Element of M st e in A holds
A \ {e} is independent ; :: according to MATROID0:def_16 ::_thesis: ( not A is empty & A is finite )
thus not A is empty by A1; ::_thesis: A is finite
set e = the Element of A;
now__::_thesis:_(_A_is_non_empty_set_implies_A_is_finite_)
assume A3: A is non empty set ; ::_thesis: A is finite
then the Element of A in A ;
then reconsider e = the Element of A 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 A is finite ; ::_thesis: verum
end;
hence A is finite ; ::_thesis: verum
end;
registration
let M be finite-degree Matroid;
cluster cycle -> non empty finite for Element of K19( 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
let M be finite-degree Matroid; ::_thesis: 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 ) ) )
let A be Subset of M; ::_thesis: ( 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 ) ) )
thus ( A is cycle implies ( not A is empty & ( for e being Element of M st e in A holds
A \ {e} is_maximal_independent_in A ) ) ) ::_thesis: ( not A is empty & ( for e being Element of M st e in A holds
A \ {e} is_maximal_independent_in A ) implies A is cycle )
proof
assume that
A1: A is dependent and
A2: for e being Element of M st e in A holds
A \ {e} is independent ; :: according to MATROID0:def_16 ::_thesis: ( not A is empty & ( for e being Element of M st e in A holds
A \ {e} is_maximal_independent_in A ) )
thus not A is empty by A1; ::_thesis: for e being Element of M st e in A holds
A \ {e} is_maximal_independent_in A
let e be Element of M; ::_thesis: ( e in A implies A \ {e} is_maximal_independent_in A )
set Ae = A \ {e};
assume A3: e in A ; ::_thesis: A \ {e} is_maximal_independent_in A
hence ( A \ {e} is independent & A \ {e} c= A ) by A2, XBOOLE_1:36; :: according to MATROID0:def_10 ::_thesis: for B being Subset of M st B is independent & B c= A & A \ {e} c= B holds
A \ {e} = B
let B be Subset of M; ::_thesis: ( B is independent & B c= A & A \ {e} c= B implies A \ {e} = B )
assume that
A4: B is independent and
A5: B c= A and
A6: A \ {e} c= B ; ::_thesis: A \ {e} = B
A = (A \ {e}) \/ {e} by A3, ZFMISC_1:116;
hence A \ {e} = B by A1, A4, A5, A6, ZFMISC_1:138; ::_thesis: verum
end;
set a = the Element of A;
assume that
A7: not A is empty and
A8: for e being Element of M st e in A holds
A \ {e} is_maximal_independent_in A ; ::_thesis: A is cycle
the Element of A in A by A7;
then reconsider a = the Element of A as Element of M ;
set Ae = A \ {a};
A9: A \ {a} c= A by XBOOLE_1:36;
A10: A \ {a} is_maximal_independent_in A by A7, A8;
hereby :: according to MATROID0:def_16 ::_thesis: for e being Element of M st e in A holds
A \ {e} is independent
assume A is independent ; ::_thesis: contradiction
then A = A \ {a} by A10, A9, Def10;
then a nin {a} by A7, XBOOLE_0:def_5;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
let e be Element of M; ::_thesis: ( e in A implies A \ {e} is independent )
assume e in A ; ::_thesis: A \ {e} is independent
then A \ {e} is_maximal_independent_in A by A8;
hence A \ {e} is independent by Def10; ::_thesis: verum
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
let M be finite-degree Matroid; ::_thesis: for A being Subset of M st A is cycle holds
(Rnk A) + 1 = card A
let A be Subset of M; ::_thesis: ( A is cycle implies (Rnk A) + 1 = card A )
assume A1: A is cycle ; ::_thesis: (Rnk A) + 1 = card A
then reconsider A = A as non empty finite Subset of M ;
set a = the Element of A;
A2: A \ { the Element of A} is_maximal_independent_in A by A1, Th38;
then A \ { the Element of A} is independent by Def10;
then A3: Rnk A = card (A \ { the Element of A}) by A2, Th19;
the Element of A in { the Element of A} by TARSKI:def_1;
then A4: the Element of A nin A \ { the Element of A} by XBOOLE_0:def_5;
A = (A \ { the Element of A}) \/ { the Element of A} by ZFMISC_1:116;
hence (Rnk A) + 1 = card A by A3, A4, CARD_2:41; ::_thesis: verum
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
let M be finite-degree Matroid; ::_thesis: 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}
let A be Subset of M; ::_thesis: for e being Element of M st A is cycle & e in A holds
e is_dependent_on A \ {e}
let e be Element of M; ::_thesis: ( A is cycle & e in A implies e is_dependent_on A \ {e} )
assume that
A1: A is cycle and
A2: e in A ; ::_thesis: e is_dependent_on A \ {e}
reconsider Ae = A \ {e} as independent Subset of M by A1, A2, Def16;
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 ;
:: according to MATROID0:def_14 ::_thesis: verum
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
let M be finite-degree Matroid; ::_thesis: for A, B being Subset of M st A is cycle & B is cycle & A c= B holds
A = B
let A, B be Subset of M; ::_thesis: ( A is cycle & B is cycle & A c= B implies A = B )
assume that
A1: A is dependent and
for e being Element of M st e in A holds
A \ {e} is independent and
B is dependent and
A2: for e being Element of M st e in B holds
B \ {e} is independent ; :: according to MATROID0:def_16 ::_thesis: ( not A c= B or A = B )
assume that
A3: A c= B and
A4: A <> B ; ::_thesis: contradiction
consider x being set such that
A5: ( ( x in A & not x in B ) or ( x in B & not x in A ) ) by A4, TARSKI:1;
reconsider x = 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; ::_thesis: verum
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
let M be finite-degree Matroid; ::_thesis: 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
let A be Subset of M; ::_thesis: ( ( for B being Subset of M st B c= A holds
not B is cycle ) implies A is independent )
assume A1: for B being Subset of M st B c= A holds
not B is cycle ; ::_thesis: A is independent
consider C being independent Subset of M such that
A2: C c= A and
A3: card C = Rnk A by Th18;
percases ( A c= C or A c/= C ) ;
suppose A c= C ; ::_thesis: A is independent
hence A is independent by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
suppose A c/= C ; ::_thesis: A is independent
then consider x being set such that
A4: x in A and
A5: x nin C by TARSKI:def_3;
reconsider x = x as Element of M by A4;
A6: C c= C \/ {x} by ZFMISC_1:137;
defpred S1[ 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 S1[n]
proof
take n = Rnk A; ::_thesis: S1[n]
take C ; ::_thesis: ( card C = n & C c= C & C \/ {x} is dependent )
thus ( card C = n & C c= C ) by A3; ::_thesis: C \/ {x} is dependent
assume A9: C \/ {x} is independent ; ::_thesis: contradiction
C is_maximal_independent_in A by A2, A3, Th19;
then C = C \/ {x} by A7, A6, A9, Def10;
then {x} c= C by XBOOLE_1:7;
hence contradiction by A5, ZFMISC_1:31; ::_thesis: verum
end;
consider n being Nat such that
A10: ( S1[n] & ( for k being Nat st S1[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; :: according to MATROID0:def_16 ::_thesis: for e being Element of M st e in B \/ {x} holds
(B \/ {x}) \ {e} is independent
let e be Element of M; ::_thesis: ( e in B \/ {x} implies (B \/ {x}) \ {e} is independent )
set Be = B \ {e};
A16: B \ {e} c= B by XBOOLE_1:36;
assume A17: e in B \/ {x} ; ::_thesis: (B \/ {x}) \ {e} is independent
percases ( e in B or e = x ) by A17, ZFMISC_1:136;
supposeA18: e in B ; ::_thesis: (B \/ {x}) \ {e} is independent
A19: e nin B \ {e} by ZFMISC_1:56;
B = (B \ {e}) \/ {e} by A18, ZFMISC_1:116;
then A20: n = (card (B \ {e})) + 1 by A11, A19, CARD_2:41;
assume A21: (B \/ {x}) \ {e} is dependent ; ::_thesis: contradiction
(B \/ {x}) \ {e} = (B \ {e}) \/ {x} by A14, A18, XBOOLE_1:87, ZFMISC_1:11;
then n <= card (B \ {e}) by A10, A12, A16, A21, XBOOLE_1:1;
hence contradiction by A20, NAT_1:13; ::_thesis: verum
end;
suppose e = x ; ::_thesis: (B \/ {x}) \ {e} is independent
hence (B \/ {x}) \ {e} is independent by A14, ZFMISC_1:117; ::_thesis: verum
end;
end;
end;
B c= A by A2, A12, XBOOLE_1:1;
then B \/ {x} c= A by A4, ZFMISC_1:137;
hence A is independent by A1, A15; ::_thesis: verum
end;
end;
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
let M be finite-degree Matroid; ::_thesis: 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} )
let A, B be Subset of M; ::_thesis: 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} )
let e be Element of M; ::_thesis: ( A is cycle & B is cycle & A <> B & e in A /\ B implies ex C being Subset of M st
( C is cycle & C c= (A \/ B) \ {e} ) )
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 being Subset of M st C is cycle holds
C c/= (A \/ B) \ {e} ; ::_thesis: contradiction
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 set such that
A7: a in A and
A8: a nin A /\ B by TARSKI:def_3;
reconsider a = 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, XBOOLE_1: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, Def16;
then A /\ B is independent by A9, Th3;
then A11: card (A9 /\ B9) = Rnk (A /\ B) by Th21;
for C being Subset of M st C c= (A \/ B) \ {e} holds
not C is 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, Def16;
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; :: according to MATROID0:def_10 ::_thesis: for B being Subset of M st B is independent & B c= A \/ B & C c= B holds
C = B
let D be Subset of M; ::_thesis: ( D is independent & D c= A \/ B & C c= D implies C = D )
A22: A c= A \/ B by XBOOLE_1:7;
A is dependent by A1, Def16;
then A \/ B is dependent by A22, Th3;
hence ( D is independent & D c= A \/ B & C c= D implies C = D ) by A21, ZFMISC_1:138; ::_thesis: verum
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; ::_thesis: verum
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
let M be finite-degree Matroid; ::_thesis: 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
let A, B, C be Subset of M; ::_thesis: 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
let e be Element of M; ::_thesis: ( A is independent & B is cycle & C is cycle & B c= A \/ {e} & C c= A \/ {e} implies B = C )
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} ; ::_thesis: B = C
now__::_thesis:_not_C_c=_A
assume C c= A ; ::_thesis: contradiction
then C is independent by A1, Th3;
hence contradiction by A3, Def16; ::_thesis: verum
end;
then consider c being set such that
A6: c in C and
A7: c nin A by TARSKI:def_3;
c in {e} by A5, A6, A7, XBOOLE_0:def_3;
then A8: c = e by TARSKI:def_1;
now__::_thesis:_not_B_c=_A
assume B c= A ; ::_thesis: contradiction
then B is independent by A1, Th3;
hence contradiction by A2, Def16; ::_thesis: verum
end;
then consider b being set such that
A9: b in B and
A10: b nin A by TARSKI:def_3;
assume A11: B <> C ; ::_thesis: contradiction
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in A )
assume A14: x in D ; ::_thesis: x in A
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 x in A by A4, A5, A15, XBOOLE_0:def_3; ::_thesis: verum
end;
then D is independent by A1, Th3;
hence contradiction by A12, Def16; ::_thesis: verum
end;