Theorems · Definition · combinatorics
Matroid.fundCocircuit
{α : Type u_1} → Matroid α → α → Set α → Set αThe fundamental cocircuit for B and e:
that is, the unique cocircuit K of M for which K ∩ B = {e}.
Should be used when B is a base and e ∈ B.
Has the junk value {e} if e ∉ B or e ∉ M.E.
- Defined in
- Mathlib.Combinatorics.Matroid.Circuit
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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.Eproof · cited by 550
- Matroid.dualproof · cited by 79
- Matroid.fundCircuitproof · cited by 19
Cited by9
Results whose statement or proof uses this declaration.
- Matroid.mem_fundCocircuitstatement · cited by 3
- Matroid.fundCocircuit_isCocircuitstatement · cited by 2
- Matroid.fundCocircuit_subset_insert_complstatement · cited by 2
- Matroid.fundCocircuit_eq_of_notMem_groundstatement · cited by 1
- Matroid.fundCocircuit_inter_eqstatement · cited by 1
- Matroid.Indep.exists_isCocircuit_inter_eq_memproof · cited by 0
- Matroid.IsNonloop.exists_mem_isCocircuitproof · cited by 0
- Matroid.IsBase.mem_fundCocircuit_iff_mem_fundCircuitstatement and proof · cited by 0
- Matroid.fundCocircuit_eq_of_notMemstatement · cited by 0