Documentation

Mathlib.Data.Matroid.Loop

Matroid loops and coloops #

Loops #

A 'loop' of a matroid M is an element e satisfying one of the following equivalent conditions:

e ∈ M.closure ∅;
{e} is dependent in M;
{e} is a circuit of M;
no base of M contains e.

In many mathematical contexts, loops can be thought of as 'trivial' or 'zero' elements; For linearly representable matroids, they correspond to the zero vector, and for graphic matroids, they correspond to edges incident with just one vertex (aka 'loops'). As trivial as they are, loops can be created from matroids with no loops by taking minors or duals, so in many contexts it is unreasonable to simply forbid loops from appearing. For M : Matroid α, this file defines a set Matroid.loops M : Set α, as well as predicates Matroid.IsLoop M : α → Prop and Matroid.IsNonloop M : α → Prop, and provides API for interacting with them.

Coloops #

The dual notion of a loop is a 'coloop'. Geometrically, these can be thought of elements that are skew to the remainder of the matroid. Coloops in graphic matroids are 'bridge' edges of the graph, and coloops in linearly representable matroids are vectors not spanned by the other vectors in the matroid. Coloops also have many equivalent definitions in abstract matroid language; a coloop is an element of M.E if any of the following equivalent conditions holds :

e is a loop of M✶;
{e} is a cocircuit of M;
e is in no circuit of M;
e is in every base of M;
for all X ⊆ M.E, e ∈ X ↔ e ∈ M.closure X,
M.E \ {e} is nonspanning.

Main Declarations #

For M : Matroid α:

M.loops is the set M.closure ∅.
M.IsLoop e means that e : α is a loop of M, defined as the statement e ∈ M.loops.
M.isLoop_tfae gives a number of properties that are equivalent to IsLoop.
M.IsNonloop e means that e ∈ M.E, but e is not a loop of M.
M.IsColoop e means that e is a loop of M✶.
M.coloops is the set of coloops of M✶.
M.isColoop_tfae gives a number of properties that are equivalent to IsColoop.
M.Loopless is a typeclass meaning M has no loops.
M.removeLoops is the matroid obtained from M by restricting to its set of nonloop elements.

def Matroid.loops {α : Type u_1} (M : Matroid α) :

Set α

Matroid.loops M is the closure of the empty set.

Equations

Instances For

theorem Matroid.loops_subset_ground {α : Type u_1} (M : Matroid α) :

M.loops ⊆ M.E

def Matroid.IsLoop {α : Type u_1} (M : Matroid α) (e : α) :

A 'loop' is a member of the closure of the empty set

Equations

Instances For

theorem Matroid.isLoop_iff {α : Type u_1} {M : Matroid α} {e : α} :

M.IsLoop e ↔ e ∈ M.loops

theorem Matroid.closure_empty {α : Type u_1} (M : Matroid α) :

M.closure ∅ = M.loops

theorem Matroid.IsLoop.mem_ground {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsLoop e) :

e ∈ M.E

theorem Matroid.isLoop_tfae {α : Type u_1} (M : Matroid α) (e : α) :

[M.IsLoop e, e ∈ M.closure ∅, M.IsCircuit {e}, M.Dep {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B].TFAE

@[simp]

theorem Matroid.singleton_dep {α : Type u_1} {M : Matroid α} {e : α} :

M.Dep {e} ↔ M.IsLoop e

theorem Matroid.IsLoop.dep {α : Type u_1} {M : Matroid α} {e : α} :

M.IsLoop e → M.Dep {e}

Alias of the reverse direction of Matroid.singleton_dep.

theorem Matroid.singleton_not_indep {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :

¬M.Indep {e} ↔ M.IsLoop e

@[simp]

theorem Matroid.singleton_isCircuit {α : Type u_1} {M : Matroid α} {e : α} :

M.IsCircuit {e} ↔ M.IsLoop e

theorem Matroid.IsLoop.isCircuit {α : Type u_1} {M : Matroid α} {e : α} :

M.IsLoop e → M.IsCircuit {e}

Alias of the reverse direction of Matroid.singleton_isCircuit.

theorem Matroid.isLoop_iff_forall_mem_compl_isBase {α : Type u_1} {M : Matroid α} {e : α} :

M.IsLoop e ↔ ∀ (B : Set α), M.IsBase B → e ∈ M.E \ B

theorem Matroid.isLoop_iff_forall_notMem_isBase {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :

M.IsLoop e ↔ ∀ (B : Set α), M.IsBase B → e ∉ B

@[deprecated Matroid.isLoop_iff_forall_notMem_isBase (since := "2025-05-23")]

theorem Matroid.isLoop_iff_forall_not_mem_isBase {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :

M.IsLoop e ↔ ∀ (B : Set α), M.IsBase B → e ∉ B

Alias of Matroid.isLoop_iff_forall_notMem_isBase.

theorem Matroid.IsLoop.mem_closure {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsLoop e) (X : Set α) :

e ∈ M.closure X

theorem Matroid.IsLoop.mem_of_isFlat {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsLoop e) {F : Set α} (hF : M.IsFlat F) :

e ∈ F

theorem Matroid.IsFlat.loops_subset {α : Type u_1} {M : Matroid α} {F : Set α} (hF : M.IsFlat F) :

theorem Matroid.IsLoop.dep_of_mem {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (he : M.IsLoop e) (h : e ∈ X) (hXE : X ⊆ M.E := by aesop_mat) :

M.Dep X

theorem Matroid.IsLoop.not_indep_of_mem {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (he : M.IsLoop e) (h : e ∈ X) :

theorem Matroid.IsLoop.notMem_of_indep {α : Type u_1} {M : Matroid α} {e : α} {I : Set α} (he : M.IsLoop e) (hI : M.Indep I) :

e ∉ I

@[deprecated Matroid.IsLoop.notMem_of_indep (since := "2025-05-23")]

theorem Matroid.IsLoop.not_mem_of_indep {α : Type u_1} {M : Matroid α} {e : α} {I : Set α} (he : M.IsLoop e) (hI : M.Indep I) :

e ∉ I

Alias of Matroid.IsLoop.notMem_of_indep.

theorem Matroid.IsLoop.eq_of_isCircuit_mem {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} (he : M.IsLoop e) (hC : M.IsCircuit C) (h : e ∈ C) :

C = {e}

theorem Matroid.Indep.disjoint_loops {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) :

Disjoint I M.loops

theorem Matroid.Indep.eq_empty_of_subset_loops {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (h : I ⊆ M.loops) :

@[simp]

theorem Matroid.isBasis_loops_iff {α : Type u_1} {M : Matroid α} {I : Set α} :

M.IsBasis I M.loops ↔ I = ∅

theorem Matroid.closure_eq_loops_of_subset {α : Type u_1} {M : Matroid α} {X : Set α} (h : X ⊆ M.loops) :

M.closure X = M.loops

theorem Matroid.isBasis_iff_empty_of_subset_loops {α : Type u_1} {M : Matroid α} {X I : Set α} (hX : X ⊆ M.loops) :

M.IsBasis I X ↔ I = ∅

theorem Matroid.IsLoop.closure {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsLoop e) :

M.closure {e} = M.loops

theorem Matroid.isLoop_iff_closure_eq_loops_and_mem_ground {α : Type u_1} {M : Matroid α} {e : α} :

M.IsLoop e ↔ M.closure {e} = M.loops ∧ e ∈ M.E

theorem Matroid.isLoop_iff_closure_eq_loops {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :

M.IsLoop e ↔ M.closure {e} = M.loops

@[simp]

theorem Matroid.closure_loops {α : Type u_1} (M : Matroid α) :

M.closure M.loops = M.loops

@[simp]

theorem Matroid.closure_union_loops_eq {α : Type u_1} (M : Matroid α) (X : Set α) :

M.closure (X ∪ M.loops) = M.closure X

@[simp]

theorem Matroid.closure_loops_union_eq {α : Type u_1} (M : Matroid α) (X : Set α) :

M.closure (M.loops ∪ X) = M.closure X

@[simp]

theorem Matroid.closure_diff_loops_eq {α : Type u_1} (M : Matroid α) (X : Set α) :

M.closure (X \ M.loops) = M.closure X

theorem Matroid.restrict_loops_eq' {α : Type u_1} (M : Matroid α) (R : Set α) :

(M.restrict R).loops = M.loops ∩ R ∪ R \ M.E

A version of restrict_loops_eq without the hypothesis that R ⊆ M.E

theorem Matroid.restrict_loops_eq {α : Type u_1} {M : Matroid α} {R : Set α} (hR : R ⊆ M.E) :

(M.restrict R).loops = M.loops ∩ R

@[simp]

theorem Matroid.restrict_isLoop_iff {α : Type u_1} {M : Matroid α} {e : α} {R : Set α} :

(M.restrict R).IsLoop e ↔ e ∈ R ∧ (M.IsLoop e ∨ e ∉ M.E)

theorem Matroid.IsRestriction.isLoop_iff {α : Type u_1} {M N : Matroid α} {e : α} (hNM : N.IsRestriction M) :

N.IsLoop e ↔ e ∈ N.E ∧ M.IsLoop e

theorem Matroid.IsLoop.of_isRestriction {α : Type u_1} {M N : Matroid α} {e : α} (he : N.IsLoop e) (hNM : N.IsRestriction M) :

theorem Matroid.IsLoop.isLoop_isRestriction {α : Type u_1} {M N : Matroid α} {e : α} (he : M.IsLoop e) (hNM : N.IsRestriction M) (heN : e ∈ N.E) :

@[simp]

theorem Matroid.map_loops {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : α → β} {hf : Set.InjOn f M.E} :

(M.map f hf).loops = f '' M.loops

@[simp]

theorem Matroid.map_isLoop_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {e : α} {f : α → β} {hf : Set.InjOn f M.E} (he : e ∈ M.E := by aesop_mat) :

(M.map f hf).IsLoop (f e) ↔ M.IsLoop e

@[simp]

theorem Matroid.mapEmbedding_isLoop_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {e : α} {f : α ↪ β} :

(M.mapEmbedding f).IsLoop (f e) ↔ M.IsLoop e

@[simp]

theorem Matroid.comap_loops {α : Type u_1} {β : Type u_2} {M : Matroid β} {f : α → β} :

(M.comap f).loops = f ⁻¹' M.loops

@[simp]

theorem Matroid.comap_isLoop_iff {α : Type u_1} {β : Type u_2} {e : α} {M : Matroid β} {f : α → β} :

(M.comap f).IsLoop e ↔ M.IsLoop (f e)

@[simp]

theorem Matroid.loopyOn_isLoop_iff {α : Type u_1} {e : α} {E : Set α} :

(loopyOn E).IsLoop e ↔ e ∈ E

theorem Matroid.eq_loopyOn_iff_loops {α : Type u_1} {M : Matroid α} {E : Set α} :

M = loopyOn E ↔ M.loops = E ∧ M.E = E

theorem Matroid.restrict_subset_loops_eq {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.loops) :

M.restrict X = loopyOn X

@[simp]

theorem Matroid.freeOn_not_isLoop {α : Type u_1} (E : Set α) (e : α) :

¬(freeOn E).IsLoop e

@[simp]

theorem Matroid.uniqueBaseOn_isLoop_iff {α : Type u_1} {e : α} {I E : Set α} :

(uniqueBaseOn I E).IsLoop e ↔ e ∈ E \ I

theorem Matroid.eq_loopyOn_iff_loops_eq {α : Type u_1} {M : Matroid α} {E : Set α} :

M = loopyOn E ↔ M.loops = E ∧ M.E = E

structure Matroid.IsNonloop {α : Type u_1} (M : Matroid α) (e : α) :

M.IsNonloop e means that e is an element of M.E but not a loop of M.

not_isLoop : ¬M.IsLoop e
mem_ground : e ∈ M.E

Instances For

theorem Matroid.isNonloop_iff {α : Type u_1} (M : Matroid α) (e : α) :

M.IsNonloop e ↔ ¬M.IsLoop e ∧ e ∈ M.E

theorem Matroid.IsLoop.not_isNonloop {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsLoop e) :

¬M.IsNonloop e

theorem Matroid.compl_loops_eq {α : Type u_1} (M : Matroid α) :

M.E \ M.loops = {e : α | M.IsNonloop e}

theorem Matroid.isNonloop_of_not_isLoop {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) (h : ¬M.IsLoop e) :

theorem Matroid.isLoop_of_not_isNonloop {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) (h : ¬M.IsNonloop e) :

@[simp]

theorem Matroid.not_isLoop_iff {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :

¬M.IsLoop e ↔ M.IsNonloop e

@[simp]

theorem Matroid.not_isNonloop_iff {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :

¬M.IsNonloop e ↔ M.IsLoop e

theorem Matroid.isNonloop_iff_mem_compl_loops {α : Type u_1} {M : Matroid α} {e : α} :

M.IsNonloop e ↔ e ∈ M.E \ M.loops

theorem Matroid.setOf_isNonloop_eq {α : Type u_1} (M : Matroid α) :

{e : α | M.IsNonloop e} = M.E \ M.loops

theorem Matroid.not_isNonloop_iff_closure {α : Type u_1} {M : Matroid α} {e : α} :

¬M.IsNonloop e ↔ M.closure {e} = M.loops

theorem Matroid.isLoop_or_isNonloop {α : Type u_1} (M : Matroid α) (e : α) (he : e ∈ M.E := by aesop_mat) :

M.IsLoop e ∨ M.IsNonloop e

@[simp]

theorem Matroid.indep_singleton {α : Type u_1} {M : Matroid α} {e : α} :

M.Indep {e} ↔ M.IsNonloop e

theorem Matroid.IsNonloop.indep {α : Type u_1} {M : Matroid α} {e : α} :

M.IsNonloop e → M.Indep {e}

Alias of the reverse direction of Matroid.indep_singleton.

theorem Matroid.Indep.isNonloop {α : Type u_1} {M : Matroid α} {e : α} :

M.Indep {e} → M.IsNonloop e

Alias of the forward direction of Matroid.indep_singleton.

theorem Matroid.Indep.isNonloop_of_mem {α : Type u_1} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) (h : e ∈ I) :

theorem Matroid.IsNonloop.exists_mem_isBase {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsNonloop e) :

∃ (B : Set α), M.IsBase B ∧ e ∈ B

theorem Matroid.IsCocircuit.isNonloop_of_mem {α : Type u_1} {M : Matroid α} {e : α} {K : Set α} (hK : M.IsCocircuit K) (he : e ∈ K) :

theorem Matroid.IsCircuit.isNonloop_of_mem {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} (hC : M.IsCircuit C) (hC' : C.Nontrivial) (he : e ∈ C) :

theorem Matroid.IsCircuit.isNonloop_of_mem_of_one_lt_card {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} (hC : M.IsCircuit C) (h : 1 < C.encard) (he : e ∈ C) :

theorem Matroid.isNonloop_of_notMem_closure {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (h : e ∉ M.closure X) (he : e ∈ M.E := by aesop_mat) :

@[deprecated Matroid.isNonloop_of_notMem_closure (since := "2025-05-23")]

theorem Matroid.isNonloop_of_not_mem_closure {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (h : e ∉ M.closure X) (he : e ∈ M.E := by aesop_mat) :

Alias of Matroid.isNonloop_of_notMem_closure.

theorem Matroid.isNonloop_iff_notMem_loops {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :

M.IsNonloop e ↔ e ∉ M.loops

@[deprecated Matroid.isNonloop_iff_notMem_loops (since := "2025-05-23")]

theorem Matroid.isNonloop_iff_not_mem_loops {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :

M.IsNonloop e ↔ e ∉ M.loops

Alias of Matroid.isNonloop_iff_notMem_loops.

theorem Matroid.IsNonloop.mem_closure_singleton {α : Type u_1} {M : Matroid α} {e f : α} (he : M.IsNonloop e) (hef : e ∈ M.closure {f}) :

f ∈ M.closure {e}

theorem Matroid.IsNonloop.mem_closure_comm {α : Type u_1} {M : Matroid α} {e f : α} (he : M.IsNonloop e) (hf : M.IsNonloop f) :

f ∈ M.closure {e} ↔ e ∈ M.closure {f}

theorem Matroid.IsNonloop.isNonloop_of_mem_closure {α : Type u_1} {M : Matroid α} {e f : α} (he : M.IsNonloop e) (hef : e ∈ M.closure {f}) :

theorem Matroid.IsNonloop.closure_eq_of_mem_closure {α : Type u_1} {M : Matroid α} {e f : α} (he : M.IsNonloop e) (hef : e ∈ M.closure {f}) :

M.closure {e} = M.closure {f}

theorem Matroid.IsNonloop.closure_eq_closure_iff_isCircuit_of_ne {α : Type u_1} {M : Matroid α} {e f : α} (he : M.IsNonloop e) (hef : e ≠ f) :

M.closure {e} = M.closure {f} ↔ M.IsCircuit {e, f}

Two distinct nonloops with the same closure form a circuit.

theorem Matroid.IsNonloop.closure_eq_closure_iff_eq_or_dep {α : Type u_1} {M : Matroid α} {e f : α} (he : M.IsNonloop e) (hf : M.IsNonloop f) :

M.closure {e} = M.closure {f} ↔ e = f ∨ ¬M.Indep {e, f}

theorem Matroid.exists_isNonloop {α : Type u_1} (M : Matroid α) [M.RankPos] :

∃ (e : α), M.IsNonloop e

theorem Matroid.IsNonloop.rankPos {α : Type u_1} {M : Matroid α} {e : α} (h : M.IsNonloop e) :

@[simp]

theorem Matroid.restrict_isNonloop_iff {α : Type u_1} {M : Matroid α} {e : α} {R : Set α} :

(M.restrict R).IsNonloop e ↔ M.IsNonloop e ∧ e ∈ R

theorem Matroid.IsNonloop.of_restrict {α : Type u_1} {M : Matroid α} {e : α} {R : Set α} (h : (M.restrict R).IsNonloop e) :

theorem Matroid.IsNonloop.of_isRestriction {α : Type u_1} {M N : Matroid α} {e : α} (h : N.IsNonloop e) (hNM : N.IsRestriction M) :

theorem Matroid.isNonloop_iff_restrict_of_mem {α : Type u_1} {M : Matroid α} {e : α} {R : Set α} (he : e ∈ R) :

M.IsNonloop e ↔ (M.restrict R).IsNonloop e

@[simp]

theorem Matroid.comap_isNonloop_iff {α : Type u_1} {β : Type u_2} {e : α} {M : Matroid β} {f : α → β} :

(M.comap f).IsNonloop e ↔ M.IsNonloop (f e)

@[simp]

theorem Matroid.freeOn_isNonloop_iff {α : Type u_1} {e : α} {E : Set α} :

(freeOn E).IsNonloop e ↔ e ∈ E

@[simp]

theorem Matroid.uniqueBaseOn_isNonloop_iff {α : Type u_1} {e : α} {I E : Set α} :

(uniqueBaseOn I E).IsNonloop e ↔ e ∈ I ∩ E

theorem Matroid.IsNonloop.exists_mem_isCocircuit {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsNonloop e) :

∃ (K : Set α), M.IsCocircuit K ∧ e ∈ K

@[simp]

theorem Matroid.closure_inter_setOf_isNonloop_eq {α : Type u_1} (M : Matroid α) (X : Set α) :

M.closure (X ∩ {e : α | M.IsNonloop e}) = M.closure X

def Matroid.IsColoop {α : Type u_1} (M : Matroid α) (e : α) :

A coloop is a loop of the dual matroid. See Matroid.isColoop_tfae for a number of equivalent definitions.

Equations

Instances For

def Matroid.coloops {α : Type u_1} (M : Matroid α) :

Set α

M.coloops is the set of coloops of M.

Equations

Instances For

theorem Matroid.IsColoop.mem_ground {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsColoop e) :

e ∈ M.E

theorem Matroid.coloops_subset_ground {α : Type u_1} (M : Matroid α) :

M.coloops ⊆ M.E

theorem Matroid.isColoop_iff_mem_coloops {α : Type u_1} {M : Matroid α} {e : α} :

M.IsColoop e ↔ e ∈ M.coloops

@[deprecated Matroid.isColoop_iff_mem_coloops (since := "2025-04-01")]

theorem Matroid.isColoop_iff_mem_loops {α : Type u_1} {M : Matroid α} {e : α} :

M.IsColoop e ↔ e ∈ M.coloops

Alias of Matroid.isColoop_iff_mem_coloops.

@[simp]

theorem Matroid.dual_loops {α : Type u_1} {M : Matroid α} :

M✶.loops = M.coloops

@[simp]

theorem Matroid.dual_coloops {α : Type u_1} {M : Matroid α} :

M✶.coloops = M.loops

theorem Matroid.IsColoop.dual_isLoop {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsColoop e) :

theorem Matroid.IsColoop.isCocircuit {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsColoop e) :

M.IsCocircuit {e}

theorem Matroid.IsLoop.dual_isColoop {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsLoop e) :

M✶.IsColoop e

@[simp]

theorem Matroid.dual_isColoop_iff_isLoop {α : Type u_1} {M : Matroid α} {e : α} :

M✶.IsColoop e ↔ M.IsLoop e

@[simp]

theorem Matroid.dual_isLoop_iff_isColoop {α : Type u_1} {M : Matroid α} {e : α} :

M✶.IsLoop e ↔ M.IsColoop e

theorem Matroid.singleton_isCocircuit {α : Type u_1} {M : Matroid α} {e : α} :

M.IsCocircuit {e} ↔ M.IsColoop e

theorem Matroid.isColoop_tfae {α : Type u_1} (M : Matroid α) (e : α) :

[M.IsColoop e, e ∈ M.coloops, M.IsCocircuit {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B, (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E, ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X, ¬M.Spanning (M.E \ {e})].TFAE

theorem Matroid.isColoop_iff_forall_mem_isBase {α : Type u_1} {M : Matroid α} {e : α} :

M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B

theorem Matroid.IsBase.mem_of_isColoop {α : Type u_1} {M : Matroid α} {e : α} {B : Set α} (hB : M.IsBase B) (he : M.IsColoop e) :

e ∈ B

theorem Matroid.IsColoop.mem_of_isBase {α : Type u_1} {M : Matroid α} {e : α} {B : Set α} (he : M.IsColoop e) (hB : M.IsBase B) :

e ∈ B

theorem Matroid.IsBase.coloops_subset {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.IsBase B) :

M.coloops ⊆ B

theorem Matroid.IsColoop.isNonloop {α : Type u_1} {M : Matroid α} {e : α} (h : M.IsColoop e) :

theorem Matroid.IsLoop.not_isColoop {α : Type u_1} {M : Matroid α} {e : α} (h : M.IsLoop e) :

theorem Matroid.IsColoop.notMem_isCircuit {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} (he : M.IsColoop e) (hC : M.IsCircuit C) :

e ∉ C

@[deprecated Matroid.IsColoop.notMem_isCircuit (since := "2025-05-23")]

theorem Matroid.IsColoop.not_mem_isCircuit {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} (he : M.IsColoop e) (hC : M.IsCircuit C) :

e ∉ C

Alias of Matroid.IsColoop.notMem_isCircuit.

theorem Matroid.IsCircuit.disjoint_coloops {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) :

Disjoint C M.coloops

theorem Matroid.isColoop_iff_forall_notMem_isCircuit {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :

M.IsColoop e ↔ ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C

@[deprecated Matroid.isColoop_iff_forall_notMem_isCircuit (since := "2025-05-23")]

theorem Matroid.isColoop_iff_forall_not_mem_isCircuit {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :

M.IsColoop e ↔ ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C

Alias of Matroid.isColoop_iff_forall_notMem_isCircuit.

theorem Matroid.isColoop_iff_forall_mem_compl_isCircuit {α : Type u_1} {M : Matroid α} {e : α} [M✶.RankPos] :

M.IsColoop e ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ M.E \ C

theorem Matroid.IsCircuit.not_isColoop_of_mem {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} (hC : M.IsCircuit C) (heC : e ∈ C) :

theorem Matroid.isColoop_iff_forall_mem_closure_iff_mem {α : Type u_1} {M : Matroid α} {e : α} :

M.IsColoop e ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X

theorem Matroid.isColoop_iff_forall_mem_closure_iff_mem' {α : Type u_1} {M : Matroid α} {e : α} :

M.IsColoop e ↔ (∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X) ∧ e ∈ M.E

A version of Matroid.isColoop_iff_forall_mem_closure_iff_mem where we only quantify over subsets of the ground set.

theorem Matroid.IsColoop.mem_closure_iff_mem {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (he : M.IsColoop e) :

e ∈ M.closure X ↔ e ∈ X

theorem Matroid.IsColoop.mem_of_mem_closure {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (he : M.IsColoop e) (heX : e ∈ M.closure X) :

e ∈ X

theorem Matroid.isColoop_iff_diff_not_spanning {α : Type u_1} {M : Matroid α} {e : α} :

M.IsColoop e ↔ ¬M.Spanning (M.E \ {e})

theorem Matroid.IsColoop.diff_not_spanning {α : Type u_1} {M : Matroid α} {e : α} :

M.IsColoop e → ¬M.Spanning (M.E \ {e})

Alias of the forward direction of Matroid.isColoop_iff_diff_not_spanning.

theorem Matroid.isColoop_iff_diff_closure {α : Type u_1} {M : Matroid α} {e : α} :

M.IsColoop e ↔ M.closure (M.E \ {e}) ≠ M.E

theorem Matroid.isColoop_iff_notMem_closure_compl {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :

M.IsColoop e ↔ e ∉ M.closure (M.E \ {e})

@[deprecated Matroid.isColoop_iff_notMem_closure_compl (since := "2025-05-23")]

theorem Matroid.isColoop_iff_not_mem_closure_compl {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :

M.IsColoop e ↔ e ∉ M.closure (M.E \ {e})

Alias of Matroid.isColoop_iff_notMem_closure_compl.

theorem Matroid.IsBase.isColoop_iff_forall_notMem_fundCircuit {α : Type u_1} {M : Matroid α} {e : α} {B : Set α} (hB : M.IsBase B) (he : e ∈ B) :

M.IsColoop e ↔ ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B

@[deprecated Matroid.IsBase.isColoop_iff_forall_notMem_fundCircuit (since := "2025-05-23")]

theorem Matroid.IsBase.isColoop_iff_forall_not_mem_fundCircuit {α : Type u_1} {M : Matroid α} {e : α} {B : Set α} (hB : M.IsBase B) (he : e ∈ B) :

M.IsColoop e ↔ ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B

Alias of Matroid.IsBase.isColoop_iff_forall_notMem_fundCircuit.

theorem Matroid.IsBasis'.inter_coloops_subset {α : Type u_1} {M : Matroid α} {X I : Set α} (hIX : M.IsBasis' I X) :

X ∩ M.coloops ⊆ I

theorem Matroid.IsBasis.inter_coloops_subset {α : Type u_1} {M : Matroid α} {X I : Set α} (hIX : M.IsBasis I X) :

X ∩ M.coloops ⊆ I

theorem Matroid.exists_mem_isCircuit_of_not_isColoop {α : Type u_1} {M : Matroid α} {e : α} (heE : e ∈ M.E) (he : ¬M.IsColoop e) :

∃ (C : Set α), M.IsCircuit C ∧ e ∈ C

@[simp]

theorem Matroid.closure_inter_coloops_eq {α : Type u_1} (M : Matroid α) (X : Set α) :

M.closure X ∩ M.coloops = X ∩ M.coloops

theorem Matroid.closure_inter_eq_of_subset_coloops {α : Type u_1} {M : Matroid α} {K : Set α} (X : Set α) (hK : K ⊆ M.coloops) :

M.closure X ∩ K = X ∩ K

theorem Matroid.closure_union_eq_of_subset_coloops {α : Type u_1} {M : Matroid α} {K : Set α} (X : Set α) (hK : K ⊆ M.coloops) :

M.closure (X ∪ K) = M.closure X ∪ K

theorem Matroid.closure_insert_isColoop_eq {α : Type u_1} {M : Matroid α} {e : α} (X : Set α) (he : M.IsColoop e) :

M.closure (insert e X) = insert e (M.closure X)

theorem Matroid.closure_eq_of_subset_coloops {α : Type u_1} {M : Matroid α} {K : Set α} (hK : K ⊆ M.coloops) :

M.closure K = K ∪ M.loops

theorem Matroid.closure_diff_eq_of_subset_coloops {α : Type u_1} {M : Matroid α} {K : Set α} (X : Set α) (hK : K ⊆ M.coloops) :

M.closure (X \ K) = M.closure X \ K

theorem Matroid.closure_disjoint_of_disjoint_of_subset_coloops {α : Type u_1} {M : Matroid α} {X K : Set α} (hXK : Disjoint X K) (hK : K ⊆ M.coloops) :

Disjoint (M.closure X) K

theorem Matroid.closure_disjoint_coloops_of_disjoint_coloops {α : Type u_1} {M : Matroid α} {X : Set α} (hX : Disjoint X M.coloops) :

Disjoint (M.closure X) M.coloops

theorem Matroid.closure_union_coloops_eq {α : Type u_1} (M : Matroid α) (X : Set α) :

M.closure (X ∪ M.coloops) = M.closure X ∪ M.coloops

theorem Matroid.IsColoop.notMem_closure_of_notMem {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (he : M.IsColoop e) (hX : e ∉ X) :

e ∉ M.closure X

@[deprecated Matroid.IsColoop.notMem_closure_of_notMem (since := "2025-05-23")]

theorem Matroid.IsColoop.not_mem_closure_of_not_mem {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (he : M.IsColoop e) (hX : e ∉ X) :

e ∉ M.closure X

Alias of Matroid.IsColoop.notMem_closure_of_notMem.

theorem Matroid.IsColoop.insert_indep_of_indep {α : Type u_1} {M : Matroid α} {e : α} {I : Set α} (he : M.IsColoop e) (hI : M.Indep I) :

M.Indep (insert e I)

theorem Matroid.union_indep_iff_indep_of_subset_coloops {α : Type u_1} {M : Matroid α} {I K : Set α} (hK : K ⊆ M.coloops) :

M.Indep (I ∪ K) ↔ M.Indep I

theorem Matroid.diff_indep_iff_indep_of_subset_coloops {α : Type u_1} {M : Matroid α} {I K : Set α} (hK : K ⊆ M.coloops) :

M.Indep (I \ K) ↔ M.Indep I

@[simp]

theorem Matroid.union_coloops_indep_iff {α : Type u_1} {M : Matroid α} {I : Set α} :

M.Indep (I ∪ M.coloops) ↔ M.Indep I

@[simp]

theorem Matroid.diff_coloops_indep_iff {α : Type u_1} {M : Matroid α} {I : Set α} :

M.Indep (I \ M.coloops) ↔ M.Indep I

theorem Matroid.coloops_indep {α : Type u_1} (M : Matroid α) :

M.Indep M.coloops

theorem Matroid.restrict_isColoop_iff {α : Type u_1} {M : Matroid α} {e : α} {R : Set α} (hRE : R ⊆ M.E) :

(M.restrict R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R

theorem Matroid.ext_indep_disjoint_loops_coloops {α : Type u_1} {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (hl : M₁.loops = M₂.loops) (hc : M₁.coloops = M₂.coloops) (h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)) :

M₁ = M₂

If two matroids agree on loops and coloops, and have the same independent sets after loops/coloops are removed, they are equal.

class Matroid.Loopless {α : Type u_1} (M : Matroid α) :

A Matroid is Loopless if it has no loop

loops_eq_empty : M.loops = ∅

Instances

theorem Matroid.loopless_iff {α : Type u_1} (M : Matroid α) :

M.Loopless ↔ M.loops = ∅

@[simp]

theorem Matroid.loops_eq_empty {α : Type u_1} (M : Matroid α) [M.Loopless] :

theorem Matroid.isNonloop_of_loopless {α : Type u_1} {M : Matroid α} {e : α} [M.Loopless] (he : e ∈ M.E := by aesop_mat) :

theorem Matroid.subsingleton_indep {α : Type u_1} {M : Matroid α} {I : Set α} [M.Loopless] (hI : I.Subsingleton) (hIE : I ⊆ M.E := by aesop_mat) :

theorem Matroid.not_isLoop {α : Type u_1} (M : Matroid α) [M.Loopless] (e : α) :

theorem Matroid.loopless_iff_forall_isNonloop {α : Type u_1} {M : Matroid α} :

M.Loopless ↔ ∀ e ∈ M.E, M.IsNonloop e

theorem Matroid.loopless_iff_forall_not_isLoop {α : Type u_1} {M : Matroid α} :

M.Loopless ↔ ∀ e ∈ M.E, ¬M.IsLoop e

theorem Matroid.loopless_iff_forall_isCircuit {α : Type u_1} {M : Matroid α} :

M.Loopless ↔ ∀ (C : Set α), M.IsCircuit C → C.Nontrivial

theorem Matroid.Loopless.ground_eq {α : Type u_1} (M : Matroid α) [M.Loopless] :

M.E = {e : α | M.IsNonloop e}

theorem Matroid.IsRestriction.loopless {α : Type u_1} {M N : Matroid α} [M.Loopless] (hR : N.IsRestriction M) :

instance Matroid.instRankPosOfNonemptyOfLoopless {α : Type u_1} {M : Matroid α} [M.Nonempty] [M.Loopless] :

@[simp]

theorem Matroid.loopyOn_isLoopless_iff {α : Type u_1} {E : Set α} :

(loopyOn E).Loopless ↔ E = ∅

def Matroid.removeLoops {α : Type u_1} (M : Matroid α) :

The loopless matroid obtained from M by deleting all its loops.

Equations

Instances For

theorem Matroid.removeLoops_eq_restrict {α : Type u_1} (M : Matroid α) :

M.removeLoops = M.restrict {e : α | M.IsNonloop e}

theorem Matroid.removeLoops_ground_eq {α : Type u_1} (M : Matroid α) :

M.removeLoops.E = {e : α | M.IsNonloop e}

instance Matroid.removeLoops_loopless {α : Type u_1} (M : Matroid α) :

M.removeLoops.Loopless

@[simp]

theorem Matroid.removeLoops_eq_self {α : Type u_1} (M : Matroid α) [M.Loopless] :

M.removeLoops = M

theorem Matroid.removeLoops_eq_self_iff {α : Type u_1} {M : Matroid α} :

M.removeLoops = M ↔ M.Loopless

theorem Matroid.removeLoops_isRestriction {α : Type u_1} (M : Matroid α) :

M.removeLoops.IsRestriction M

theorem Matroid.eq_restrict_removeLoops {α : Type u_1} (M : Matroid α) :

M.removeLoops.restrict M.E = M

@[simp]

theorem Matroid.removeLoops_indep_eq {α : Type u_1} {M : Matroid α} :

M.removeLoops.Indep = M.Indep

@[simp]

theorem Matroid.removeLoops_isBasis'_eq {α : Type u_1} {M : Matroid α} :

M.removeLoops.IsBasis' = M.IsBasis'

@[simp]

theorem Matroid.removeLoops_isBase_eq {α : Type u_1} {M : Matroid α} :

M.removeLoops.IsBase = M.IsBase

@[simp]

theorem Matroid.removeLoops_isNonloop_eq {α : Type u_1} {M : Matroid α} :

M.removeLoops.IsNonloop = M.IsNonloop

theorem Matroid.IsNonloop.removeLoops_isNonloop {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsNonloop e) :

M.removeLoops.IsNonloop e

theorem Matroid.removeLoops_idem {α : Type u_1} (M : Matroid α) :

M.removeLoops.removeLoops = M.removeLoops

theorem Matroid.removeLoops_restrict_eq_restrict {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ {e : α | M.IsNonloop e}) :

M.removeLoops.restrict X = M.restrict X

@[simp]

theorem Matroid.restrict_univ_removeLoops_eq {α : Type u_1} {M : Matroid α} :

(M.restrict Set.univ).removeLoops = M.removeLoops

theorem Matroid.IsRestriction.isRestriction_removeLoops {α : Type u_1} {M N : Matroid α} (hNM : N.IsRestriction M) [N.Loopless] :

N.IsRestriction M.removeLoops

theorem Matroid.removeLoops_mono_isRestriction {α : Type u_1} {M N : Matroid α} (hNM : N.IsRestriction M) :

N.removeLoops.IsRestriction M.removeLoops