theorem pairwise_on_bool' {α : Type u_1} {r : α → α → Prop} {f : Bool → α} (i : Bool) : Pairwise (Function.onFun r f) ↔ r (f i) (f !i) ∧ r (f !i) (f i)

theorem pairwise_disjoint_on_bool' {α : Type u_1} {f : Bool → Set α} (i : Bool) : Pairwise (Function.onFun Disjoint f) ↔ Disjoint (f i) (f !i)

theorem iUnion_bool' {α : Type u_1} (f : Bool → Set α) (i : Bool) : ⋃ (i : Bool), f i = f i ∪ f !i

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

A bipartition of the ground set of a matroid, implicitly including the data of the actual matroid.

Equations

• M.Separation = M.E.IndexedPartition Bool

@[implicit_reducible]

instance Matroid.instFunLikeSeparationBoolSet {α : Type u_1} {M : Matroid α} : FunLike M.Separation Bool (Set α)

Equations

• Matroid.instFunLikeSeparationBoolSet = { coe := fun (P : M.Separation) (i : Bool) => P.toFun i, coe_injective' := ⋯ }

def Matroid.Separation.toBipartition {α : Type u_1} {M : Matroid α} (P : M.Separation) : M.E.IndexedPartition Bool

Equations

• P.toBipartition = P

@[simp]

theorem Matroid.Separation.toBipartition_apply {α : Type u_1} {M : Matroid α} (P : M.Separation) (i : Bool) : P.toBipartition i = P i

@[simp]

theorem Matroid.Separation.toFun_eq_coe {α : Type u_1} {M : Matroid α} (P : M.Separation) : P.toFun = ⇑P

theorem Matroid.Separation.pairwise_disjoint {α : Type u_1} {M : Matroid α} (P : M.Separation) : Pairwise (Function.onFun Disjoint ⇑P)

theorem Matroid.Separation.disjoint {α : Type u_1} {M : Matroid α} {i j : Bool} (P : M.Separation) (hij : i ≠ j) : Disjoint (P i) (P j)

theorem Matroid.Separation.subset {α : Type u_1} {M : Matroid α} (P : M.Separation) {i : Bool} : P i ⊆ M.E

theorem Matroid.Separation.subset' {α : Type u_1} {M : Matroid α} (P : M.Separation) (i : Bool) : P i ⊆ M.E

A version of Separation.subset with an explicit argument.

theorem Matroid.Separation.iUnion_eq {α : Type u_1} {M : Matroid α} (P : M.Separation) : ⋃ (i : Bool), P i = M.E

@[simp]

theorem Matroid.Separation.union_eq {α : Type u_1} {M : Matroid α} {P : M.Separation} : P true ∪ P false = M.E

@[simp]

theorem Matroid.Separation.union_eq' {α : Type u_1} {M : Matroid α} {P : M.Separation} : P false ∪ P true = M.E

@[simp]

theorem Matroid.Separation.union_bool_eq {α : Type u_1} {M : Matroid α} {P : M.Separation} (i : Bool) : (P i ∪ P !i) = M.E

@[simp]

theorem Matroid.Separation.union_bool_eq' {α : Type u_1} {M : Matroid α} {P : M.Separation} (i : Bool) : (P !i) ∪ P i = M.E

@[simp]

theorem Matroid.Separation.disjoint_true_false {α : Type u_1} {M : Matroid α} {P : M.Separation} : Disjoint (P true) (P false)

@[simp]

theorem Matroid.Separation.disjoint_false_true {α : Type u_1} {M : Matroid α} {P : M.Separation} : Disjoint (P false) (P true)

@[simp]

theorem Matroid.Separation.disjoint_bool {α : Type u_1} {M : Matroid α} {P : M.Separation} (i : Bool) : Disjoint (P i) (P !i)

@[simp]

theorem Matroid.Separation.compl_eq {α : Type u_1} {M : Matroid α} (P : M.Separation) (i : Bool) : M.E \ P i = P !i

@[simp]

theorem Matroid.Separation.compl_not_eq {α : Type u_1} {M : Matroid α} (P : M.Separation) (i : Bool) : (M.E \ P !i) = P i

@[simp]

theorem Matroid.Separation.compl_dual_eq {α : Type u_1} {M : Matroid α} (P : M✶.Separation) (i : Bool) : M.E \ P i = P !i

@[simp]

theorem Matroid.Separation.compl_dual_not_eq {α : Type u_1} {M : Matroid α} (P : M✶.Separation) (i : Bool) : (M.E \ P !i) = P i

theorem Matroid.Separation.disjoint_iff_subset_not {α : Type u_1} {M : Matroid α} {X : Set α} {i : Bool} {P : M.Separation} (hX : X ⊆ M.E := by aesop_mat) : Disjoint X (P i) ↔ X ⊆ P !i

theorem Matroid.Separation.disjoint_not_iff_subset {α : Type u_1} {M : Matroid α} {X : Set α} {i : Bool} {P : M.Separation} (hX : X ⊆ M.E := by aesop_mat) : Disjoint X (P !i) ↔ X ⊆ P i

theorem Matroid.Separation.not_mem_iff_mem_not {α : Type u_1} {M : Matroid α} {i : Bool} {P : M.Separation} {x : α} (hx : x ∈ M.E := by aesop_mat) : x ∉ P i ↔ x ∈ P !i

def Matroid.Separation.mk {α : Type u_1} {M : Matroid α} (f : Bool → Set α) (dj : Pairwise (Function.onFun Disjoint f)) (iUnion_eq : ⋃ (i : Bool), f i = M.E) : M.Separation

Equations

• Matroid.Separation.mk f dj iUnion_eq = { toFun := f, pairwise_disjoint' := dj, iUnion_eq' := iUnion_eq }

@[simp]

theorem Matroid.Separation.mk_apply {α : Type u_1} {M : Matroid α} (f : Bool → Set α) (dj : Pairwise (Function.onFun Disjoint f)) (iUnion_eq : ⋃ (i : Bool), f i = M.E) (i : Bool) : (Separation.mk f dj iUnion_eq) i = f i

def Matroid.Separation.mk' {α : Type u_1} {M : Matroid α} (A B : Set α) (disjoint : Disjoint A B) (union_eq : A ∪ B = M.E) : M.Separation

Equations

• Matroid.Separation.mk' A B disjoint union_eq = { toFun := fun (i : Bool) => bif i then A else B, pairwise_disjoint' := ⋯, iUnion_eq' := ⋯ }

@[simp]

theorem Matroid.Separation.mk'_true {α : Type u_1} {M : Matroid α} {A B : Set α} {hdj : Disjoint A B} {hu : A ∪ B = M.E} : (Separation.mk' A B hdj hu) true = A

@[simp]

theorem Matroid.Separation.mk'_false {α : Type u_1} {M : Matroid α} {A B : Set α} {hdj : Disjoint A B} {hu : A ∪ B = M.E} : (Separation.mk' A B hdj hu) false = B

theorem Matroid.Separation.ext_bool {α : Type u_1} {M : Matroid α} {P P' : M.Separation} (i : Bool) (h : P i = P' i) : P = P'

theorem Matroid.Separation.ext {α : Type u_1} {M : Matroid α} {P P' : M.Separation} (h : P true = P' true) : P = P'

theorem Matroid.Separation.ext_iff_bool {α : Type u_1} {M : Matroid α} {P P' : M.Separation} (i : Bool) : P = P' ↔ P i = P' i

def Matroid.Separation.symm {α : Type u_1} {M : Matroid α} (P : M.Separation) : M.Separation

Equations

• P.symm = Set.IndexedPartition.symm P

@[simp]

theorem Matroid.Separation.symm_true {α : Type u_1} {M : Matroid α} (P : M.Separation) : P.symm true = P false

@[simp]

theorem Matroid.Separation.symm_false {α : Type u_1} {M : Matroid α} (P : M.Separation) : P.symm false = P true

@[simp]

theorem Matroid.Separation.symm_apply {α : Type u_1} {M : Matroid α} (P : M.Separation) (i : Bool) : P.symm i = P !i

@[simp]

theorem Matroid.Separation.symm_symm {α : Type u_1} {M : Matroid α} (P : M.Separation) : P.symm.symm = P

def Matroid.Separation.bSymm {α : Type u_1} {M : Matroid α} (P : M.Separation) (b : Bool) : M.Separation

Equations

• P.bSymm b = bif b then P.symm else P

@[simp]

theorem Matroid.Separation.bSymm_apply {α : Type u_1} {M : Matroid α} (P : M.Separation) (b i : Bool) : (P.bSymm b) i = P (i != b)

@[simp]

theorem Matroid.Separation.bSymm_false {α : Type u_1} {M : Matroid α} (P : M.Separation) : P.bSymm false = P

@[simp]

theorem Matroid.Separation.bSymm_true {α : Type u_1} {M : Matroid α} (P : M.Separation) : P.bSymm true = P.symm

@[simp]

theorem Matroid.Separation.bSymm_bSymm {α : Type u_1} {M : Matroid α} (P : M.Separation) (b c : Bool) : (P.bSymm b).bSymm c = P.bSymm (b != c)

@[simp]

theorem Matroid.Separation.compl_true {α : Type u_1} {M : Matroid α} (P : M.Separation) : M.E \ P true = P false

@[simp]

theorem Matroid.Separation.compl_false {α : Type u_1} {M : Matroid α} (P : M.Separation) : M.E \ P false = P true

@[simp]

theorem Matroid.Separation.subset_ground {α : Type u_1} {M : Matroid α} {i : Bool} (P : M.Separation) : P i ⊆ M.E

theorem Matroid.Separation.apply_eq_iff {α : Type u_1} {M : Matroid α} {i : Bool} {P : M.Separation} : P i = M.E ↔ (P !i) = ∅

def Matroid.Separation.copy {α : Type u_1} {M M' : Matroid α} (P : M.Separation) (h_eq : M = M') : M'.Separation

Transfer a separation across a matroid equality.

Equations

• P.copy h_eq = { toFun := P.toFun, pairwise_disjoint' := ⋯, iUnion_eq' := ⋯ }

@[simp]

theorem Matroid.Separation.copy_apply {α : Type u_1} {M N : Matroid α} (P : M.Separation) (h_eq : M = N) (i : Bool) : (P.copy h_eq) i = P i

@[simp]

theorem Matroid.Separation.copy_rfl {α : Type u_1} {M : Matroid α} (P : M.Separation) (h : M = M := ⋯) : P.copy h = P

@[simp]

theorem Matroid.Separation.bSymm_copy {α : Type u_1} {M N : Matroid α} (P : M.Separation) (b : Bool) (h : M = N) : (P.copy h).bSymm b = (P.bSymm b).copy h

@[simp]

theorem Matroid.Separation.symm_copy {α : Type u_1} {M N : Matroid α} (P : M.Separation) (h : M = N) : (P.copy h).symm = P.symm.copy h

def Matroid.Separation.copy' {α : Type u_1} {M M' : Matroid α} (P : M.Separation) (h_eq : M.E = M'.E) : M'.E.IndexedPartition Bool

A version of copy where the ground sets are equal, but the matroids need not be. copy is preferred where possible, so that lemmas depending on matroid structure like eConn_copy can be @[simp].

Equations

• P.copy' h_eq = Set.IndexedPartition.copy P h_eq

@[simp]

theorem Matroid.Separation.copy'_apply {α : Type u_1} {M N : Matroid α} (P : M.Separation) (h_eq : M.E = N.E) (i : Bool) : (P.copy' h_eq) i = P i

def Matroid.Separation.induce {α : Type u_1} {M : Matroid α} (P : M.Separation) (N : Matroid α) (i : Bool := false) : N.Separation

Transfer a separation from M to another matroid N, putting any new elements on side i. If N.E ⊆ M.E, the value of i does not matter, so we allow a default value of false, and state lemmas where N.E ⊆ M.E only in terms of P.induce N. In the more general case (for example, if M = N ＼ D), then both values of i are potentially relevant, so we give lemmas more generally in terms of P.induce N i.

Equations

• P.induce N i = Set.IndexedPartition.shift P N.E i

theorem Matroid.Separation.induce_apply_eq_cond {α : Type u_1} {M : Matroid α} {j : Bool} (P : M.Separation) (N : Matroid α) (i : Bool) : (P.induce N i) j = bif j == i then P j ∩ N.E ∪ N.E \ M.E else P j ∩ N.E

