namespace http://mathhub.info/MitM/core/collections ❚
import base http://mathhub.info/MitM/Foundation ❚

theory Matroids : base:?Logic =
	include ?Properties ❙
	include typedsets?FiniteCardinality ❙
	include arithmetics?NaturalArithmetics ❙

	theory matroid_theory : base:?Logic > X : type ❘ =
		include typedsets?SetCollection/setColl_theory (X) ❙
		
		axiom_finite : {s : set X} ⊦ s ∈ coll ⟶ ⊦ s finite ❙
		axiom_empty : ⊦ prop_emptyInColl coll ❙
		axiom_subset : ⊦ prop_subsetClosed coll ❙
		axiom_augmentation : ⊦ ∀ [A] ∀ [B] A ∈ coll ∧ B ∈ coll ∧ | B | ≤ | A | 
				⇒ ∃ [x] x ∈ (A \ B) ∧ (B ∪ (single x)) ∈ coll ❙
	❚
❚