Theorems · Theorem · combinatorics

Matroid.closure_subset_closure_iff_subset_closure

∀ {α : Type u_2} {M : Matroid α} {X Y : Set α},
  autoParam (X ⊆ M.E) Matroid.closure_subset_closure_iff_subset_closure._auto_1 →
    (M.closure X ⊆ M.closure Y ↔ X ⊆ M.closure Y)

Defined in: Mathlib.Combinatorics.Matroid.Closure
Cited by: 3 results in Mathlib
Foundations: Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites7

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
Matroid.Estatement and proof · cited by 550
Matroid.closurestatement · cited by 272
Matroid.subset_closureproof · cited by 23
Matroid.closure_subset_closure_of_subset_closureproof · cited by 9

Cited by3

Results whose statement or proof uses this declaration.

Matroid.IsBasis.subset_closureproof · cited by 15
Matroid.fundCircuit_eq_sInterproof · cited by 3
Matroid.isLoop_iff_closure_eq_loops_and_mem_groundproof · cited by 1