Mathlib Map

Theorems · Inductive type · combinatorics

Matroid.IsFlat

{α : Type u_2} → Matroid α → Set α → Prop

A flat is a maximal set having a given basis

Defined in
Mathlib.Combinatorics.Matroid.Closure
Cited by
27 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Matroid.closure · cited by 272Matroid.closureMatroid.closure_subset_closure · cited by 24Matroid.closure_subset_cl…Matroid.subset_closure · cited by 23Matroid.subset_closureMatroid.closure_inter_ground · cited by 22Matroid.closure_inter_gro…Matroid.closure_closure · cited by 14Matroid.closure_closureMatroid.Indep.closure_eq_setOfPred_isBasis_insert · cited by 6Indep.closure_eq_setOfPre…Matroid.IsFlat.subset_ground · cited by 5IsFlat.subset_groundMatroid.closure_iUnion_closure_eq_closure_iUnion · cited by 4Matroid.closure_iUnion_cl…Matroid.subtypeClosure · cited by 4Matroid.subtypeClosureMatroid.IsFlat.closure · cited by 3IsFlat.closureMatroid.closure_def' · cited by 3Matroid.closure_def'Matroid.ground_isFlat · cited by 2Matroid.ground_isFlatMatroid.IsFlat.subset_of_isBasis_of_isBasis · cited by 2IsFlat.subset_of_isBasis_…Matroid.inter_ground_subset_closure · cited by 2Matroid.inter_ground_subs…Matroid.IsFlat.casesOn · cited by 1IsFlat.casesOnSet · cited by 53352SetMatroid · cited by 1258MatroidMatroid.IsFlatCITED BYCITES

Cites2

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

  • Setstatement · cited by 53,352
  • Matroidstatement · cited by 1,258

Cited by31

Results whose statement or proof uses this declaration.