Theorems · Theorem · combinatorics
Matroid.closure_sdiff_eq_self
∀ {α : Type u_2} {M : Matroid α} {X Y : Set α}, Y ⊆ M.closure (X \ Y) → M.closure (X \ Y) = M.closure X- Defined in
- Mathlib.Combinatorics.Matroid.Closure
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- LE.le.transproof · cited by 3,151
- Matroidstatement and proof · cited by 1,258
- Set.inter_subset_rightproof · cited by 329
- Matroid.closurestatement and proof · cited by 272
- Set.union_eq_self_of_subset_rightproof · cited by 25
- Set.sdiff_union_interproof · cited by 19
- Matroid.closure_closureproof · cited by 14
- Matroid.closure_union_closure_left_eqproof · cited by 5
Cited by3
Results whose statement or proof uses this declaration.
- Matroid.subset_closure_sdiff_iff_closure_eqproof · cited by 2
- Matroid.closure_sdiff_singleton_eq_closureproof · cited by 1
- Matroid.closure_diff_eq_selfproof · cited by 0