:: Introduction to Matroids :: by Grzegorz Bancerek and Yasunari Shidama :: :: Received July 30, 2008 :: Copyright (c) 2008-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, TARSKI, PRE_TOPC, SUBSET_1, BVFUNC_2, RCOMP_1, SETFAM_1, CLASSES1, FINSET_1, CARD_1, ARYTM_3, XBOOLE_0, STRUCT_0, ZFMISC_1, NAT_1, XXREAL_0, TAXONOM2, AOFA_000, ORDERS_1, FUNCT_1, RELAT_1, NATTRA_1, EQREL_1, VECTSP_1, RLVECT_3, CARD_3, RLVECT_2, SUPINF_2, REALSET1, ARYTM_1, RLVECT_5, JORDAN13, MATROID0; notations TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, SETFAM_1, FINSET_1, ORDINAL1, NUMBERS, FUNCT_1, RELSET_1, FUNCT_2, EQREL_1, ORDERS_1, TAXONOM2, XCMPLX_0, XXREAL_0, NAT_1, CARD_1, CLASSES1, AOFA_000, STRUCT_0, RLVECT_1, VECTSP_1, VECTSP_6, VECTSP_7, PRE_TOPC, TDLAT_3, MATRLIN, PENCIL_1, RANKNULL; constructors COH_SP, TDLAT_3, TAXONOM2, RANKNULL, VECTSP_7, PENCIL_1, REALSET1, RELSET_1; registrations FINSET_1, CARD_1, RELSET_1, STRUCT_0, SUBSET_1, PENCIL_1, TDLAT_3, SETFAM_1, EQREL_1, MATRLIN, XREAL_0, ALGSTR_0, BINOM, RLVECT_1, VECTSP_1, VECTSP_7, ORDINAL1; requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL; begin :: Definition by Independent Sets notation let x,y be set; antonym x c/= y for x c= y; end; definition mode SubsetFamilyStr is TopStruct; end; notation let M be SubsetFamilyStr; let A be Subset of M; synonym A is independent for A is open; antonym A is dependent for A is open; end; definition let M be SubsetFamilyStr; func the_family_of M -> Subset-Family of M equals :: MATROID0:def 1 the topology of M; end; definition let M be SubsetFamilyStr; let A be Subset of M; redefine attr A is independent means :: MATROID0:def 2 A in the_family_of M; end; definition let M be SubsetFamilyStr; attr M is subset-closed means :: MATROID0:def 3 the_family_of M is subset-closed; attr M is with_exchange_property means :: MATROID0:def 4 for A,B being finite Subset of M st A in the_family_of M & B in the_family_of M & card B = (card A) + 1 ex e being Element of M st e in B \ A & A \/ {e} in the_family_of M; end; registration cluster strict non empty non void finite subset-closed with_exchange_property for SubsetFamilyStr; end; registration let M be non void SubsetFamilyStr; cluster independent for Subset of M; end; registration let M be subset-closed SubsetFamilyStr; cluster the_family_of M -> subset-closed; end; theorem :: MATROID0:1 for M being non void subset-closed SubsetFamilyStr for A being independent Subset of M for B being set st B c= A holds B is independent Subset of M; registration let M be non void subset-closed SubsetFamilyStr; cluster finite independent for Subset of M; end; definition mode Matroid is non empty non void subset-closed with_exchange_property SubsetFamilyStr; end; theorem :: MATROID0:2 for M being subset-closed SubsetFamilyStr holds M is non void iff {} in the_family_of M; registration let M be non void subset-closed SubsetFamilyStr; cluster empty -> independent for Subset of M; end; theorem :: MATROID0:3 for M being non void SubsetFamilyStr holds M is subset-closed iff for A,B being Subset of M st A is independent & B c= A holds B is independent ; registration let M be non void subset-closed SubsetFamilyStr; let A be independent Subset of M; let B be set; cluster A/\B -> independent for Subset of M; cluster B/\A -> independent for Subset of M; cluster A\B -> independent for Subset of M; end; theorem :: MATROID0:4 for M being non void non empty SubsetFamilyStr holds M is with_exchange_property iff for A,B being finite Subset of M st A is independent & B is independent & card B = (card A) + 1 ex e being Element of M st e in B \ A & A \/ {e} is independent; definition ::$CD let M be SubsetFamilyStr; attr M is finite-membered means :: MATROID0:def 6 the_family_of M is finite-membered; end; definition let M be SubsetFamilyStr; attr M is finite-degree means :: MATROID0:def 7 M is finite-membered & ex n being Nat st for A being finite Subset of M st A is independent holds card A <= n; end; registration cluster finite-degree -> finite-membered for SubsetFamilyStr; cluster finite -> finite-degree for SubsetFamilyStr; end; begin :: Examples registration cluster mutually-disjoint non empty with_non-empty_elements for set; end; theorem :: MATROID0:5 for A,B being finite set st card A < card B ex x being set st x in B \ A; theorem :: MATROID0:6 for P being mutually-disjoint with_non-empty_elements non empty set for f being Choice_Function of P holds f is one-to-one; registration cluster -> non void subset-closed with_exchange_property for discrete SubsetFamilyStr; end; theorem :: MATROID0:7 for T being non empty discrete TopStruct holds T is Matroid; definition let P be set; func ProdMatroid P -> strict SubsetFamilyStr means :: MATROID0:def 8 the carrier of it = union P & the_family_of it = {A where A is Subset of union P: for D being set st D in P ex d being set st A /\ D c= {d}}; end; registration let P be non empty with_non-empty_elements set; cluster ProdMatroid P -> non empty; end; theorem :: MATROID0:8 for P being set for A being Subset of ProdMatroid P holds A is independent iff for D being Element of P ex d being Element of D st A /\ D c= { d}; registration let P be set; cluster ProdMatroid P -> non void subset-closed; end; theorem :: MATROID0:9 for P being mutually-disjoint set for x being Subset of ProdMatroid P ex f being Function of x,P st for a being object st a in x holds a in f.a; theorem :: MATROID0:10 for P being mutually-disjoint set for x being Subset of ProdMatroid P for f being Function of x,P st for a being object st a in x holds a in f.a holds x is independent iff f is one-to-one; registration let P be mutually-disjoint set; cluster ProdMatroid P -> with_exchange_property; end; registration let X be finite set; let P be Subset of bool X; cluster ProdMatroid P -> finite; end; registration let X be set; cluster -> mutually-disjoint for a_partition of X; end; registration cluster finite strict for Matroid; end; registration let M be finite-membered non void SubsetFamilyStr; cluster -> finite for independent Subset of M; end; definition let F be Field; let V be VectSp of F; func LinearlyIndependentSubsets V -> strict SubsetFamilyStr means :: MATROID0:def 9 the carrier of it = the carrier of V & the_family_of it = {A where A is Subset of V : A is linearly-independent}; end; registration let F be Field; let V be VectSp of F; cluster LinearlyIndependentSubsets V -> non empty non void subset-closed; end; theorem :: MATROID0:11 for F being Field, V being VectSp of F for A being Subset of LinearlyIndependentSubsets V holds A is independent iff A is linearly-independent Subset of V; theorem :: MATROID0:12 for F being Field for V being VectSp of F for A, B being finite Subset of V st B c= A for v being Vector of V st v in Lin(A) & not v in Lin(B) holds ex w being Vector of V st w in A\B & w in Lin(A \ {w} \/ {v}); theorem :: MATROID0:13 for F being Field, V being VectSp of F for A being Subset of V st A is linearly-independent for a being Element of V st a nin the carrier of Lin A holds A\/{a} is linearly-independent; registration let F be Field; let V be VectSp of F; cluster LinearlyIndependentSubsets V -> with_exchange_property; end; registration let F be Field; let V be finite-dimensional VectSp of F; cluster LinearlyIndependentSubsets V -> finite-membered; end; begin :: Maximal Independent Subsets, Ranks, and Basis definition let M be SubsetFamilyStr; let A,C be Subset of M; pred A is_maximal_independent_in C means :: MATROID0:def 10 A is independent & A c= C & for B being Subset of M st B is independent & B c= C & A c= B holds A = B; end; theorem :: MATROID0:14 for M being non void finite-degree SubsetFamilyStr for C,A being Subset of M st A c= C & A is independent ex B being independent Subset of M st A c= B & B is_maximal_independent_in C; theorem :: MATROID0:15 for M being non void finite-degree subset-closed SubsetFamilyStr for C being Subset of M ex A being independent Subset of M st A is_maximal_independent_in C; theorem :: MATROID0:16 for M being non empty non void subset-closed finite-degree SubsetFamilyStr holds M is Matroid iff for C being Subset of M, A,B being independent Subset of M st A is_maximal_independent_in C & B is_maximal_independent_in C holds card A = card B; definition let M be finite-degree Matroid; let C be Subset of M; func Rnk C -> Nat equals :: MATROID0:def 11 union {card A where A is independent Subset of M: A c= C}; end; theorem :: MATROID0:17 for M being finite-degree Matroid for C being Subset of M for A being independent Subset of M st A c= C holds card A <= Rnk C; theorem :: MATROID0:18 for M being finite-degree Matroid for C being Subset of M ex A being independent Subset of M st A c= C & card A = Rnk C; theorem :: MATROID0:19 for M being finite-degree Matroid for C being Subset of M for A being independent Subset of M holds A is_maximal_independent_in C iff A c= C & card A = Rnk C; theorem :: MATROID0:20 for M being finite-degree Matroid for C being finite Subset of M holds Rnk C <= card C; theorem :: MATROID0:21 for M being finite-degree Matroid for C being finite Subset of M holds C is independent iff card C = Rnk C; definition let M be finite-degree Matroid; func Rnk M -> Nat equals :: MATROID0:def 12 Rnk [#]M; end; definition let M be non void finite-degree SubsetFamilyStr; mode Basis of M -> independent Subset of M means :: MATROID0:def 13 it is_maximal_independent_in [#]M; end; theorem :: MATROID0:22 for M being finite-degree Matroid for B1,B2 being Basis of M holds card B1 = card B2; theorem :: MATROID0:23 for M being finite-degree Matroid for A being independent Subset of M ex B being Basis of M st A c= B; reserve M for finite-degree Matroid, A,B,C for Subset of M, e,f for Element of M; theorem :: MATROID0:24 A c= B implies Rnk A <= Rnk B; theorem :: MATROID0:25 Rnk (A\/B) + Rnk (A/\B) <= Rnk A + Rnk B; theorem :: MATROID0:26 Rnk A <= Rnk (A\/B) & Rnk (A \/ {e}) <= Rnk A + 1; theorem :: MATROID0:27 Rnk (A\/{e}) = Rnk (A\/{f}) & Rnk (A\/{f}) = Rnk A implies Rnk (A \/ { e,f}) = Rnk A; begin :: Dependence from a Set, Spans, and Cycles definition let M be finite-degree Matroid; let e be Element of M; let A be Subset of M; pred e is_dependent_on A means :: MATROID0:def 14 Rnk (A \/ {e}) = Rnk A; end; theorem :: MATROID0:28 e in A implies e is_dependent_on A; theorem :: MATROID0:29 A c= B & e is_dependent_on A implies e is_dependent_on B; definition let M be finite-degree Matroid; let A be Subset of M; func Span A -> Subset of M equals :: MATROID0:def 15 {e where e is Element of M: e is_dependent_on A}; end; theorem :: MATROID0:30 e in Span A iff Rnk (A \/ {e}) = Rnk A; theorem :: MATROID0:31 A c= Span A; theorem :: MATROID0:32 A c= B implies Span A c= Span B; theorem :: MATROID0:33 Rnk Span A = Rnk A; theorem :: MATROID0:34 e is_dependent_on Span A implies e is_dependent_on A; theorem :: MATROID0:35 Span Span A = Span A; theorem :: MATROID0:36 f nin Span A & f in Span (A \/ {e}) implies e in Span (A \/ {f}); definition let M be SubsetFamilyStr; let A be Subset of M; attr A is cycle means :: MATROID0:def 16 A is dependent & for e being Element of M st e in A holds A \ {e} is independent; end; theorem :: MATROID0:37 A is cycle implies A is non empty finite; registration let M; cluster cycle -> non empty finite for Subset of M; end; theorem :: MATROID0:38 A is cycle iff A is non empty & for e st e in A holds A\{e} is_maximal_independent_in A; theorem :: MATROID0:39 A is cycle implies Rnk A + 1 = card A; theorem :: MATROID0:40 A is cycle & e in A implies e is_dependent_on A\{e}; theorem :: MATROID0:41 A is cycle & B is cycle & A c= B implies A = B; theorem :: MATROID0:42 (for B st B c= A holds B is not cycle) implies A is independent; theorem :: MATROID0:43 A is cycle & B is cycle & A <> B & e in A /\ B implies ex C st C is cycle & C c= (A \/ B) \ {e}; theorem :: MATROID0:44 A is independent & B is cycle & C is cycle & B c= A\/{e} & C c= A\/{e} implies B = C;