@[simp]

theorem Matroid.Separation.induce_apply_not {α : Type u_1} {M : Matroid α} (P : M.Separation) (N : Matroid α) (i : Bool) : ((P.induce N i) !i) = (P !i) ∩ N.E

@[simp]

theorem Matroid.Separation.induce_not_apply {α : Type u_1} {M : Matroid α} (P : M.Separation) (N : Matroid α) (i : Bool) : (P.induce N !i) i = P i ∩ N.E

@[simp]

theorem Matroid.Separation.induce_true_false {α : Type u_1} {M N : Matroid α} {P : M.Separation} : (P.induce N true) false = P false ∩ N.E

@[simp]

theorem Matroid.Separation.induce_false_true {α : Type u_1} {M N : Matroid α} {P : M.Separation} : (P.induce N) true = P true ∩ N.E

theorem Matroid.Separation.induce_apply_self {α : Type u_1} {M N : Matroid α} {i : Bool} {P : M.Separation} : (P.induce N i) i = N.E \ P !i

theorem Matroid.Separation.induce_apply_subset {α : Type u_1} {M N : Matroid α} (P : M.Separation) (hNM : N.E ⊆ M.E) (i j : Bool) : (P.induce N i) j = P j ∩ N.E

theorem Matroid.Separation.induce_eq_induce_of_subset {α : Type u_1} {M N : Matroid α} {i : Bool} (P : M.Separation) (hNM : N.E ⊆ M.E) : P.induce N i = P.induce N

theorem Matroid.Separation.induce_eq_copy {α : Type u_1} {M N : Matroid α} {i : Bool} (P : M.Separation) (hMN : M = N) : P.induce N i = P.copy hMN

@[simp]

theorem Matroid.Separation.copy_induce {α : Type u_1} {M M' : Matroid α} (P : M.Separation) (hM' : M = M') (N : Matroid α) (i : Bool) : (P.copy hM').induce N i = P.induce N i

theorem Matroid.Separation.induce_copy {α : Type u_1} {M N N' : Matroid α} (P : M.Separation) (hN : N = N') (i : Bool) : (P.induce N i).copy hN = P.induce N' i

This looks like it should be a simp lemma, but simp will 'forget' that N = N' with annoying consequences.

theorem Matroid.Separation.induce_symm {α : Type u_1} {M : Matroid α} (P : M.Separation) (N : Matroid α) (i : Bool) : (P.induce N i).symm = P.symm.induce N !i

theorem Matroid.Separation.induce_symm_of_subset {α : Type u_1} {M N : Matroid α} (P : M.Separation) (hNM : N.E ⊆ M.E) : (P.induce N).symm = P.symm.induce N

