theorem disjoint_map_prod_right {α : Type u_1} {ι : Type u_2} {f : ι → Set α} : Pairwise (Function.onFun Disjoint fun (i : ι) => (fun (x : α) => (x, i)) '' f i)

theorem disjoint_map_prod_left {α : Type u_1} {ι : Type u_2} {f : ι → Set α} : Pairwise (Function.onFun Disjoint fun (i : ι) => (fun (x : α) => (i, x)) '' f i)

theorem injOn_prod_fst_mk_left_iff_pairwise_disjoint {α : Type u_1} {ι : Type u_2} (f : ι → Set α) : Set.InjOn Prod.fst (⋃ (i : ι), (fun (x : α) => (x, i)) '' f i) ↔ Pairwise (Function.onFun Disjoint f)

noncomputable def Matroid.multiConnAux {α : Type u_1} {ι : Type u_2} (M : Matroid α) (X : ι → Set α) : ℕ∞

An auxiliary version of multi-connectivity used in the real definition. If the sets are disjoint, then this is equal to multiConn, but otherwise it is badly behaved.

Equations

• M.multiConnAux X = ⨅ (I : { I : ι → Set α // ∀ (i : ι), M.IsBasis' (I i) (X i) }), M.nullity (⋃ (i : ι), ↑I i)

noncomputable def Matroid.multiConn {α : Type u_1} {ι : Type u_2} (M : Matroid α) (X : ι → Set α) : ℕ∞

The local connectivity of an indexed collection X : ι → Set α of sets. This is defined indirectly using comaps so that it is meaningful even when the X are not disjoint. If they are disjoint, it is equal to M.nullity (⋃ i, I i) for any bases I i for the X i; see multiConn_eq_nullity_iUnion. If the union of the X i has finite rank, then this is equal to ∑' i, r (X i) - r (⋃ i, X i). If the X i are not disjoint, and the rank of their union is infinite, then there is no simple formula in general, but for pairs, an expression using cardinality is given in multiConn_cond.

Equations

• M.multiConn X = (M.comap Prod.fst).multiConnAux fun (i : ι) => (fun (x : α) => (x, i)) '' (X i ∩ M.E)

theorem Matroid.multiConn_inter_ground {α : Type u_1} {ι : Type u_2} (M : Matroid α) (X : ι → Set α) : (M.multiConn fun (i : ι) => X i ∩ M.E) = M.multiConn X

theorem Matroid.multiConn_inter_ground_congr {α : Type u_1} {M : Matroid α} {ι : Type u_2} {X Y : ι → Set α} (hXY : ∀ (i : ι), X i ∩ M.E = Y i ∩ M.E) : M.multiConn X = M.multiConn Y

theorem Matroid.multiConn_eq_comap_nullity {α : Type u_1} {M : Matroid α} {ι : Type u_2} {I X : ι → Set α} (h : ∀ (i : ι), M.IsBasis' (I i) (X i)) : M.multiConn X = (M.comap Prod.fst).nullity (⋃ (i : ι), (fun (x : α) => (x, i)) '' I i)

theorem Matroid.multiConn_eq_nullity_iUnion_add_tsum {α : Type u_1} {M : Matroid α} {ι : Type u_2} {I X : ι → Set α} (hI : ∀ (i : ι), M.IsBasis' (I i) (X i)) : M.multiConn X = M.nullity (⋃ (i : ι), I i) + ∑' (e : ↑(⋃ (i : ι), I i)), ({i : ι | ↑e ∈ I i}.encard - 1)

theorem Matroid.multiConn_eq_nullity_iUnion_add_tsum' {α : Type u_1} {M : Matroid α} {ι : Type u_2} {I X : ι → Set α} (hI : ∀ (i : ι), M.IsBasis' (I i) (X i)) : M.multiConn X = M.nullity (⋃ (i : ι), I i) + ∑' (e : α), ({i : ι | e ∈ I i}.encard - 1)

theorem Matroid.multiConn_eq_nullity_iUnion' {α : Type u_1} {M : Matroid α} {ι : Type u_2} {I X : ι → Set α} (hdj : Pairwise (Function.onFun Disjoint I)) (hIX : ∀ (i : ι), M.IsBasis' (I i) (X i)) : M.multiConn X = M.nullity (⋃ (i : ι), I i)

theorem Matroid.multiConn_eq_nullity_iUnion {α : Type u_1} {M : Matroid α} {ι : Type u_2} {I X : ι → Set α} (hdj : Pairwise (Function.onFun Disjoint I)) (hIX : ∀ (i : ι), M.IsBasis (I i) (X i)) : M.multiConn X = M.nullity (⋃ (i : ι), I i)

theorem Matroid.multiConn_eq_nullity_iUnion'' {α : Type u_1} {M : Matroid α} {ι : Type u_2} {I X : ι → Set α} (hdj : Pairwise (Function.onFun Disjoint X)) (hIX : ∀ (i : ι), M.IsBasis' (I i) (X i)) : M.multiConn X = M.nullity (⋃ (i : ι), I i)

@[simp]

theorem Matroid.multiConn_subsingleton {α : Type u_1} {ι : Type u_2} [Subsingleton ι] (M : Matroid α) (X : ι → Set α) : M.multiConn X = 0

@[simp]

theorem Matroid.multiConn_const {α : Type u_1} {ι : Type u_2} (M : Matroid α) (X : Set α) : (M.multiConn fun (x : ι) => X) = (ENat.card ι - 1) * M.eRk X

theorem Matroid.multiconn_eq_comap_prod_multiConn {α : Type u_1} {M : Matroid α} {ι : Type u_2} (X : ι → Set α) : M.multiConn X = (M.comap Prod.fst).multiConn fun (i : ι) => (fun (x : α) => (x, i)) '' X i

theorem Matroid.multiConn_mono {α : Type u_1} {ι : Type u_2} {X Y : ι → Set α} (M : Matroid α) (hXY : ∀ (i : ι), X i ⊆ Y i) : M.multiConn X ≤ M.multiConn Y

theorem Matroid.multiConn_map_image {α : Type u_1} {ι : Type u_2} {β : Type u_3} {f : α → β} (M : Matroid α) (hf : Set.InjOn f M.E) (X : ι → Set α) (hXE : ∀ (i : ι), X i ⊆ M.E) : ((M.map f hf).multiConn fun (i : ι) => f '' X i) = M.multiConn X

@[simp]

theorem Matroid.multiConn_map {α : Type u_1} {ι : Type u_2} {β : Type u_3} {f : α → β} (M : Matroid α) (hf : Set.InjOn f M.E) (X : ι → Set β) : (M.map f hf).multiConn X = M.multiConn fun (i : ι) => f ⁻¹' X i

instance Matroid.instInvariantFunForallSetENatMultiConn {ι : Type u_2} : InvariantFun (fun {α : Type u_3} => multiConn) fun {β : Type u_4} => multiConn

theorem Matroid.multiConn_closure {α : Type u_1} {ι : Type u_2} (M : Matroid α) (X : ι → Set α) : (M.multiConn fun (i : ι) => M.closure (X i)) = M.multiConn X

theorem Matroid.multiConn_closure_congr {α : Type u_1} {M : Matroid α} {ι : Type u_2} {X Y : ι → Set α} (hXY : ∀ (i : ι), M.closure (X i) = M.closure (Y i)) : M.multiConn X = M.multiConn Y

@[simp]

theorem Matroid.multiConn_comap {α : Type u_1} {ι : Type u_2} {β : Type u_3} (M : Matroid β) (X : ι → Set α) (f : α → β) : (M.comap f).multiConn X = M.multiConn fun (i : ι) => f '' X i

theorem Matroid.IsSkewFamily.multiConn {α : Type u_1} {M : Matroid α} {ι : Type u_2} {X : ι → Set α} (h : M.IsSkewFamily X) : M.multiConn X = 0

theorem Matroid.multiConn_eq_zero_iff {α : Type u_1} {M : Matroid α} {ι : Type u_2} {X : ι → Set α} (hX : ∀ (i : ι), X i ⊆ M.E) : M.multiConn X = 0 ↔ M.IsSkewFamily X

theorem Matroid.multiConn_eq_zero_iff' {α : Type u_1} {M : Matroid α} {ι : Type u_2} {X : ι → Set α} (hX : ⋃ (i : ι), X i = M.E) : M.multiConn X = 0 ↔ M.IsSkewFamily X

A version of multiConn_eq_zero_iff where the union is M.E, since this is a common application

theorem Matroid.tsum_eRk_eq_eRk_iUnion_add_multiConn {α : Type u_1} {M : Matroid α} {ι : Type u_2} {X : ι → Set α} : ∑' (i : ι), M.eRk (X i) = M.eRk (⋃ (i : ι), X i) + M.multiConn X

theorem Matroid.multiConn_restrict {α : Type u_1} {ι : Type u_2} (M : Matroid α) (X : ι → Set α) (R : Set α) : (M.restrict R).multiConn X = M.multiConn fun (i : ι) => X i ∩ R

theorem Matroid.multiConn_restrict_of_subset {α : Type u_1} {ι : Type u_2} {X : ι → Set α} (M : Matroid α) {R : Set α} (hX : ∀ (i : ι), X i ⊆ R) : (M.restrict R).multiConn X = M.multiConn X

theorem Matroid.multiConn_restrict_le {α : Type u_1} {ι : Type u_2} (M : Matroid α) (X : ι → Set α) (R : Set α) : ((M.restrict R).multiConn fun (i : ι) => X i ∩ R) ≤ M.multiConn X

theorem Matroid.multiConn_delete {α : Type u_1} {ι : Type u_2} (M : Matroid α) (X : ι → Set α) (D : Set α) : (M.delete D).multiConn X = M.multiConn fun (i : ι) => X i \ D

theorem Matroid.IsRestriction.multiConn {α : Type u_1} {M : Matroid α} {ι : Type u_2} {X : ι → Set α} {N : Matroid α} (hNM : N.IsRestriction M) : N.multiConn X = M.multiConn fun (i : ι) => X i ∩ N.E

theorem Matroid.IsRestriction.multiConn_of_subset {α : Type u_1} {M : Matroid α} {ι : Type u_2} {X : ι → Set α} {N : Matroid α} (hNM : N.IsRestriction M) (hX : ∀ (i : ι), X i ⊆ N.E) : N.multiConn X = M.multiConn X

theorem Matroid.multiConn_delete_of_disjoint {α : Type u_1} {ι : Type u_2} {X : ι → Set α} (M : Matroid α) {D : Set α} (hXD : ∀ (i : ι), Disjoint (X i) D) : (M.delete D).multiConn X = M.multiConn X

@[simp]

theorem Matroid.multiConn_loopyOn {α : Type u_1} {ι : Type u_2} (E : Set α) (X : ι → Set α) : (loopyOn E).multiConn X = 0

theorem Matroid.IsBase.exists_restrict_multiConn_eq' {α : Type u_1} {M : Matroid α} {ι : Type u_2} {B : Set α} {X : ι → Set α} {k : ℕ∞} (hB : M.IsBase B) (hdj : Pairwise (Function.onFun Disjoint X)) (hX : ⋃ (i : ι), X i = M.E) (hkX : k ≤ M.multiConn X) : ∃ R ⊆ M.E, B ⊆ R ∧ (R \ B).encard = k ∧ ((M.restrict R).multiConn fun (i : ι) => X i ∩ R) = k

theorem Matroid.multiConn_cond {α : Type u_1} {M : Matroid α} {I J X Y : Set α} (hIX : M.IsBasis' I X) (hJY : M.IsBasis' J Y) : (M.multiConn fun (b : Bool) => bif b then X else Y) = M.nullity (I ∪ J) + (I ∩ J).encard

The local connectivity of a pair of sets X,Y is the nullity of I ∪ J plus the cardinality of I ∩ J, for any respective bases I and J for X and Y.

noncomputable def Matroid.eLocalConn {α : Type u_1} (M : Matroid α) (X Y : Set α) : ℕ∞

The ℕ∞-valued local connectivity between two sets X and Y, often written ⊓ (X,Y). Defined to correctly describe the connectivity even when one or both sets has infinite rank. For a ℕ-valued version, see Matroid.localConn.

Equations

• M.eLocalConn X Y = M.multiConn fun (b : Bool) => bif b then X else Y

theorem Matroid.IsBasis'.eLocalConn_eq {α : Type u_1} {M : Matroid α} {I J X Y : Set α} (hI : M.IsBasis' I X) (hJ : M.IsBasis' J Y) : M.eLocalConn X Y = (I ∩ J).encard + M.nullity (I ∪ J)

theorem Matroid.IsBasis.eLocalConn_eq {α : Type u_1} {M : Matroid α} {I J X Y : Set α} (hI : M.IsBasis I X) (hJ : M.IsBasis J Y) : M.eLocalConn X Y = (I ∩ J).encard + M.nullity (I ∪ J)

theorem Matroid.eLocalConn_comm {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eLocalConn X Y = M.eLocalConn Y X

theorem Matroid.eLocalConn_eq_multiConn {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eLocalConn X Y = M.multiConn fun (b : Bool) => bif b then X else Y

theorem Matroid.IsBasis'.eLocalConn_eq_nullity_project_right {α : Type u_1} {M : Matroid α} {X I : Set α} (hI : M.IsBasis' I X) (Y : Set α) : M.eLocalConn X Y = (M.project Y).nullity I

theorem Matroid.IsBasis.eLocalConn_eq_nullity_project_right {α : Type u_1} {M : Matroid α} {X I : Set α} (hI : M.IsBasis I X) (Y : Set α) : M.eLocalConn X Y = (M.project Y).nullity I

theorem Matroid.IsBasis'.eLocalConn_eq_nullity_project_left {α : Type u_1} {M : Matroid α} {Y I : Set α} (hI : M.IsBasis' I Y) (X : Set α) : M.eLocalConn X Y = (M.project X).nullity I

theorem Matroid.IsBasis.eLocalConn_eq_nullity_project_left {α : Type u_1} {M : Matroid α} {Y I : Set α} (hI : M.IsBasis I Y) (X : Set α) : M.eLocalConn X Y = (M.project X).nullity I

theorem Matroid.Indep.eLocalConn_eq_nullity_project_left {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (X : Set α) : M.eLocalConn I X = (M.project X).nullity I

theorem Matroid.Indep.eLocalConn_eq_nullity_project_right {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (X : Set α) : M.eLocalConn X I = (M.project X).nullity I

theorem Matroid.Indep.eLocalConn_eq {α : Type u_1} {M : Matroid α} {I J : Set α} (hI : M.Indep I) (hJ : M.Indep J) : M.eLocalConn I J = (I ∩ J).encard + M.nullity (I ∪ J)

theorem Matroid.Indep.eLocalConn_eq_encard_inter {α : Type u_1} {M : Matroid α} {I J : Set α} (hI : M.Indep (I ∪ J)) : M.eLocalConn I J = (I ∩ J).encard

theorem Matroid.IsBasis'.eLocalConn_eq_of_disjoint' {α : Type u_1} {M : Matroid α} {X Y I J : Set α} (hI : M.IsBasis' I X) (hJ : M.IsBasis' J Y) (hIJ : Disjoint I J) : M.eLocalConn X Y = M.nullity (I ∪ J)

theorem Matroid.IsBasis.eLocalConn_eq_of_disjoint' {α : Type u_1} {M : Matroid α} {X Y I J : Set α} (hI : M.IsBasis I X) (hJ : M.IsBasis J Y) (hIJ : Disjoint I J) : M.eLocalConn X Y = M.nullity (I ∪ J)

theorem Matroid.IsBasis'.eLocalConn_eq_of_disjoint {α : Type u_1} {M : Matroid α} {X Y I J : Set α} (hI : M.IsBasis' I X) (hJ : M.IsBasis' J Y) (hXY : Disjoint X Y) : M.eLocalConn X Y = M.nullity (I ∪ J)

theorem Matroid.IsBasis.eLocalConn_eq_of_disjoint {α : Type u_1} {M : Matroid α} {X Y I J : Set α} (hI : M.IsBasis I X) (hJ : M.IsBasis J Y) (hXY : Disjoint X Y) : M.eLocalConn X Y = M.nullity (I ∪ J)

theorem Matroid.eLocalConn_eq_encard_of_diff {α : Type u_1} {M : Matroid α} {X Y I J F : Set α} (hXY : Disjoint X Y) (hI : M.IsBasis' I X) (hJ : M.IsBasis' J Y) (hFIJ : F ⊆ I ∪ J) (hF : M.IsBasis' ((I ∪ J) \ F) (X ∪ Y)) : M.eLocalConn X Y = F.encard

theorem Matroid.eLocalConn_eq_encard_of_diff' {α : Type u_1} {M : Matroid α} {X Y I J F : Set α} (hXY : Disjoint X Y) (hI : M.IsBasis' I X) (hJ : M.IsBasis' J Y) (hFI : F ⊆ I) (hF : M.IsBasis' (I \ F ∪ J) (X ∪ Y)) : M.eLocalConn X Y = F.encard

@[simp]

theorem Matroid.eLocalConn_closure_right {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eLocalConn X (M.closure Y) = M.eLocalConn X Y

@[simp]

theorem Matroid.eLocalConn_closure_left {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eLocalConn (M.closure X) Y = M.eLocalConn X Y

@[simp]

theorem Matroid.eLocalConn_closure_closure {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eLocalConn (M.closure X) (M.closure Y) = M.eLocalConn X Y

theorem Matroid.eLocalConn_inter_ground {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eLocalConn (X ∩ M.E) (Y ∩ M.E) = M.eLocalConn X Y

@[simp]

theorem Matroid.eLocalConn_inter_ground_left {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eLocalConn (X ∩ M.E) Y = M.eLocalConn X Y

@[simp]

theorem Matroid.eLocalConn_inter_ground_right {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eLocalConn X (Y ∩ M.E) = M.eLocalConn X Y

@[simp]

theorem Matroid.eLocalConn_self {α : Type u_1} (M : Matroid α) (X : Set α) : M.eLocalConn X X = M.eRk X

theorem Matroid.eLocalConn_of_subset_coloops {α : Type u_1} {Y : Set α} (M : Matroid α) (X : Set α) (hY : Y ⊆ M.coloops) : M.eLocalConn X Y = (X ∩ Y).encard

@[simp]

theorem Matroid.eLocalConn_restrict_eq {α : Type u_1} (M : Matroid α) (X Y R : Set α) : (M.restrict R).eLocalConn X Y = M.eLocalConn (X ∩ R) (Y ∩ R)

theorem Matroid.eLocalConn_restrict_univ {α : Type u_1} (M : Matroid α) (X Y : Set α) : (M.restrict Set.univ).eLocalConn X Y = M.eLocalConn X Y

theorem Matroid.eLocalConn_union_left_of_subset_loops {α : Type u_1} {M : Matroid α} {X Y L : Set α} (hL : L ⊆ M.loops) : M.eLocalConn (X ∪ L) Y = M.eLocalConn X Y

theorem Matroid.eLocalConn_union_right_of_subset_loops {α : Type u_1} {M : Matroid α} {X Y L : Set α} (hL : L ⊆ M.loops) : M.eLocalConn X (Y ∪ L) = M.eLocalConn X Y

theorem Matroid.eLocalConn_diff_left_of_subset_loops {α : Type u_1} {M : Matroid α} {X Y L : Set α} (hL : L ⊆ M.loops) : M.eLocalConn (X \ L) Y = M.eLocalConn X Y

theorem Matroid.eLocalConn_diff_right_of_subset_loops {α : Type u_1} {M : Matroid α} {X Y L : Set α} (hL : L ⊆ M.loops) : M.eLocalConn X (Y \ L) = M.eLocalConn X Y

theorem Matroid.IsRestriction.eLocalConn_eq {α : Type u_1} {M N : Matroid α} (hNM : N.IsRestriction M) (X Y : Set α) : N.eLocalConn X Y = M.eLocalConn (X ∩ N.E) (Y ∩ N.E)

theorem Matroid.IsRestriction.eLocalConn_eq_of_subset {α : Type u_1} {M : Matroid α} {X Y : Set α} {N : Matroid α} (hNM : N.IsRestriction M) (hXE : X ⊆ N.E := by aesop_mat) (hYE : Y ⊆ N.E := by aesop_mat) : N.eLocalConn X Y = M.eLocalConn X Y

theorem Matroid.eRk_add_eRk_eq_eRk_union_add_eLocalConn {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRk X + M.eRk Y = M.eRk (X ∪ Y) + M.eLocalConn X Y

theorem Matroid.eRk_inter_le_eLocalConn {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRk (X ∩ Y) ≤ M.eLocalConn X Y

theorem Matroid.eLocalConn_mono_left {α : Type u_1} {X X' : Set α} (M : Matroid α) (hX : X' ⊆ X) (Y : Set α) : M.eLocalConn X' Y ≤ M.eLocalConn X Y

theorem Matroid.eLocalConn_mono_right {α : Type u_1} {Y Y' : Set α} (M : Matroid α) (X : Set α) (hY : Y' ⊆ Y) : M.eLocalConn X Y' ≤ M.eLocalConn X Y

theorem Matroid.eLocalConn_mono {α : Type u_1} {X Y X' Y' : Set α} (M : Matroid α) (hX : X' ⊆ X) (hY : Y' ⊆ Y) : M.eLocalConn X' Y' ≤ M.eLocalConn X Y

@[simp]

theorem Matroid.empty_eLocalConn {α : Type u_1} (M : Matroid α) (X : Set α) : M.eLocalConn ∅ X = 0

@[simp]

theorem Matroid.eLocalConn_empty {α : Type u_1} (M : Matroid α) (X : Set α) : M.eLocalConn X ∅ = 0

theorem Matroid.eLocalConn_subset {α : Type u_1} {X Y : Set α} (M : Matroid α) (hXY : X ⊆ Y) : M.eLocalConn X Y = M.eRk X

theorem Matroid.eLocalConn_eq_zero {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : X ⊆ M.E := by aesop_mat) (hY : Y ⊆ M.E := by aesop_mat) : M.eLocalConn X Y = 0 ↔ M.Skew X Y

theorem Matroid.Skew.eLocalConn {α : Type u_1} {M : Matroid α} {X Y : Set α} (hXY : M.Skew X Y) : M.eLocalConn X Y = 0

theorem Matroid.eLocalConn_restrict_of_subset {α : Type u_1} {X Y : Set α} (M : Matroid α) {R : Set α} (hXR : X ⊆ R) (hYR : Y ⊆ R) : (M.restrict R).eLocalConn X Y = M.eLocalConn X Y

theorem Matroid.eLocalConn_delete_eq {α : Type u_1} (M : Matroid α) (X Y D : Set α) : (M.delete D).eLocalConn X Y = M.eLocalConn (X \ D) (Y \ D)

theorem Matroid.eLocalConn_delete_eq_of_disjoint {α : Type u_1} {X Y : Set α} (M : Matroid α) {D : Set α} (hXD : Disjoint X D) (hYD : Disjoint Y D) : (M.delete D).eLocalConn X Y = M.eLocalConn X Y

theorem Matroid.eLocalConn_delete_eq_of_subset_loops {α : Type u_1} {M : Matroid α} {X Y L : Set α} (hL : L ⊆ M.loops) : (M.delete L).eLocalConn X Y = M.eLocalConn X Y

@[simp]

theorem Matroid.eLocalConn_map {α : Type u_1} {β : Type u_3} (M : Matroid α) (f : α → β) (hf : Set.InjOn f M.E) (X Y : Set β) : (M.map f hf).eLocalConn X Y = M.eLocalConn (f ⁻¹' X) (f ⁻¹' Y)

instance Matroid.instInvariantFun₂SetENatELocalConn : InvariantFun₂ (fun {α : Type u_3} => eLocalConn) fun {β : Type u_4} => eLocalConn

@[simp]

theorem Matroid.eLocalConn_comap {α : Type u_1} {β : Type u_3} (M : Matroid β) (f : α → β) (X Y : Set α) : (M.comap f).eLocalConn X Y = M.eLocalConn (f '' X) (f '' Y)

@[simp]

theorem Matroid.eLocalConn_ground_eq {α : Type u_1} (M : Matroid α) (X : Set α) : M.eLocalConn X M.E = M.eRk X

@[simp]

theorem Matroid.ground_eLocalConn_eq {α : Type u_1} (M : Matroid α) (X : Set α) : M.eLocalConn M.E X = M.eRk X

theorem Matroid.eLocalConn_le_eRk_left {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eLocalConn X Y ≤ M.eRk X

theorem Matroid.eLocalConn_le_eRk_right {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eLocalConn X Y ≤ M.eRk Y

@[simp]

theorem Matroid.eLocalConn_lt_top {α : Type u_1} (M : Matroid α) [M.RankFinite] (X Y : Set α) : M.eLocalConn X Y < ⊤

@[simp]

theorem Matroid.eLocalConn_ne_top {α : Type u_1} (M : Matroid α) [M.RankFinite] (X Y : Set α) : M.eLocalConn X Y ≠ ⊤

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

theorem Matroid.eLocalConn_union_left_le_eLocalConn_add_encard {α : Type u_1} (M : Matroid α) (X Y Z : Set α) : M.eLocalConn (X ∪ Z) Y ≤ M.eLocalConn X Y + Z.encard

theorem Matroid.eLocalConn_insert_left_le_add_one {α : Type u_1} (M : Matroid α) (X Y : Set α) (e : α) : M.eLocalConn (insert e X) Y ≤ M.eLocalConn X Y + 1

@[simp]

theorem Matroid.loopyOn_eLocalConn {α : Type u_1} {E X Y : Set α} : (loopyOn E).eLocalConn X Y = 0

theorem Matroid.Indep.encard_inter_add_nullity_le_eLocalConn {α : Type u_1} {M : Matroid α} {X Y I J : Set α} (hI : M.Indep I) (hIX : I ⊆ X) (hJ : M.Indep J) (hJY : J ⊆ Y) : (I ∩ J).encard + M.nullity (I ∪ J) ≤ M.eLocalConn X Y

theorem Matroid.IsModularPair.eLocalConn_eq_eRk_inter {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsModularPair X Y) : M.eLocalConn X Y = M.eRk (X ∩ Y)

theorem Matroid.eLocalConn_insert_left_eq_add_one {α : Type u_1} {M : Matroid α} {X Y : Set α} {e : α} (heX : e ∉ M.closure X) (heXY : e ∈ M.closure (X ∪ Y)) : M.eLocalConn (insert e X) Y = M.eLocalConn X Y + 1

theorem Matroid.eLocalConn_insert_right_eq_add_one {α : Type u_1} {M : Matroid α} {X Y : Set α} {e : α} (heY : e ∉ M.closure Y) (heXY : e ∈ M.closure (X ∪ Y)) : M.eLocalConn X (insert e Y) = M.eLocalConn X Y + 1

theorem Matroid.IsNonloop.eLocalConn_eq_zero_iff {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (he : M.IsNonloop e) : M.eLocalConn {e} X = 0 ↔ e ∉ M.closure X

theorem Matroid.IsNonloop.eLocalConn_eq_one_iff {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (he : M.IsNonloop e) : M.eLocalConn {e} X = 1 ↔ e ∈ M.closure X

theorem Matroid.eLocalConn_singleton_left_eq_zero {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (he : e ∉ M.closure X) : M.eLocalConn {e} X = 0

theorem Matroid.eLocalConn_singleton_right_eq_zero {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (he : e ∉ M.closure X) : M.eLocalConn X {e} = 0

theorem Matroid.IsNonloop.eLocalConn_eq_ite {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsNonloop e) (X : Set α) [Decidable (e ∈ M.closure X)] : M.eLocalConn {e} X = if e ∈ M.closure X then 1 else 0

theorem Matroid.IsCircuit.eLocalConn_subset_compl {α : Type u_1} {M : Matroid α} {I C : Set α} (hC : M.IsCircuit C) (hI : I.Nonempty) (hIC : I ⊂ C) : M.eLocalConn I (C \ I) = 1

theorem Matroid.IsCircuit.union_isCircuit_of_inter_eq_singleton {α : Type u_1} {M : Matroid α} {C₁ C₂ : Set α} {e : α} (hC₁ : M.IsCircuit C₁) (hC₂ : M.IsCircuit C₂) (hne : C₁ ≠ C₂) (heC₁ : e ∈ C₁) (heC₂ : e ∈ C₂) (hc : M.eLocalConn C₁ C₂ ≤ 1) : M.IsCircuit ((C₁ ∪ C₂) \ {e})

If two circuits intersect in an element e and have connectivity at most one, then their symmetric difference is a circuit.

theorem Matroid.IsTriangle.union_diff_singleton_isCircuit {α : Type u_1} {M : Matroid α} {e f g : α} {C : Set α} (hT : M.IsTriangle {e, f, g}) (hC : M.IsCircuit C) (heC : e ∈ C) (hfC : f ∉ M.closure C) : M.IsCircuit (insert f (insert g (C \ {e})))

theorem Matroid.IsTriangle.union_diff_singleton_isCircuit_four {α : Type u_1} {M : Matroid α} {e f e' f' x : α} (hT : M.IsTriangle {e, f, x}) (hT' : M.IsTriangle {e', f', x}) (hee' : e ≠ e') (h_indep : M.Indep {e, e', x}) : M.IsCircuit {e, f, e', f'}

theorem Matroid.IsCircuit.union_isCircuit_of_inter_nonempty {α : Type u_1} {M : Matroid α} {C₁ C₂ : Set α} (hC₁ : M.IsCircuit C₁) (hC₂ : M.IsCircuit C₂) (hne : C₁ ≠ C₂) (h_inter : (C₁ ∩ C₂).Nonempty) (hc : M.eLocalConn C₁ C₂ ≤ 1) : M.IsCircuit ((C₁ ∪ C₂) \ (C₁ ∩ C₂))

theorem Matroid.IsRkFinite.isModularPair_iff_eLocalConn_eq_eRk_inter {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.IsRkFinite X) (Y : Set α) (hXE : X ⊆ M.E := by aesop_mat) (hYE : Y ⊆ M.E := by aesop_mat) : M.IsModularPair X Y ↔ M.eLocalConn X Y = M.eRk (X ∩ Y)

theorem Matroid.eLocalConn_add_eRelRk_union_eq_eRk {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eLocalConn X Y + M.eRelRk Y (X ∪ Y) = M.eRk X

For finite matroids, this is another rearrangement of the formula in Matroid.eRk_add_eRk_eq_eRk_union_add_eLocalConn. For infinite matroids it needs a separate proof.

theorem Matroid.eRk_project_add_eLocalConn_eq {α : Type u_1} (M : Matroid α) (X Y : Set α) : (M.project Y).eRk X + M.eLocalConn X Y = M.eRk X

theorem Matroid.eRk_contract_add_eLocalConn_eq {α : Type u_1} (M : Matroid α) (X Y : Set α) : (M.contract Y).eRk X + M.eLocalConn X Y = M.eRk X

theorem Matroid.IsHyperplane.eLocalConn_add_one_eq {α : Type u_1} {M : Matroid α} {H X : Set α} (hH : M.IsHyperplane H) (hXH : ¬X ⊆ H) (hXE : X ⊆ M.E := by aesop_mat) : M.eLocalConn X H + 1 = M.eRk X

theorem Matroid.eLocalConn_le_add_eRelRk_left {α : Type u_1} {X Y : Set α} (M : Matroid α) (hXY : X ⊆ Y) (Z : Set α) : M.eLocalConn Y Z ≤ M.eLocalConn X Z + M.eRelRk X Y

theorem Matroid.eLocalConn_le_add_eRelRk_right {α : Type u_1} {X Y : Set α} (M : Matroid α) (hXY : X ⊆ Y) (Z : Set α) : M.eLocalConn Z Y ≤ M.eLocalConn Z X + M.eRelRk X Y

theorem Matroid.eLocalConn_union_left_le {α : Type u_1} (M : Matroid α) (X Y A : Set α) : M.eLocalConn (X ∪ A) Y ≤ M.eLocalConn X Y + M.eRelRk X (X ∪ A)

theorem Matroid.eLocalConn_union_right_le {α : Type u_1} (M : Matroid α) (X Y A : Set α) : M.eLocalConn X (Y ∪ A) ≤ M.eLocalConn X Y + M.eRelRk Y (Y ∪ A)

theorem Matroid.eLocalConn_insert_left_le {α : Type u_1} (M : Matroid α) (X Y : Set α) (e : α) : M.eLocalConn (insert e X) Y ≤ M.eLocalConn X Y + 1

theorem Matroid.eLocalConn_insert_right_le {α : Type u_1} (M : Matroid α) (X Y : Set α) (e : α) : M.eLocalConn X (insert e Y) ≤ M.eLocalConn X Y + 1

@[simp]

theorem Matroid.removeLoops_eLocalConn {α : Type u_1} (M : Matroid α) : M.removeLoops.eLocalConn = M.eLocalConn

theorem Matroid.eRk_union_right_add_eRk_union_right_eq {α : Type u_1} (M : Matroid α) (X Y C : Set α) : M.eRk (X ∪ C) + M.eRk (Y ∪ C) = M.eRk (X ∪ Y ∪ C) + M.eRk C + (M.project C).eLocalConn X Y

A submodularity-like equality with an explicit slack term in the form of local connectivity.

theorem Matroid.eRk_add_eRk_eq_eRk_union_add_eRk_inter_add_eLocalConn {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRk X + M.eRk Y = M.eRk (X ∪ Y) + M.eRk (X ∩ Y) + (M.project (X ∩ Y)).eLocalConn X Y

A version of submodularity with an explicit slack term.