structure ConnSystem (α : Type u_3) (R : Type u_4) [Add R] [LE R] : Type (max u_3 u_4)

A submodular function on Set α that is determined by its behaviour on a given ground set E, and is invariant under taking complements within E. Examples include the connectivity function of a matroid, and the vertex- and edge-connectivity functions of a graph.

• E : Set α
• toFun : Set α → R
• toFun_inter_ground (X : Set α) : ↑self (X ∩ self.E) = ↑self X
• toFun_compl (X : Set α) : X ⊆ self.E → ↑self (self.E \ X) = ↑self X
• toFun_submod (X Y : Set α) : X ⊆ self.E → Y ⊆ self.E → ↑self (X ∩ Y) + ↑self (X ∪ Y) ≤ ↑self X + ↑self Y

@[instance_reducible]

instance ConnSystem.instCoeFunForallSet {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] : CoeFun (ConnSystem α R) fun (x : ConnSystem α R) => Set α → R

Equations

• ConnSystem.instCoeFunForallSet = { coe := ConnSystem.toFun }

theorem ConnSystem.ext {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] {μ ν : ConnSystem α R} (hE : μ.E = ν.E) (hf : ∀ X ⊆ μ.E, ↑μ X = ↑ν X) : μ = ν

theorem ConnSystem.ext_iff {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] {μ ν : ConnSystem α R} : μ = ν ↔ μ.E = ν.E ∧ ∀ X ⊆ μ.E, ↑μ X = ↑ν X

@[simp]

theorem ConnSystem.toFun_eq_coe {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] (μ : ConnSystem α R) (X : Set α) : ↑μ X = ↑μ X

@[simp]

theorem ConnSystem.apply_inter_ground {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] (μ : ConnSystem α R) (X : Set α) : ↑μ (X ∩ μ.E) = ↑μ X

@[simp]

theorem ConnSystem.apply_compl {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] (μ : ConnSystem α R) (X : Set α) : ↑μ (μ.E \ X) = ↑μ X

@[simp]

theorem ConnSystem.apply_compl' {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] (μ : ConnSystem α R) (X : Set α) : ↑μ Xᶜ = ↑μ X

theorem ConnSystem.apply_submod {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] (μ : ConnSystem α R) (X Y : Set α) : ↑μ (X ∩ Y) + ↑μ (X ∪ Y) ≤ ↑μ X + ↑μ Y

def ConnSystem.pConn {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] (μ : ConnSystem α R) (P : μ.E.IndexedPartition Bool) : R

A connectivity system assigns a connectivity to each bipartition of its ground set.

Equations

• μ.pConn P = ↑μ (P true)

@[simp]

theorem ConnSystem.pConn_symm {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] {μ : ConnSystem α R} (P : μ.E.IndexedPartition Bool) : μ.pConn P.symm = μ.pConn P

@[simp]

theorem ConnSystem.pConn_ofSubset {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] (μ : ConnSystem α R) (X : Set α) (hX : X ⊆ μ.E) (i : Bool) : μ.pConn (Set.IndexedPartition.ofSubset hX i) = ↑μ X

@[simp]

theorem ConnSystem.apply_eq_pConn {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] {μ : ConnSystem α R} (P : μ.E.IndexedPartition Bool) (i : Bool) : ↑μ (P i) = μ.pConn P

def ConnSystem.induce {α : Type u_1} {R : Type u_2} {F : Set α} [PartialOrder R] [Add R] (μ : ConnSystem α R) (hF : μ.E ⊆ F) : ConnSystem α R

Move a connectivity system to a larger ground set.

Equations

• μ.induce hF = { E := F, toFun := ↑μ, toFun_inter_ground := ⋯, toFun_compl := ⋯, toFun_submod := ⋯ }

@[simp]

theorem ConnSystem.induce_toFun {α : Type u_1} {R : Type u_2} {F : Set α} [PartialOrder R] [Add R] (μ : ConnSystem α R) (hF : μ.E ⊆ F) (a✝ : Set α) : ↑(μ.induce hF) a✝ = ↑μ a✝

@[simp]

theorem ConnSystem.induce_E {α : Type u_1} {R : Type u_2} {F : Set α} [PartialOrder R] [Add R] (μ : ConnSystem α R) (hF : μ.E ⊆ F) : (μ.induce hF).E = F