theorem Matroid.Separation.induce_induce {α : Type u_1} {M N : Matroid α} {i : Bool} {N' : Matroid α} (P : M.Separation) (hN' : N'.E ⊆ N.E) : (P.induce N i).induce N' = P.induce N' i

theorem Matroid.Separation.induce_induce_of_subset {α : Type u_1} {M N N' : Matroid α} (P : M.Separation) {i : Bool} (hss : M.E ⊆ N.E) : (P.induce N i).induce N' i = P.induce N' i

@[simp]

theorem Matroid.Separation.induce_self {α : Type u_1} {M : Matroid α} {i : Bool} (P : M.Separation) : P.induce M i = P

theorem Matroid.Separation.induce_induce_eq_self {α : Type u_1} {M N : Matroid α} (P : M.Separation) (hss : M.E ⊆ N.E) (i : Bool) : (P.induce N i).induce M = P

theorem Matroid.Separation.induce_induce_eq_self_of_subset_union {α : Type u_1} {M N : Matroid α} (P : M.Separation) (hN : N.E ⊆ M.E) {i : Bool} (hi : (P !i) ⊆ N.E) : (P.induce N).induce M i = P

def Matroid.Separation.Trivial {α : Type u_1} {M : Matroid α} (P : M.Separation) : Prop

A separation is trivial if one side is empty.

Equations

• P.Trivial = Set.IndexedPartition.Trivial P

theorem Matroid.Separation.trivial_of_eq_empty {α : Type u_1} {M : Matroid α} {i : Bool} {P : M.Separation} (h : P i = ∅) : P.Trivial

theorem Matroid.Separation.trivial_of_eq_ground {α : Type u_1} {M : Matroid α} {i : Bool} {P : M.Separation} (h : P i = M.E) : P.Trivial

theorem Matroid.Separation.trivial_def {α : Type u_1} {M : Matroid α} {P : M.Separation} : P.Trivial ↔ P false = ∅ ∨ P true = ∅

theorem Matroid.Separation.trivial_def' {α : Type u_1} {M : Matroid α} {P : M.Separation} : P.Trivial ↔ P false = M.E ∨ P true = M.E

theorem Matroid.Separation.Trivial.exists_eq_ground {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.Trivial) : ∃ (i : Bool), P i = M.E

theorem Matroid.Separation.trivial_of_ground_subsingleton {α : Type u_1} {M : Matroid α} (P : M.Separation) (h : M.E.Subsingleton) : P.Trivial

@[simp]

theorem Matroid.Separation.trivial_copy_iff {α : Type u_1} {M M' : Matroid α} (h : M = M') (P : M.Separation) : (P.copy h).Trivial ↔ P.Trivial

def Matroid.Separation.Nontrivial {α : Type u_1} {M : Matroid α} (P : M.Separation) : Prop

A separation is nontrivial if both sides are nonempty

Equations

• P.Nontrivial = Set.IndexedPartition.Nontrivial P

theorem Matroid.Separation.Nontrivial.nonempty {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.Nontrivial) (i : Bool) : (P i).Nonempty

theorem Matroid.Separation.nontrivial_def {α : Type u_1} {M : Matroid α} {P : M.Separation} : P.Nontrivial ↔ (P false).Nonempty ∧ (P true).Nonempty

theorem Matroid.Separation.nontrivial_iff_forall {α : Type u_1} {M : Matroid α} {P : M.Separation} : P.Nontrivial ↔ ∀ (i : Bool), (P i).Nonempty

theorem Matroid.Separation.nontrivial_iff_bool {α : Type u_1} {M : Matroid α} {P : M.Separation} (i : Bool) : P.Nontrivial ↔ (P i).Nonempty ∧ (P !i).Nonempty

@[simp]

theorem Matroid.Separation.not_trivial_iff {α : Type u_1} {M : Matroid α} {P : M.Separation} : ¬P.Trivial ↔ P.Nontrivial

@[simp]

theorem Matroid.Separation.not_nontrivial_iff {α : Type u_1} {M : Matroid α} {P : M.Separation} : ¬P.Nontrivial ↔ P.Trivial

theorem Matroid.Separation.Nontrivial.not_trivial {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.Nontrivial) : ¬P.Trivial

theorem Matroid.Separation.Trivial.not_nontrivial {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.Trivial) : ¬P.Nontrivial

theorem Matroid.Separation.trivial_or_nontrivial {α : Type u_1} {M : Matroid α} (P : M.Separation) : P.Trivial ∨ P.Nontrivial

theorem Matroid.Separation.Nontrivial.ssubset_ground {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.Nontrivial) {i : Bool} : P i ⊂ M.E

@[simp]

theorem Matroid.Separation.nontrivial_copy_iff {α : Type u_1} {M M' : Matroid α} (h : M = M') (P : M.Separation) : (P.copy h).Nontrivial ↔ P.Nontrivial

def Matroid.Separation.map {α : Type u_1} {M : Matroid α} {β : Type u_2} (P : M.Separation) (f : α → β) (hf : Set.InjOn f M.E) : (M.map f hf).Separation

Push a separation forward along a matroid map.

Equations

• P.map f hf = { toFun := fun (i : Bool) => f '' P i, pairwise_disjoint' := ⋯, iUnion_eq' := ⋯ }

@[simp]

theorem Matroid.Separation.map_apply {α : Type u_1} {M : Matroid α} {β : Type u_2} (P : M.Separation) {f : α → β} (hf : Set.InjOn f M.E) (i : Bool) : (P.map f hf) i = f '' P i

@[reducible, inline]

noncomputable abbrev Matroid.Separation.eConn {α : Type u_1} {M : Matroid α} (P : M.Separation) : ℕ∞

The connectivity of a separation of M.

Equations

• P.eConn = M.eLocalConn (P true) (P false)

@[simp]

theorem Matroid.Separation.eConn_symm {α : Type u_1} {M : Matroid α} (P : M.Separation) : P.symm.eConn = P.eConn

@[simp]

theorem Matroid.Separation.eConn_bSymm {α : Type u_1} {M : Matroid α} (P : M.Separation) (b : Bool) : (P.bSymm b).eConn = P.eConn

@[simp]

theorem Matroid.Separation.eConn_copy {α : Type u_1} {M M' : Matroid α} (P : M.Separation) (h_eq : M = M') : (P.copy h_eq).eConn = P.eConn

@[simp]

theorem Matroid.Separation.eConn_eq {α : Type u_1} {M : Matroid α} (P : M.Separation) (i : Bool) : ↑M.eConn (P i) = P.eConn

theorem Matroid.Separation.eConn_eq_eLocalConn_true_false {α : Type u_1} {M : Matroid α} (P : M.Separation) : P.eConn = M.eLocalConn (P true) (P false)

theorem Matroid.Separation.eConn_eq_eLocalConn {α : Type u_1} {M : Matroid α} (P : M.Separation) (i : Bool) : P.eConn = M.eLocalConn (P i) (P !i)

theorem Matroid.Separation.eConn_eq_eLocalConn_of_isRestriction {α : Type u_1} {M N : Matroid α} (P : N.Separation) (hNM : N.IsRestriction M) (i : Bool) : P.eConn = M.eLocalConn (P i) (P !i)

@[simp]

theorem Matroid.Separation.induce_dual_apply {α : Type u_1} {M : Matroid α} (P : M.Separation) (i : Bool) : (P.induce M✶) i = P i

@[simp]

theorem Matroid.Separation.induce_of_dual_apply {α : Type u_1} {M : Matroid α} (P : M✶.Separation) (i : Bool) : (P.induce M) i = P i

@[simp]

theorem Matroid.Separation.induce_induce_dual {α : Type u_1} {M : Matroid α} (P : M.Separation) (N : Matroid α) (i : Bool) : (P.induce N i).induce N✶ = P.induce N✶ i

@[simp]

theorem Matroid.Separation.induce_dual_induce_self {α : Type u_1} {M : Matroid α} (P : M.Separation) (N : Matroid α) (i : Bool) : (P.induce N✶ i).induce N = P.induce N i

@[simp]

theorem Matroid.Separation.induce_induce_bDual {α : Type u_1} {M : Matroid α} (P : M.Separation) (N : Matroid α) (i b : Bool) : (P.induce N i).induce (N.bDual b) = P.induce (N.bDual b) i

@[simp]

theorem Matroid.Separation.induce_bDual_induce {α : Type u_1} {M : Matroid α} (P : M.Separation) (N : Matroid α) (i b : Bool) : (P.induce (N.bDual b) i).induce N = P.induce N i

@[simp]

theorem Matroid.Separation.induce_bDual_apply {α : Type u_1} {M : Matroid α} (P : M.Separation) (b i : Bool) : (P.induce (M.bDual b)) i = P i

@[simp]

theorem Matroid.Separation.eConn_induce_dual {α : Type u_1} {M : Matroid α} (P : M.Separation) : (P.induce M✶).eConn = P.eConn

@[simp]

theorem Matroid.Separation.eConn_induce_of_dual {α : Type u_1} {M : Matroid α} (P : M✶.Separation) : (P.induce M).eConn = P.eConn

@[simp]

theorem Matroid.Separation.induce_dual_eConn {α : Type u_1} {M : Matroid α} {i : Bool} (P : M.Separation) (N : Matroid α) : (P.induce N✶ i).eConn = (P.induce N i).eConn

@[simp]

theorem Matroid.Separation.induce_dual_induce {α : Type u_1} {M : Matroid α} (P : M.Separation) (N : Matroid α) (i : Bool) : (P.induce M✶).induce N i = P.induce N i

@[simp]

theorem Matroid.Separation.eConn_induce_bDual {α : Type u_1} {M : Matroid α} (P : M.Separation) (b : Bool) : (P.induce (M.bDual b)).eConn = P.eConn

theorem Matroid.Separation.Trivial.eConn {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.Trivial) : P.eConn = 0

@[simp]

theorem Matroid.Separation.map_eConn {α : Type u_1} {M : Matroid α} {β : Type u_2} (P : M.Separation) (f : α → β) (hf : Set.InjOn f M.E) : (P.map f hf).eConn = P.eConn

@[simp]

theorem Matroid.Separation.not_indep_iff {α : Type u_1} {M : Matroid α} {i : Bool} {P : M.Separation} : ¬M.Indep (P i) ↔ M.Dep (P i)

@[simp]

theorem Matroid.Separation.not_dep_iff {α : Type u_1} {M : Matroid α} {i : Bool} {P : M.Separation} : ¬M.Dep (P i) ↔ M.Indep (P i)

@[simp]

theorem Matroid.Separation.not_coindep_iff {α : Type u_1} {M : Matroid α} {i : Bool} {P : M.Separation} : ¬M.Coindep (P i) ↔ M.Codep (P i)

@[simp]

theorem Matroid.Separation.not_codep_iff {α : Type u_1} {M : Matroid α} {i : Bool} {P : M.Separation} : ¬M.Codep (P i) ↔ M.Coindep (P i)

@[simp]

theorem Matroid.Separation.not_indep_dual_iff {α : Type u_1} {M : Matroid α} {i : Bool} {P : M.Separation} : ¬M✶.Indep (P i) ↔ M.Codep (P i)

@[simp]

theorem Matroid.Separation.not_spanning_iff {α : Type u_1} {M : Matroid α} {i : Bool} {P : M.Separation} : ¬M.Spanning (P i) ↔ M.Nonspanning (P i)

@[simp]

theorem Matroid.Separation.not_nonspanning_iff {α : Type u_1} {M : Matroid α} {i : Bool} {P : M.Separation} : ¬M.Nonspanning (P i) ↔ M.Spanning (P i)

theorem Matroid.Separation.coindep_not_iff {α : Type u_1} {M : Matroid α} {i : Bool} {P : M.Separation} : M.Coindep (P !i) ↔ M.Spanning (P i)

theorem Matroid.Separation.codep_not_iff {α : Type u_1} {M : Matroid α} {i : Bool} {P : M.Separation} : M.Codep (P !i) ↔ M.Nonspanning (P i)

theorem Matroid.Separation.nonspanning_not_iff {α : Type u_1} {M : Matroid α} {i : Bool} {P : M.Separation} : M.Nonspanning (P !i) ↔ M.Codep (P i)

theorem Matroid.Separation.spanning_not_iff {α : Type u_1} {M : Matroid α} {i : Bool} {P : M.Separation} : M.Spanning (P !i) ↔ M.Coindep (P i)

theorem Matroid.Separation.isCocircuit_not_iff {α : Type u_1} {M : Matroid α} {i : Bool} {P : M.Separation} : M.IsCocircuit (P !i) ↔ M.IsHyperplane (P i)

theorem Matroid.Separation.isHyperplane_not_iff {α : Type u_1} {M : Matroid α} {i : Bool} {P : M.Separation} : M.IsHyperplane (P !i) ↔ M.IsCocircuit (P i)

theorem Matroid.Separation.spanning_dual_iff {α : Type u_1} {M : Matroid α} {i : Bool} {P : M.Separation} : M✶.Spanning (P i) ↔ M.Indep (P !i)

theorem Matroid.Separation.nonspanning_dual_iff {α : Type u_1} {M : Matroid α} {i : Bool} {P : M.Separation} : M✶.Nonspanning (P i) ↔ M.Dep (P !i)

noncomputable def Matroid.Separation.conn {α : Type u_1} {M : Matroid α} (P : M.Separation) : ℕ

The connectivity of a separation as a natural number. Takes a value of 0 if infinite.

Equations

• P.conn = M.localConn (P true) (P false)

@[simp]

theorem Matroid.Separation.conn_symm {α : Type u_1} {M : Matroid α} (P : M.Separation) : P.symm.conn = P.conn

def Matroid.Separation.setCompl {α : Type u_1} (M : Matroid α) [M.OnUniv] (X : Set α) : M.Separation

Equations

• Matroid.Separation.setCompl M X = Matroid.Separation.mk' X Xᶜ ⋯ ⋯

@[simp]

theorem Matroid.Separation.setCompl_apply {α : Type u_1} (M : Matroid α) [M.OnUniv] (X : Set α) (i : Bool) : (Separation.setCompl M X) i = bif i then X else Xᶜ

def Matroid.ofSetSep {α : Type u_1} (M : Matroid α) (A : Set α) (i : Bool) (hA : A ⊆ M.E := by aesop_mat) : M.Separation

The separation of M given by a subset of M.E and its complement. The elements of the set go on side b.

Equations

• M.ofSetSep A i hA = Set.IndexedPartition.ofSubset hA i

@[simp]

theorem Matroid.ofSetSep_apply {α : Type u_1} (M : Matroid α) (A : Set α) (i : Bool) (hA : A ⊆ M.E := by aesop_mat) (j : Bool) : (M.ofSetSep A i hA) j = bif j == i then A else M.E \ A

@[simp]

theorem Matroid.ofSetSep_apply_self {α : Type u_1} {M : Matroid α} {A : Set α} {i : Bool} (hA : A ⊆ M.E) : (M.ofSetSep A i hA) i = A

@[simp]

theorem Matroid.ofSetSep_apply_not {α : Type u_1} {M : Matroid α} {A : Set α} {i : Bool} (hA : A ⊆ M.E) : ((M.ofSetSep A i hA) !i) = M.E \ A

@[simp]

theorem Matroid.ofSetSep_not_apply {α : Type u_1} {M : Matroid α} {A : Set α} {i : Bool} (hA : A ⊆ M.E) : (M.ofSetSep A (!i) hA) i = M.E \ A

@[simp]

theorem Matroid.ofSetSep_true_false {α : Type u_1} {M : Matroid α} {A : Set α} (hA : A ⊆ M.E) : (M.ofSetSep A true hA) false = M.E \ A

@[simp]

theorem Matroid.ofSetSep_false_true {α : Type u_1} {M : Matroid α} {A : Set α} (hA : A ⊆ M.E) : (M.ofSetSep A false hA) true = M.E \ A

@[simp]

theorem Matroid.eConn_ofSetSep {α : Type u_1} {M : Matroid α} {A : Set α} {i : Bool} (hA : A ⊆ M.E) : (M.ofSetSep A i hA).eConn = ↑M.eConn A

def Matroid.ofSumSep {α : Type u_2} {β : Type u_3} (M : Matroid (α ⊕ β)) : M.Separation

The natural separation of a matroid on a sum type, where the false side is the first summand.

Equations

• M.ofSumSep = M.ofSetSep (Set.range Sum.inl ∩ M.E) false ⋯

@[simp]

theorem Matroid.ofSumSep_apply_false {α : Type u_2} {β : Type u_3} (M : Matroid (α ⊕ β)) : M.ofSumSep false = Set.range Sum.inl ∩ M.E

@[simp]

theorem Matroid.ofSumSep_apply_true {α : Type u_2} {β : Type u_3} (M : Matroid (α ⊕ β)) : M.ofSumSep true = Set.range Sum.inr ∩ M.E

def Matroid.Separation.disjointSumSep {α : Type u_1} (M N : Matroid α) (hMN : Disjoint M.E N.E) : (M.disjointSum N hMN).Separation

The natural separation of a disjoint sum of two matroids, where the first summand is the false side.

Equations

• Matroid.Separation.disjointSumSep M N hMN = (M.disjointSum N hMN).ofSetSep M.E false ⋯

@[simp]

theorem Matroid.Separation.disjointSumSep_apply_false {α : Type u_1} {M N : Matroid α} (hMN : Disjoint M.E N.E) : (disjointSumSep M N hMN) false = M.E

@[simp]

theorem Matroid.Separation.disjointSumSep_apply_true {α : Type u_1} {M N : Matroid α} (hMN : Disjoint M.E N.E) : (disjointSumSep M N hMN) true = N.E

theorem Matroid.Separation.Trivial.exists_eq {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.Trivial) : ∃ (i : Bool), P = M.ofSetSep ∅ i ⋯

theorem Matroid.Separation.exists_larger_side {α : Type u_1} {M : Matroid α} {β : Type u_2} [ConditionallyCompleteLinearOrder β] (P : M.Separation) (f : Set α → β) : ∃ (i : Bool), ∀ (j : Bool), f (P j) ≤ f (P i)

Every separation has a larger side for a given numerical notion of 'large'

theorem Matroid.Separation.exists_smaller_side {α : Type u_1} {M : Matroid α} {β : Type u_2} [ConditionallyCompleteLinearOrder β] (P : M.Separation) (f : Set α → β) : ∃ (i : Bool), ∀ (j : Bool), f (P i) ≤ f (P j)

For any two separations, one of the four cells obtained by intersecting them is the smaller one, for a given numerical notion of 'small'.

theorem Matroid.Separation.exists_largest_inter {α : Type u_1} {M N : Matroid α} {β : Type u_2} [ConditionallyCompleteLinearOrder β] (P : M.Separation) (Q : N.Separation) (f : Set α → β) : ∃ (i : Bool) (i' : Bool), ∀ (j j' : Bool), f (P j ∩ Q j') ≤ f (P i ∩ Q i')

For any two separations, one of the four cells obtained by intersecting them is the largest one, for a given numerical notion of 'large'.

theorem Matroid.Separation.exists_smallest_inter {α : Type u_1} {M N : Matroid α} {β : Type u_2} [ConditionallyCompleteLinearOrder β] (P : M.Separation) (Q : N.Separation) (f : Set α → β) : ∃ (i : Bool) (i' : Bool), ∀ (j j' : Bool), f (P i ∩ Q i') ≤ f (P j ∩ Q j')

For any two separations, one of the four cells obtained by intersecting them is the smallest one, for a given numerical notion of small'.

def Matroid.Separation.cross {α : Type u_1} {M : Matroid α} (P Q : M.Separation) (b c i : Bool) : M.Separation

The separation of M whose i side is (P b ∩ Q c) and whose !i side is (P !b ∪ Q !c).

Equations

• P.cross Q b c i = Set.IndexedPartition.cross P Q b c i

theorem Matroid.Separation.cross_apply {α : Type u_1} {M : Matroid α} {b c i j : Bool} (P Q : M.Separation) : (P.cross Q b c i) j = bif j == i then P b ∩ Q c else (P !b) ∪ Q !c

@[simp]

theorem Matroid.Separation.cross_symm {α : Type u_1} {M : Matroid α} (P Q : M.Separation) (b c i : Bool) : (P.cross Q b c i).symm = P.cross Q b c !i

@[simp]

theorem Matroid.Separation.cross_symm_left {α : Type u_1} {M : Matroid α} (P Q : M.Separation) (b c i : Bool) : P.symm.cross Q b c i = P.cross Q (!b) c i

@[simp]

theorem Matroid.Separation.cross_symm_right {α : Type u_1} {M : Matroid α} (P Q : M.Separation) (b c i : Bool) : P.cross Q.symm b c i = P.cross Q b (!c) i

@[simp]

theorem Matroid.Separation.cross_bSymm_left {α : Type u_1} {M : Matroid α} (P Q : M.Separation) (b b' c i : Bool) : (P.bSymm b').cross Q b c i = P.cross Q (b != b') c i

@[simp]

theorem Matroid.Separation.cross_bSymm_right {α : Type u_1} {M : Matroid α} (P Q : M.Separation) (b c c' i : Bool) : P.cross (Q.bSymm c') b c i = P.cross Q b (c != c') i

@[simp]

theorem Matroid.Separation.cross_bSymm {α : Type u_1} {M : Matroid α} (P Q : M.Separation) (b c i j : Bool) : (P.cross Q b c i).bSymm j = P.cross Q b c (i != j)

@[simp]

theorem Matroid.Separation.cross_apply_self {α : Type u_1} {M : Matroid α} {b c i : Bool} (P Q : M.Separation) : (P.cross Q b c i) i = P b ∩ Q c

@[simp]

theorem Matroid.Separation.cross_apply_not {α : Type u_1} {M : Matroid α} {b c i : Bool} (P Q : M.Separation) : ((P.cross Q b c i) !i) = (P !b) ∪ Q !c

@[simp]

theorem Matroid.Separation.cross_not_apply {α : Type u_1} {M : Matroid α} {b c i : Bool} (P Q : M.Separation) : (P.cross Q b c !i) i = (P !b) ∪ Q !c

@[simp]

theorem Matroid.Separation.cross_apply_true_false {α : Type u_1} {M : Matroid α} {b c : Bool} (P Q : M.Separation) : (P.cross Q b c true) false = (P !b) ∪ Q !c

@[simp]

theorem Matroid.Separation.cross_apply_false_true {α : Type u_1} {M : Matroid α} {b c : Bool} (P Q : M.Separation) : (P.cross Q b c false) true = (P !b) ∪ Q !c

theorem Matroid.Separation.cross_comm {α : Type u_1} {M : Matroid α} {i : Bool} (P Q : M.Separation) (b c : Bool) : P.cross Q b c i = Q.cross P c b i

theorem Matroid.Separation.induce_cross {α : Type u_1} {M N : Matroid α} (P Q : M.Separation) (b c i j : Bool) (hNM : N.E ⊆ M.E) : (P.cross Q b c i).induce N = (P.induce N).cross (Q.induce N) b c i

def Matroid.Separation.interCross {α : Type u_1} {M : Matroid α} (P Q : M.Separation) : M.Separation

The bipartition whose true side is P true ∩ Q true and whose false side is P false ∪ Q false

Equations

• P.interCross Q = P.cross Q true true true

def Matroid.Separation.unionCross {α : Type u_1} {M : Matroid α} (P Q : M.Separation) : M.Separation

The bipartition whose true side is P true ∪ Q true and whose false side is P false ∩ Q false

Equations

• P.unionCross Q = P.cross Q false false false

@[simp]

theorem Matroid.Separation.interCross_apply_true {α : Type u_1} {M : Matroid α} (P Q : M.Separation) : (P.interCross Q) true = P true ∩ Q true

@[simp]

theorem Matroid.Separation.interCross_apply_false {α : Type u_1} {M : Matroid α} (P Q : M.Separation) : (P.interCross Q) false = P false ∪ Q false

@[simp]

theorem Matroid.Separation.unionCross_apply_true {α : Type u_1} {M : Matroid α} (P Q : M.Separation) : (P.unionCross Q) true = P true ∪ Q true

@[simp]

theorem Matroid.Separation.unionCross_apply_false {α : Type u_1} {M : Matroid α} (P Q : M.Separation) : (P.unionCross Q) false = P false ∩ Q false

@[simp]

theorem Matroid.Separation.unionCross_symm {α : Type u_1} {M : Matroid α} (P Q : M.Separation) : (P.unionCross Q).symm = P.symm.interCross Q.symm

@[simp]

theorem Matroid.Separation.interCross_symm {α : Type u_1} {M : Matroid α} (P Q : M.Separation) : (P.interCross Q).symm = P.symm.unionCross Q.symm

theorem Matroid.Separation.interCross_comm {α : Type u_1} {M : Matroid α} (P Q : M.Separation) : P.interCross Q = Q.interCross P

theorem Matroid.Separation.unionCross_comm {α : Type u_1} {M : Matroid α} (P Q : M.Separation) : P.unionCross Q = Q.unionCross P

theorem Matroid.Separation.Nontrivial.cross_trivial_iff {α : Type u_1} {M : Matroid α} {P Q : M.Separation} (hP : P.Nontrivial) (b c i : Bool) : (P.cross Q b c i).Trivial ↔ P b ⊆ Q !c ∨ Q c ⊆ P !b

theorem Matroid.Separation.cross_trivial_iff {α : Type u_1} {M : Matroid α} {i : Bool} (P Q : M.Separation) (b c : Bool) : (P.cross Q b c i).Trivial ↔ P b ⊆ Q !c ∨ Q c ⊆ P !b ∨ P b = M.E ∧ Q c = M.E

theorem Matroid.Separation.submod_cross {α : Type u_1} {M : Matroid α} (P Q : M.Separation) (b c i j : Bool) : (P.cross Q b c i).eConn + (P.cross Q (!b) (!c) j).eConn ≤ P.eConn + Q.eConn

theorem Matroid.Separation.submod_cross' {α : Type u_1} {M : Matroid α} (P Q : M.Separation) (b c i j : Bool) : (P.cross Q b (!c) i).eConn + (P.cross Q (!b) c j).eConn ≤ P.eConn + Q.eConn

theorem Matroid.Separation.submod_interCross_unionCross {α : Type u_1} {M : Matroid α} (P Q : M.Separation) : (P.interCross Q).eConn + (P.unionCross Q).eConn ≤ P.eConn + Q.eConn

@[simp]

theorem Matroid.Separation.disjoint_inter_right {α : Type u_1} {M : Matroid α} {X Y : Set α} (P : M.Separation) : Disjoint (P true ∩ X) (P false ∩ Y)

@[simp]

theorem Matroid.Separation.disjoint_inter_left {α : Type u_1} {M : Matroid α} {X Y : Set α} (P : M.Separation) : Disjoint (X ∩ P true) (Y ∩ P false)

@[simp]

theorem Matroid.Separation.disjoint_bool_inter_right {α : Type u_1} {M : Matroid α} {X Y : Set α} (P : M.Separation) (i : Bool) : Disjoint (P i ∩ X) ((P !i) ∩ Y)

@[simp]

theorem Matroid.Separation.disjoint_bool_inter_left {α : Type u_1} {M : Matroid α} {X Y : Set α} (P : M.Separation) (i : Bool) : Disjoint (X ∩ P i) (Y ∩ P !i)

@[simp]

theorem Matroid.Separation.disjoint_bool_inter_right' {α : Type u_1} {M : Matroid α} {X Y : Set α} (P : M.Separation) (i : Bool) : Disjoint ((P !i) ∩ X) (P i ∩ Y)

@[simp]

theorem Matroid.Separation.disjoint_bool_inter_left' {α : Type u_1} {M : Matroid α} {X Y : Set α} (P : M.Separation) (i : Bool) : Disjoint (X ∩ P !i) (Y ∩ P i)

@[simp]

theorem Matroid.Separation.inter_ground_eq {α : Type u_1} {M : Matroid α} (P : M.Separation) (i : Bool) : P i ∩ M.E = P i

theorem Matroid.Separation.union_inter_right' {α : Type u_1} {M : Matroid α} (P : M.Separation) (X : Set α) (i : Bool) : P i ∩ X ∪ (P !i) ∩ X = X ∩ M.E

theorem Matroid.Separation.union_inter_left' {α : Type u_1} {M : Matroid α} (P : M.Separation) (X : Set α) (i : Bool) : (X ∩ P i ∪ X ∩ P !i) = X ∩ M.E

@[simp]

theorem Matroid.Separation.union_inter_right {α : Type u_1} {M : Matroid α} (P : M.Separation) (X : Set α) (hX : X ⊆ M.E := by aesop_mat) (i : Bool) : P i ∩ X ∪ (P !i) ∩ X = X

@[simp]

theorem Matroid.Separation.union_inter_left {α : Type u_1} {M : Matroid α} (P : M.Separation) (X : Set α) (hX : X ⊆ M.E := by aesop_mat) (i : Bool) : (X ∩ P i ∪ X ∩ P !i) = X

theorem Matroid.Separation.diff_eq_inter_bool {α : Type u_1} {M : Matroid α} {X : Set α} (P : M.Separation) (i : Bool) (hX : X ⊆ M.E := by aesop_mat) : X \ P i = X ∩ P !i

def Matroid.Separation.toggle {α : Type u_1} {M : Matroid α} (P : M.Separation) (X : Set α) : M.Separation

Equations

• P.toggle X = { toFun := fun (i : Bool) => symmDiff (P i) (X ∩ M.E), pairwise_disjoint' := ⋯, iUnion_eq' := ⋯ }

theorem Matroid.Separation.toggle_apply' {α : Type u_1} {M : Matroid α} (P : M.Separation) (X : Set α) (i : Bool) : (P.toggle X) i = symmDiff (P i) (X ∩ M.E)

theorem Matroid.Separation.toggle_apply {α : Type u_1} {M : Matroid α} {X : Set α} (P : M.Separation) (hX : X ⊆ M.E := by aesop_mat) (i : Bool) : (P.toggle X) i = symmDiff (P i) X

@[simp]

theorem Matroid.Separation.toggle_inter_ground {α : Type u_1} {M : Matroid α} (P : M.Separation) (X : Set α) : P.toggle (X ∩ M.E) = P.toggle X

theorem Matroid.Separation.toggle_apply_eq_diff {α : Type u_1} {M : Matroid α} {X : Set α} {i : Bool} (P : M.Separation) (hX : X ⊆ P i) : (P.toggle X) i = P i \ X

theorem Matroid.Separation.toggle_apply_eq_union {α : Type u_1} {M : Matroid α} {X : Set α} {i : Bool} (P : M.Separation) (hX : X ⊆ P !i) : (P.toggle X) i = P i ∪ X

@[simp]

theorem Matroid.Separation.toggle_empty {α : Type u_1} {M : Matroid α} (P : M.Separation) : P.toggle ∅ = P

theorem Matroid.Separation.toggle_induce_of_inter_subset {α : Type u_1} {M N : Matroid α} {X : Set α} {i : Bool} (P : M.Separation) (hX : X ∩ N.E ⊆ M.E) : (P.toggle X).induce N i = (P.induce N i).toggle X

theorem Matroid.Separation.toggle_induce_of_ground_subset {α : Type u_1} {M N : Matroid α} {X : Set α} (P : M.Separation) (hN : N.E ⊆ M.E) : (P.toggle X).induce N = (P.induce N).toggle X

theorem Matroid.Separation.toggle_induce {α : Type u_1} {M N : Matroid α} {X : Set α} {i : Bool} (P : M.Separation) (hX : X ⊆ M.E := by aesop_mat) : (P.toggle X).induce N i = (P.induce N i).toggle X

theorem Matroid.Separation.eConn_eq_zero_iff_skew {α : Type u_1} {M : Matroid α} {P : M.Separation} {i : Bool} : P.eConn = 0 ↔ M.Skew (P i) (P !i)

theorem Matroid.Separation.eConn_eq_zero_iff_eq_disjointSum {α : Type u_1} {M : Matroid α} {P : M.Separation} {i : Bool} : P.eConn = 0 ↔ M = (M.restrict (P i)).disjointSum (M.restrict (P !i)) ⋯

@[simp]

theorem Matroid.Separation.disjointSumSep_eConn {α : Type u_1} {M N : Matroid α} (hMN : Disjoint M.E N.E) : (disjointSumSep M N hMN).eConn = 0

theorem Matroid.exists_separation_of_not_connected {α : Type u_1} {M : Matroid α} [M.Nonempty] (h : ¬M.Connected) : ∃ (P : M.Separation), P.eConn = 0 ∧ P.Nontrivial

theorem Matroid.exists_separation_iff_not_connected {α : Type u_1} {M : Matroid α} [M.Nonempty] : ¬M.Connected ↔ ∃ (P : M.Separation), P.eConn = 0 ∧ P.Nontrivial

theorem Matroid.connected_iff_forall_separation {α : Type u_1} {M : Matroid α} [M.Nonempty] : M.Connected ↔ ∀ (P : M.Separation), P.eConn = 0 → P.Trivial

theorem Matroid.Connected.trivial_of_eConn_eq_zero {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : M.Connected) (hP : P.eConn = 0) : P.Trivial

theorem Matroid.Connected.eq_ground_of_eConn_eq_zero {α : Type u_1} {M : Matroid α} {X : Set α} (hM : M.Connected) (hX : ↑M.eConn X = 0) (hne : X.Nonempty) (hXE : X ⊆ M.E := by aesop_mat) : X = M.E

theorem Matroid.Separation.Nontrivial.one_le_eConn_of_connected {α : Type u_1} {M : Matroid α} {P : M.Separation} (hP : P.Nontrivial) (hM : M.Connected) : 1 ≤ P.eConn

@[simp]

theorem Matroid.Separation.sum_ofSumSep_eConn {α : Type u_2} {β : Type u_3} (M : Matroid α) (N : Matroid β) : (M.sum N).ofSumSep.eConn = 0