:: 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 Def2 defines independent MATROID0:def 2 :
:: deftheorem Def3 defines subset-closed MATROID0:def 3 :
:: deftheorem defines with_exchange_property MATROID0:def 4 :
theorem Th1: :: MATROID0:1
theorem Th2: :: MATROID0:2
theorem Th3: :: MATROID0:3
theorem Th4: :: MATROID0:4
:: deftheorem Def5 defines finite-membered MATROID0:def 5 :
:: deftheorem Def6 defines finite-membered MATROID0:def 6 :
:: deftheorem Def7 defines finite-degree MATROID0:def 7 :
theorem Th5: :: MATROID0:5
theorem :: MATROID0:6
theorem :: MATROID0:7
:: deftheorem Def8 defines ProdMatroid MATROID0:def 8 :
theorem Th8: :: MATROID0:8
theorem Th9: :: MATROID0:9
theorem Th10: :: MATROID0:10
:: deftheorem Def9 defines LinearlyIndependentSubsets MATROID0:def 9 :
theorem Th11: :: MATROID0:11
theorem :: MATROID0:12
theorem Th13: :: MATROID0:13
:: deftheorem Def10 defines is_maximal_independent_in MATROID0:def 10 :
theorem Th14: :: MATROID0:14
theorem :: MATROID0:15
theorem Th16: :: MATROID0:16
:: deftheorem defines Rnk MATROID0:def 11 :
theorem Th17: :: MATROID0:17
theorem Th18: :: MATROID0:18
theorem Th19: :: MATROID0:19
theorem Th20: :: MATROID0:20
theorem Th21: :: MATROID0:21
:: deftheorem defines Rnk MATROID0:def 12 :
:: deftheorem Def13 defines Basis MATROID0:def 13 :
theorem :: MATROID0:22
theorem :: MATROID0:23
theorem Th24: :: MATROID0:24
theorem Th25: :: MATROID0:25
theorem Th26: :: MATROID0:26
theorem :: MATROID0:27
:: deftheorem Def14 defines is_dependent_on MATROID0:def 14 :
theorem Th28: :: MATROID0:28
theorem Th29: :: MATROID0:29
:: deftheorem defines Span MATROID0:def 15 :
theorem Th30: :: MATROID0:30
theorem Th31: :: MATROID0:31
theorem :: MATROID0:32
theorem Th33: :: MATROID0:33
theorem Th34: :: MATROID0:34
theorem :: MATROID0:35
theorem :: MATROID0:36
:: deftheorem Def16 defines cycle MATROID0:def 16 :
theorem Th37: :: MATROID0:37
theorem Th38: :: MATROID0:38
theorem Th39: :: MATROID0:39
theorem :: MATROID0:40
theorem Th41: :: MATROID0:41
theorem Th42: :: MATROID0:42
theorem Th43: :: MATROID0:43
theorem :: MATROID0:44