Theorems · Definition · combinatorics

IndepMatroid.mk.noConfusion

{α : Type u_2} →
  {P : Sort u} →
    {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' : 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 := 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', Indep := Indep', indep_empty := indep_empty',
                                      indep_subset := indep_subset', indep_aug := indep_aug',
                                      indep_maximal := indep_maximal', subset_ground := subset_ground' } →
                                  (E ≍ E' → Indep ≍ Indep' → P) → P

Defined in

Mathlib.Combinatorics.Matroid.IndepAxioms

Cited by

1 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms