:: Introduction to Matroids
:: by Grzegorz Bancerek and Yasunari Shidama
::
:: Received July 30, 2008
:: Copyright (c) 2008 Association of Mizar Users
:: deftheorem defines the_family_of MATROID0:def 1 :
:: deftheorem Def8 defines independent MATROID0:def 2 :
:: deftheorem Def2 defines subset-closed MATROID0:def 3 :
:: deftheorem defines with_exchange_property MATROID0:def 4 :
theorem Th2: :: MATROID0:1
theorem M0: :: MATROID0:2
theorem M1: :: MATROID0:3
theorem M2: :: MATROID0:4
:: deftheorem Def6 defines finite-membered MATROID0:def 5 :
:: deftheorem Def7 defines finite-membered MATROID0:def 6 :
:: deftheorem Def9 defines finite-degree MATROID0:def 7 :
theorem Th11: :: MATROID0:5
theorem :: MATROID0:6
theorem :: MATROID0:7
:: deftheorem Def4 defines ProdMatroid MATROID0:def 8 :
theorem Th10: :: MATROID0:8
theorem Th14: :: MATROID0:9
theorem Th13: :: MATROID0:10
:: deftheorem Def5 defines LinearlyIndependentSubsets MATROID0:def 9 :
theorem Th21: :: MATROID0:11
theorem :: MATROID0:12
theorem ThI1: :: MATROID0:13
:: deftheorem MAXIMAL defines is_maximal_independent_in MATROID0:def 10 :
theorem Th: :: MATROID0:14
theorem :: MATROID0:15
theorem M3: :: MATROID0:16
:: deftheorem defines Rnk MATROID0:def 11 :
theorem ThR0: :: MATROID0:17
theorem ThR1: :: MATROID0:18
theorem ThR2: :: MATROID0:19
theorem ThR3: :: MATROID0:20
theorem ThR4: :: MATROID0:21
:: deftheorem defines Rnk MATROID0:def 12 :
:: deftheorem BASIS defines Basis MATROID0:def 13 :
theorem :: MATROID0:22
theorem :: MATROID0:23
theorem R2: :: MATROID0:24
theorem R3: :: MATROID0:25
theorem R4: :: MATROID0:26
theorem :: MATROID0:27
:: deftheorem DF defines is_dependent_on MATROID0:def 14 :
theorem ThD1: :: MATROID0:28
theorem ThD2: :: MATROID0:29
:: deftheorem defines Span MATROID0:def 15 :
theorem SPAN: :: MATROID0:30
theorem S1: :: MATROID0:31
theorem :: MATROID0:32
theorem S0: :: MATROID0:33
theorem Sd: :: MATROID0:34
theorem :: MATROID0:35
theorem :: MATROID0:36
:: deftheorem CYCLE defines cycle MATROID0:def 16 :
theorem LemC: :: MATROID0:37
theorem C5: :: MATROID0:38
theorem C4: :: MATROID0:39
theorem :: MATROID0:40
theorem C1: :: MATROID0:41
theorem C3: :: MATROID0:42
theorem C2: :: MATROID0:43
theorem :: MATROID0:44