Theorems · Theorem · combinatorics

IndepMatroid.mk.inj

∀ {α : Type u_2} {E : Set α} {Indep : Set α → Prop} {indep_empty : Indep ∅}
  {indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I}
  {indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)}
  {indep_maximal : ∀ X ⊆ E, Matroid.ExistsMaximalSubsetProperty Indep X}
  {subset_ground : ∀ (I : Set α), Indep I → I ⊆ E} {E_1 : Set α} {Indep_1 : Set α → Prop} {indep_empty_1 : Indep_1 ∅}
  {indep_subset_1 : ∀ ⦃I J : Set α⦄, Indep_1 J → I ⊆ J → Indep_1 I}
  {indep_aug_1 :
    ∀ ⦃I B : Set α⦄, Indep_1 I → ¬Maximal Indep_1 I → Maximal Indep_1 B → ∃ x ∈ B \ I, Indep_1 (insert x I)}
  {indep_maximal_1 : ∀ X ⊆ E_1, Matroid.ExistsMaximalSubsetProperty Indep_1 X}
  {subset_ground_1 : ∀ (I : Set α), Indep_1 I → I ⊆ E_1},
  { E := E, Indep := Indep, indep_empty := indep_empty, indep_subset := indep_subset, indep_aug := indep_aug,
        indep_maximal := indep_maximal, subset_ground := subset_ground } =
      { E := E_1, Indep := Indep_1, indep_empty := indep_empty_1, indep_subset := indep_subset_1,
        indep_aug := indep_aug_1, indep_maximal := indep_maximal_1, subset_ground := subset_ground_1 } →
    E = E_1 ∧ Indep = Indep_1

Defined in

Mathlib.Combinatorics.Matroid.IndepAxioms

Cited by

1 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms