Mathlib Map

Theorems · Theorem · combinatorics

Matroid.IsFlat.subset_ground

∀ {α : Type u_2} {M : Matroid α} {F : Set α}, M.IsFlat F → F ⊆ M.E
Defined in
Mathlib.Combinatorics.Matroid.Closure
Cited by
5 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Matroid.Indep.closure_eq_setOfPred_isBasis_insert · cited by 6Indep.closure_eq_setOfPre…Matroid.IsFlat.closure · cited by 3IsFlat.closureMatroid.IsFlat.iInter · cited by 1IsFlat.iInterMatroid.closure_eq_subtypeClosure · cited by 1Matroid.closure_eq_subtyp…Matroid.isFlat_iff_isClosed · cited by 0Matroid.isFlat_iff_isClos…Set · cited by 53352SetMatroid · cited by 1258MatroidMatroid.E · cited by 550Matroid.EMatroid.IsFlat · cited by 27Matroid.IsFlatIsFlat.subset_groundCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement and proof · cited by 53,352
  • Matroidstatement and proof · cited by 1,258
  • Matroid.Estatement · cited by 550
  • Matroid.IsFlatstatement and proof · cited by 27

Cited by5

Results whose statement or proof uses this declaration.