Theorems · Theorem · combinatorics

IndepMatroid.ofFinset_indep

∀ {α : Type u_1} [inst : DecidableEq α] (E : Set α) (Indep : Finset α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I))
  (subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E) {I : Finset α},
  (IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).Indep ↑I ↔ Indep I

Defined in

Mathlib.Combinatorics.Matroid.IndepAxioms

Cited by

0 results in Mathlib

Foundations

Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEq