Matroid.Parallel.Basic

source

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

Partition (Set α)

The partition of the nonloops of M into parallel classes.

Equations

M.parallelClasses = ⋯.covByPartition

Instances For

source

@[simp]

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

M.parallelClasses.supp = {e : α | M.IsNonloop e}

source

@[simp]

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

e ∈ M.parallelClasses.supp ↔ M.IsNonloop e

source

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

α → α → Prop

Equations

M.Parallel = ⇑M.parallelClasses

Instances For

source

@[simp]

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

⇑M.parallelClasses = M.Parallel

source

theorem Matroid.parallel_iff {α : Type u_1} {M : Matroid α} {e f : α} :

M.Parallel e f ↔ M.IsNonloop e ∧ M.IsNonloop f ∧ M.closure {e} = M.closure {f}

source

instance Matroid.instSymmParallel {α : Type u_1} {M : Matroid α} :

Std.Symm M.Parallel

source

instance Matroid.instIsTransParallel {α : Type u_1} {M : Matroid α} :

IsTrans α M.Parallel

source

theorem Matroid.Parallel.symm {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel e f) :

M.Parallel f e

source

theorem Matroid.parallel_comm {α : Type u_1} {M : Matroid α} {e f : α} :

M.Parallel e f ↔ M.Parallel f e

source

theorem Matroid.Parallel.trans {α : Type u_1} {M : Matroid α} {e f g : α} (h : M.Parallel e f) (h' : M.Parallel f g) :

M.Parallel e g

source

theorem Matroid.Parallel.closure_eq_closure {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel e f) :

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

source

theorem Matroid.Parallel.isNonloop_left {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel e f) :

M.IsNonloop e

source

theorem Matroid.Parallel.isNonloop_right {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel e f) :

M.IsNonloop f

source

theorem Matroid.Parallel.mem_ground_left {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel e f) :

e ∈ M.E

source

theorem Matroid.Parallel.mem_ground_right {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel e f) :

f ∈ M.E

source

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

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

source

theorem Matroid.Parallel.mem_closure {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel e f) :

e ∈ M.closure {f}

source

theorem Matroid.Parallel.parallel_iff_left {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel e f) {x : α} :

M.Parallel x e ↔ M.Parallel x f

source

theorem Matroid.Parallel.parallel_iff_right {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel e f) {x : α} :

M.Parallel e x ↔ M.Parallel f x

source

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

{f : α | M.Parallel e f} = M.closure {e} \ M.loops

source

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

M.closure {e} = {f : α | M.Parallel e f} ∪ M.loops

source

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

M.Parallel e e

source

@[simp]

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

M.Parallel e e ↔ M.IsNonloop e

source

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

¬M.Parallel e f

source

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

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

source

theorem Matroid.Loopless.parallel_class_eq_closure {α : Type u_1} {M : Matroid α} (h : M.Loopless) (e : α) :

{f : α | M.Parallel e f} = M.closure {e}

source

theorem Matroid.Parallel.dep_of_ne {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel e f) (hne : e ≠ f) :

M.Dep {e, f}

source

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

M.Parallel e f ↔ M.IsCircuit {e, f}

source

theorem Matroid.Parallel.isCircuit_of_ne {α : Type u_1} {M : Matroid α} {e f : α} (hef : M.Parallel e f) (hne : e ≠ f) :

M.IsCircuit {e, f}

source

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

M.Parallel e f ↔ M.Dep {e, f}

source

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

¬M.Parallel e f ↔ M.Indep {e, f}

source

theorem Matroid.Parallel.eq_of_indep {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel e f) (hi : M.Indep {e, f}) :

e = f

source

theorem Matroid.parallel_iff_isNonloop_isNonloop_indep_imp_eq {α : Type u_1} {M : Matroid α} {e f : α} :

M.Parallel e f ↔ M.IsNonloop e ∧ M.IsNonloop f ∧ (M.Indep {e, f} → e = f)

source

theorem Matroid.Parallel.mem_closure_iff_mem_closure {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel e f) {X : Set α} :

e ∈ M.closure X ↔ f ∈ M.closure X

source

theorem Matroid.IsNonloop.parallel_iff_forall_mem_of_mem_of_isCocircuit {α : Type u_1} {M : Matroid α} {e f : α} (henl : M.IsNonloop e) (hf : f ∈ M.E) :

M.Parallel e f ↔ ∀ (C : Set α), M.IsCocircuit C → e ∈ C → f ∈ C

source

theorem Matroid.IsCocircuit.mem_iff_mem_of_parallel {α : Type u_1} {M : Matroid α} {e f : α} {K : Set α} (hK : M.IsCocircuit K) (hef : M.Parallel e f) :

e ∈ K ↔ f ∈ K

source

theorem Matroid.parallel_dual_iff_forall_circuit {α : Type u_1} {M : Matroid α} {e f : α} (henl : M✶.IsNonloop e) (hf : f ∈ M.E) :

M✶.Parallel e f ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ C → f ∈ C

source

theorem Matroid.IsNonloop.exists_isCircuit_mem_notMem {α : Type u_1} {M : Matroid α} {e f : α} (henl : M✶.IsNonloop e) (hnp : ¬M✶.Parallel e f) :

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

source

theorem Matroid.Parallel.isLoop_contractElem {α : Type u_1} {M : Matroid α} {e f : α} (hef : M.Parallel e f) (hne : e ≠ f) :

(M.contract {e}).IsLoop f

source

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

(M.restrict R).Parallel e f ↔ M.Parallel e f ∧ e ∈ R ∧ f ∈ R

source

theorem Matroid.delete_parallel_iff {α : Type u_1} {M : Matroid α} {e f : α} {D : Set α} :

(M.delete D).Parallel e f ↔ M.Parallel e f ∧ e ∉ D ∧ f ∉ D

source

theorem Matroid.contract_parallel_iff {α : Type u_1} {M : Matroid α} {e f : α} {C : Set α} :

(M.contract C).Parallel e f ↔ f ∈ M.closure (insert e C) ∧ f ∉ M.closure C

source

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

N.Parallel e f ↔ M.Parallel e f ∧ e ∈ N.E ∧ f ∈ N.E

source

theorem Matroid.Parallel.of_isRestriction {α : Type u_1} {M N : Matroid α} {e f : α} (hN : N.Parallel e f) (hNM : N.IsRestriction M) :

M.Parallel e f

source

theorem Matroid.Parallel.parallel_isRestriction {α : Type u_1} {M N : Matroid α} {e f : α} (hM : M.Parallel e f) (hNM : N.IsRestriction M) (he : e ∈ N.E) (hf : f ∈ N.E) :

N.Parallel e f

source

@[simp]

theorem Matroid.removeLoops_parallel_iff {α : Type u_1} {M : Matroid α} {e f : α} :

M.removeLoops.Parallel e f ↔ M.Parallel e f

source

theorem Matroid.Parallel.mem_isCocircuit_of_mem {α : Type u_1} {M : Matroid α} {e f : α} {K : Set α} (hef : M.Parallel e f) (hK : M.IsCocircuit K) (he : e ∈ K) :

f ∈ K

source

@[simp]

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

(M.comap φ).Parallel e f ↔ M.Parallel (φ e) (φ f)

source

@[simp]

theorem Matroid.comapOn_parallel_iff {α : Type u_1} {e f : α} {β : Type u_2} {φ : α → β} {M : Matroid β} {E : Set α} :

(M.comapOn E φ).Parallel e f ↔ M.Parallel (φ e) (φ f) ∧ e ∈ E ∧ f ∈ E

source

theorem Matroid.IsCircuit.mem_iff_mem_of_parallel_dual {α : Type u_1} {M : Matroid α} {e f : α} {C : Set α} (h : M.IsCircuit C) (hef : M✶.Parallel e f) :

e ∈ C ↔ f ∈ C

source

theorem Matroid.IsCircuit.mem_iff_mem_of_parallel_bDual {α : Type u_1} {M : Matroid α} {e f : α} {C : Set α} {b : Bool} (h : (M.bDual b).IsCircuit C) (hef : (M.bDual !b).Parallel e f) :

e ∈ C ↔ f ∈ C

source

theorem Matroid.Dep.eq_of_subset_pair {α : Type u_1} {M : Matroid α} {e f : α} {D : Set α} (hD : M.Dep D) (hDss : D ⊆ {e, f}) (he : M.IsNonloop e) (hf : M.IsNonloop f) :

D = {e, f}

source

def Matroid.Parallel' {α : Type u_1} (M : Matroid α) (e f : α) :

Prop

Two elements are Parallel' if they are either both loops or are Parallel isNonloops. (Sometimes allowing loops is more convenient.)

Equations

M.Parallel' e f = (e ∈ M.E ∧ f ∈ M.E ∧ M.closure {e} = M.closure {f})

Instances For

source

theorem Matroid.Parallel'.mem_ground_left {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel' e f) :

e ∈ M.E

source

theorem Matroid.Parallel'.mem_ground_right {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel' e f) :

f ∈ M.E

source

theorem Matroid.Parallel'.closure_eq_closure {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel' e f) :

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

source

theorem Matroid.Parallel'.symm {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel' e f) :

M.Parallel' f e

source

theorem Matroid.parallel'_self {α : Type u_1} {M : Matroid α} {e : α} (h : e ∈ M.E) :

M.Parallel' e e

source

theorem Matroid.Parallel'.trans {α : Type u_1} {M : Matroid α} {e f g : α} (h : M.Parallel' e f) (h' : M.Parallel' f g) :

M.Parallel' e g

source

theorem Matroid.Parallel'.parallel_of_isNonloop {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel' e f) (he : M.IsNonloop e) :

M.Parallel e f

source

theorem Matroid.Parallel.parallel' {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel e f) :

M.Parallel' e f

source

theorem Matroid.Parallel'.parallel_iff {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel' e f) :

M.Parallel e f ↔ M.IsNonloop e

source

theorem Matroid.Parallel'.isLoop_of_isLoop {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel' e f) (he : M.IsLoop e) :

M.IsLoop f

source

theorem Matroid.Parallel'.isLoop_or_parallel {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel' e f) :

M.IsLoop e ∧ M.IsLoop f ∨ M.Parallel e f

source

theorem Matroid.parallel'_iff_loops_or_parallel {α : Type u_1} {M : Matroid α} {e f : α} :

M.Parallel' e f ↔ M.IsLoop e ∧ M.IsLoop f ∨ M.Parallel e f

source

theorem Matroid.parallel'_iff_closure_eq_closure {α : Type u_1} {M : Matroid α} (e f : α) (he : e ∈ M.E := by aesop_mat) (hf : f ∈ M.E := by aesop_mat) :

M.Parallel' e f ↔ M.closure {e} = M.closure {f}

source

theorem Matroid.Parallel'.mem_closure {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel' e f) :

e ∈ M.closure {f}

source

theorem Matroid.Parallel'.eq_of_indep {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel' e f) (hef : M.Indep {e, f}) :

e = f

source

@[simp]

theorem Matroid.parallel'_iff_parallel {α : Type u_1} {M : Matroid α} {e f : α} [M.Loopless] :

M.Parallel' e f ↔ M.Parallel e f

source

theorem Matroid.Parallel'.mem_closure_iff_mem_closure {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel' e f) {X : Set α} :

e ∈ M.closure X ↔ f ∈ M.closure X

source

theorem Matroid.Parallel'.restrict {α : Type u_1} {M : Matroid α} {e f : α} (hef : M.Parallel' e f) {R : Set α} (heR : e ∈ R) (hfR : f ∈ R) :

(M.restrict R).Parallel' e f

source

theorem Matroid.Parallel'.delete {α : Type u_1} {M : Matroid α} {e f : α} (hef : M.Parallel' e f) {D : Set α} (heD : e ∉ D) (hfD : f ∉ D) :

(M.delete D).Parallel' e f

source

theorem Matroid.Parallel'.contract {α : Type u_1} {M : Matroid α} {e f : α} (hef : M.Parallel' e f) {C : Set α} (heC : e ∉ C) (hfC : f ∉ C) :

(M.contract C).Parallel' e f

source

theorem Matroid.Parallel'.of_isMinor {α : Type u_1} {M N : Matroid α} {e f : α} (hef : M.Parallel' e f) (hNM : N ≤m M) (heN : e ∈ N.E) (hfN : f ∈ N.E) :

N.Parallel' e f

source

theorem Matroid.Parallel.project {α : Type u_1} {M : Matroid α} {e f : α} (hef : M.Parallel' e f) (X : Set α) :

(M.project X).Parallel' e f

source

theorem Matroid.closure_range_of_forall_parallel'_subtype {α : Type u_1} {M : Matroid α} {X : Set α} (φ : ↑X → α) (h_para : ∀ (e : ↑X), M.Parallel' (↑e) (φ e)) :

M.closure (Set.range φ) = M.closure X

source

theorem Matroid.closure_image_of_forall_parallel'_subtype {α : Type u_1} {M : Matroid α} {X : Set α} (φ : ↑X → α) (h_para : ∀ (e : ↑X), M.Parallel' (↑e) (φ e)) (Y : Set ↑X) :

M.closure (φ '' Y) = M.closure (Subtype.val '' Y)

source

theorem Matroid.closure_image_of_forall_parallel' {α : Type u_1} {M : Matroid α} (φ : α → α) (h_para : ∀ (e : α), M.Parallel' e (φ e)) (X : Set α) :

M.closure (φ '' X) = M.closure X

source

def Matroid.isoOfMapParallelRestr {α : Type u_1} {M : Matroid α} {X Y : Set α} (φ : ↑X ≃ ↑Y) (h_para : ∀ (e : ↑X), M.Parallel' ↑e ↑(φ e)) :

M.restrict X ≂ M.restrict Y

If φ : X ≃ Y is such that e and φ e are always Parallel', then φ determines a matroid isomorphism between M ↾ X and M ↾ Y.

Equations

Matroid.isoOfMapParallelRestr φ h_para = Matroid.isoOfForallImageclosure φ ⋯

Instances For

source

def Matroid.isoOfMapParallel {α : Type u_1} {M : Matroid α} (φ : ↑M.E ≃ ↑M.E) (h_para : ∀ (e : ↑M.E), M.Parallel' ↑e ↑(φ e)) :

M ≂ M

If φ is a permutation of M.E that maps each element to something Parallel', then φ determines an automorphism of M.

Equations

Matroid.isoOfMapParallel φ h_para = (Matroid.Iso.ofEq ⋯).symm.trans ((Matroid.isoOfMapParallelRestr φ h_para).trans (Matroid.Iso.ofEq ⋯))

Instances For

source

noncomputable def Matroid.isoOfMapParallelBijOn {α : Type u_1} {M : Matroid α} {φ : α → α} (hφ : Set.BijOn φ M.E M.E) (h_para : ∀ e ∈ M.E, M.Parallel' e (φ e)) :

M ≂ M

If φ : α → α restricts to a permutation of M.E and maps each element to something Parallel', it induces an automorphism of M.

Equations

Matroid.isoOfMapParallelBijOn hφ h_para = { toEquiv := Set.BijOn.equiv φ hφ, indep_image_iff' := ⋯ }

Instances For

source

@[simp]

theorem Matroid.isoOfMapParallelBijOn_toEquiv {α : Type u_1} {M : Matroid α} {φ : α → α} (hφ : Set.BijOn φ M.E M.E) (h_para : ∀ e ∈ M.E, M.Parallel' e (φ e)) :

(isoOfMapParallelBijOn hφ h_para).toEquiv = Set.BijOn.equiv φ hφ

source

@[simp]

theorem Matroid.isoOfMapParallelBijOn_apply {α : Type u_1} {M : Matroid α} {φ : α → α} (hφ : Set.BijOn φ M.E M.E) (h_para : ∀ e ∈ M.E, M.Parallel' e (φ e)) (x : ↑M.E) :

(isoOfMapParallelBijOn hφ h_para) x = ⟨φ ↑x, ⋯⟩

source

@[simp]

theorem Matroid.isoOfMapParallelBijOn_apply_image {α : Type u_1} {M : Matroid α} {φ : α → α} (hφ : Set.BijOn φ M.E M.E) (h_para : ∀ e ∈ M.E, M.Parallel' e (φ e)) (X : Set ↑M.E) :

Subtype.val '' ⇑(isoOfMapParallelBijOn hφ h_para) '' X = φ '' Subtype.val '' X

source

noncomputable def Matroid.isoOfSwapParallel {α : Type u_1} {M : Matroid α} {e f : α} [DecidableEq α] (h_para : M.Parallel' e f) :

M ≂ M

Swapping two Parallel' matroid elements gives an automorphism

Equations

Matroid.isoOfSwapParallel h_para = Matroid.isoOfMapParallelBijOn ⋯ ⋯

Instances For

source

@[simp]

theorem Matroid.isoOfSwapParallel_toEquiv_apply_coe {α : Type u_1} {M : Matroid α} {e f : α} [DecidableEq α] (h_para : M.Parallel' e f) (a✝ : ↑M.E) :

↑((isoOfSwapParallel h_para).toEquiv a✝) = (Equiv.swap e f) ↑a✝

source

@[simp]

theorem Matroid.isoOfSwapParallel_toEquiv_symm_apply {α : Type u_1} {M : Matroid α} {e f : α} [DecidableEq α] (h_para : M.Parallel' e f) (b : ↑M.E) :

(isoOfSwapParallel h_para).toEquiv.symm b = Function.surjInv ⋯ b

source

@[simp]

theorem Matroid.isoOfSwapParallel_apply {α : Type u_1} {M : Matroid α} {e f : α} [DecidableEq α] (h_para : M.Parallel' e f) (x : ↑M.E) :

(isoOfSwapParallel h_para) x = ⟨(Equiv.swap e f) ↑x, ⋯⟩

source

@[simp]

theorem Matroid.isoOfSwapParallel_apply_image {α : Type u_1} {M : Matroid α} {e f : α} [DecidableEq α] (h_para : M.Parallel' e f) (X : Set ↑M.E) :

Subtype.val '' ⇑(isoOfSwapParallel h_para) '' X = ⇑(Equiv.swap e f) '' Subtype.val '' X

source

theorem Matroid.Indep.parallel'_substitute {α : Type u_1} {M : Matroid α} {e f : α} {I : Set α} (hI : M.Indep I) (h_para : M.Parallel' e f) (heI : e ∈ I) :

M.Indep (insert f (I \ {e}))

source

theorem Matroid.Parallel'.indep_substitute_iff {α : Type u_1} {M : Matroid α} {e f : α} {I : Set α} (h_para : M.Parallel' e f) (he : e ∈ I) (hf : f ∉ I) :

M.Indep I ↔ M.Indep (insert f (I \ {e}))

source

theorem Matroid.Parallel'.eq_mapEquiv_swap {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel' e f) [DecidableEq α] :

M.mapEquiv (Equiv.swap e f) = M

source

theorem Matroid.Parallel'.contract_pair_eq {α : Type u_1} {M : Matroid α} {e f : α} (hef : M.Parallel' e f) :

M.contract {e, f} = (M.contract {e}).delete {f}

source

theorem Matroid.Parallel'.contract_delete_comm {α : Type u_1} {M : Matroid α} {e f : α} (hef : M.Parallel' e f) :

(M.contract {e}).delete {f} = (M.contract {f}).delete {e}

source

theorem Matroid.Parallel'.deleteElem_eq_mapEquiv {α : Type u_1} {M : Matroid α} {e f : α} [DecidableEq α] (hef : M.Parallel' e f) :

M.delete {e} = (M.delete {f}).mapEquiv (Equiv.swap e f)

source

theorem Matroid.indep_iff_range_indep_of_paraMap {α : Type u_1} {M : Matroid α} {I : Set α} {φ : ↑I → α} (hφ : Function.Injective φ) (h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)) :

M.Indep I ↔ M.Indep (Set.range φ)

source

theorem Matroid.Indep.paraMap_injective {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (φ : ↑I → α) (h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)) :

Function.Injective φ

source

theorem Matroid.Indep.indep_range_paraMap {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (φ : ↑I → α) (h_para : ∀ (e : ↑I), M.Parallel' (↑e) (φ e)) :

M.Indep (Set.range φ)

source

theorem Matroid.Indep.image_paraMap {α : Type u_1} {M : Matroid α} {I : Set α} {φ : α → α} (hI : M.Indep I) (h_para : ∀ e ∈ I, M.Parallel' e (φ e)) :

M.Indep (φ '' I)

source

theorem Matroid.Indep.of_image_paraMap {α : Type u_1} {M : Matroid α} {I : Set α} {φ : α → α} (hI : M.Indep (φ '' I)) (hφ : Set.InjOn φ I) (h_para : ∀ e ∈ I, M.Parallel' e (φ e)) :

M.Indep I

source

theorem Matroid.indep_image_iff_of_injOn_paraMap {α : Type u_1} {M : Matroid α} {I : Set α} {φ : α → α} (hφ : Set.InjOn φ I) (h : ∀ e ∈ I, M.Parallel' e (φ e)) :

M.Indep (φ '' I) ↔ M.Indep I

source

theorem Matroid.mem_parallelClasses_iff_eq_closure_diff_loops {α : Type u_1} {M : Matroid α} {P : Set α} :

P ∈ M.parallelClasses ↔ ∃ (e : α), M.IsNonloop e ∧ P = M.closure {e} \ M.loops

source

theorem Matroid.mem_parallelClasses_iff {α : Type u_1} {M : Matroid α} {P : Set α} :

P ∈ M.parallelClasses ↔ ∃ (e : α), M.IsNonloop e ∧ P = {f : α | M.Parallel e f}

source

@[simp]

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

M.parallelClasses.partOf e = {f : α | M.Parallel e f}

source

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

↥M.parallelClasses ≃ { P : Set α // M.IsPoint P }

Parallel classes are equivalent to points.

Equations

M.parallelPointEquiv = { toFun := fun (P : ↥M.parallelClasses) => ⟨↑P ∪ M.loops, ⋯⟩, invFun := fun (P : { P : Set α // M.IsPoint P }) => ⟨↑P \ M.loops, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem Matroid.parallelPointEquiv_symm_apply_coe {α : Type u_1} (M : Matroid α) (P : { P : Set α // M.IsPoint P }) :

↑(M.parallelPointEquiv.symm P) = ↑P \ M.loops

source

@[simp]

theorem Matroid.parallelPointEquiv_apply_coe {α : Type u_1} (M : Matroid α) (P : ↥M.parallelClasses) :

↑(M.parallelPointEquiv P) = ↑P ∪ M.loops

source

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

Prop

Equations

M.Series e f = M✶.Parallel e f

Instances For