@[simp]

theorem ConnSystem.induce_pConn {α : Type u_1} {R : Type u_2} {F : Set α} [PartialOrder R] [Add R] (μ : ConnSystem α R) (hF : μ.E ⊆ F) (P : F.IndexedPartition Bool) : (μ.induce hF).pConn P = μ.pConn (P.induce hF)

def ConnSystem.Normal {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] [Zero R] (μ : ConnSystem α R) : Prop

A connectivity system is Normal if the empty set has connectivity zero .

Equations

• μ.Normal = (↑μ ∅ = 0)

theorem ConnSystem.Normal.apply_empty {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] [Zero R] {μ : ConnSystem α R} (hμ : μ.Normal) : ↑μ ∅ = 0

theorem ConnSystem.Normal.apply_ground {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] [Zero R] {μ : ConnSystem α R} (hμ : μ.Normal) : ↑μ μ.E = 0

structure ConnSystem.Unitary {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] [Zero R] [One R] (μ : ConnSystem α R) : Prop

A connectivity system is Unitary if it assigns the empty set a connectivity of zero and singletons to a connectivity of at most 1.

• apply_empty : ↑μ ∅ = 0
• apply_singleton_le (e : α) : ↑μ {e} ≤ 1

theorem ConnSystem.unitary_iff {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] [Zero R] [One R] (μ : ConnSystem α R) : μ.Unitary ↔ ↑μ ∅ = 0 ∧ ∀ (e : α), ↑μ {e} ≤ 1

theorem ConnSystem.Unitary.normal {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] [Zero R] [One R] {μ : ConnSystem α R} (hμ : μ.Unitary) : μ.Normal

theorem ConnSystem.Unitary.apply_le_encard {α : Type u_1} {μ : ConnSystem α ℕ∞} (hμ : μ.Unitary) (X : Set α) : ↑μ X ≤ X.encard

@[instance_reducible]

instance ConnSystem.instPartialOrder {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] : PartialOrder (ConnSystem α R)

Equations

• ConnSystem.instPartialOrder = { le := fun (ν μ : ConnSystem α R) => ν.E ⊆ μ.E ∧ ∀ (X : Set α), ↑ν X ≤ ↑μ X, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

theorem ConnSystem.subset_of_le {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] {μ ν : ConnSystem α R} (h : μ ≤ ν) : μ.E ⊆ ν.E

theorem ConnSystem.apply_le_of_le {α : Type u_1} {R : Type u_2} {X : Set α} [PartialOrder R] [Add R] {μ ν : ConnSystem α R} (h : μ ≤ ν) : ↑μ X ≤ ↑ν X

@[simp]

theorem ConnSystem.le_induce {α : Type u_1} {R : Type u_2} {F : Set α} [PartialOrder R] [Add R] (μ : ConnSystem α R) (hF : μ.E ⊆ F) : μ ≤ μ.induce hF

def ConnSystem.SplitsIn {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] {ν : ConnSystem α R} (P : ν.E.IndexedPartition Bool) (μ : ConnSystem α R) : Prop

If μ, ν are connectivity systems, and P is a bipartition of ν.E, then we say that SplitsIn P μ if one side of P has a bipartition into two parts, each of which has connectivity at most the connectivity of P in ν.

Equations

• ConnSystem.SplitsIn P μ = ∃ (i : Bool) (P₀ : (P i).IndexedPartition Bool), ∀ (j : Bool), ↑μ (P₀ j) ≤ ν.pConn P

structure ConnSystem.AdheresTo {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] (ν μ : ConnSystem α R) : Prop

If μ and ν are connectivity systems with μ dominating ν, then ν adheres to μ if each partition of ν.E splits in μ.

• le : ν ≤ μ
• forall_splits (P : ν.E.IndexedPartition Bool) : SplitsIn P μ

theorem ConnSystem.AdheresTo.subset {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] {μ ν : ConnSystem α R} (h : ν.AdheresTo μ) : ν.E ⊆ μ.E

theorem ConnSystem.AdheresTo.apply_le {α : Type u_1} {R : Type u_2} [PartialOrder R] [Add R] {μ ν : ConnSystem α R} (h : ν.AdheresTo μ) (X : Set α) : ↑ν X ≤ ↑μ X