Documentation

Matroid.Connectivity.Connected

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

Equations

M.ConnectedTo e f = (e = f ∧ e ∈ M.E ∨ ∃ (C : Set α), M.IsCircuit C ∧ e ∈ C ∧ f ∈ C)

Instances For

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

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

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

M.ConnectedTo e f

theorem Matroid.connectedTo_self {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E) :

M.ConnectedTo e e

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

M.ConnectedTo f e

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

M.ConnectedTo e f ↔ M.ConnectedTo f e

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

Std.Symm M.ConnectedTo

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

e ∈ M.E

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

f ∈ M.E

@[simp]

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

{x : α | M.ConnectedTo e x} ⊆ M.E

@[simp]

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

M.ConnectedTo e e ↔ e ∈ M.E

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

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

theorem Matroid.ConnectedTo.to_dual {α : Type u_1} {M : Matroid α} {e f : α} (h : M.ConnectedTo e f) :

M✶.ConnectedTo e f

theorem Matroid.ConnectedTo.of_dual {α : Type u_1} {M : Matroid α} {e f : α} (h : M✶.ConnectedTo e f) :

M.ConnectedTo e f

@[simp]

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

M✶.ConnectedTo e f ↔ M.ConnectedTo e f

theorem Matroid.IsCocircuit.mem_connectedTo_mem {α : Type u_1} {M : Matroid α} {K : Set α} {e f : α} (hK : M.IsCocircuit K) (heK : e ∈ K) (hfK : f ∈ K) :

M.ConnectedTo e f

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

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

theorem Matroid.ConnectedTo.of_restrict {α : Type u_1} {M : Matroid α} {e f : α} {R : Set α} (hR : R ⊆ M.E) (hef : (M.restrict R).ConnectedTo e f) :

M.ConnectedTo e f

theorem Matroid.ConnectedTo.of_delete {α : Type u_1} {M : Matroid α} {e f : α} {D : Set α} (hef : (M.delete D).ConnectedTo e f) :

M.ConnectedTo e f

theorem Matroid.ConnectedTo.of_contract {α : Type u_1} {M : Matroid α} {e f : α} {C : Set α} (hef : (M.contract C).ConnectedTo e f) :

M.ConnectedTo e f

theorem Matroid.ConnectedTo.of_isMinor {α : Type u_1} {M : Matroid α} {e f : α} {N : Matroid α} (hef : N.ConnectedTo e f) (h : N ≤m M) :

M.ConnectedTo e f

theorem Matroid.ConnectedTo.trans {α : Type u_1} {M : Matroid α} {f e₁ e₂ : α} (h₁ : M.ConnectedTo e₁ f) (h₂ : M.ConnectedTo f e₂) :

M.ConnectedTo e₁ e₂

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

IsTrans α M.ConnectedTo

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

Partition (Set α)

Equations

M.ConnPartition = Partition.ofRel M.ConnectedTo

Instances For

@[simp]

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

M.ConnPartition.supp = M.E

@[simp]

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

M.ConnPartition e f ↔ M.ConnectedTo e f

theorem Matroid.IsCircuit.disjoint_or_subset {α : Type u_1} {M : Matroid α} {C K : Set α} (hC : M.IsCircuit C) (hK : K ∈ M.ConnPartition) :

Disjoint C K ∨ C ⊆ K

theorem Matroid.IsCircuit.subset_of_mem_connPartition {α : Type u_1} {M : Matroid α} {C K : Set α} {e : α} (hC : M.IsCircuit C) (hK : K ∈ M.ConnPartition) (heC : e ∈ C) (heK : e ∈ K) :

C ⊆ K

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

nonempty : M.Nonempty
forall_connectedTo ⦃e f : α⦄ : e ∈ M.E → f ∈ M.E → M.ConnectedTo e f

Instances For

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

M.Connected ↔ M.Nonempty ∧ ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.ConnectedTo e f

theorem Matroid.Connected.connectedTo {α : Type u_1} {M : Matroid α} (hM : M.Connected) (x y : α) (hx : x ∈ M.E := by aesop_mat) (hy : y ∈ M.E := by aesop_mat) :

M.ConnectedTo x y

theorem Matroid.Connected.to_dual {α : Type u_1} {M : Matroid α} (hM : M.Connected) :

theorem Matroid.Connected.of_dual {α : Type u_1} {M : Matroid α} (hM : M✶.Connected) :

@[simp]

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

M✶.Connected ↔ M.Connected

theorem Matroid.IsColoop.not_connected {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsColoop e) (hE : M.E.Nontrivial) :

theorem Matroid.IsLoop.not_connected {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsLoop e) (hE : M.E.Nontrivial) :

theorem Matroid.Connected.loopless {α : Type u_1} {M : Matroid α} (hM : M.Connected) (hE : M.E.Nontrivial) :

theorem Matroid.Connected.exists_isCircuit_of_ne {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Connected) (he : e ∈ M.E) (hf : f ∈ M.E) (hne : e ≠ f) :

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

theorem Matroid.Connected.exists_isCircuit {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Connected) (hM : M.E.Nontrivial) (he : e ∈ M.E) (hf : f ∈ M.E) :

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

theorem Matroid.Connected.rankPos {α : Type u_1} {M : Matroid α} (h : M.Connected) (hM : M.E.Nontrivial) :

theorem Matroid.singleton_connected {α : Type u_1} {M : Matroid α} {e : α} (hM : M.E = {e}) :

theorem Matroid.not_connected_iff_exists {α : Type u_1} {M : Matroid α} [hne : M.Nonempty] :

¬M.Connected ↔ ∃ e ∈ M.E, ∃ f ∈ M.E, e ≠ f ∧ ¬M.ConnectedTo e f

theorem Matroid.eq_disjointSum_of_not_connected {α : Type u_1} {M : Matroid α} [hne : M.Nonempty] (h : ¬M.Connected) :

∃ (M₁ : Matroid α) (M₂ : Matroid α) (hdj : Disjoint M₁.E M₂.E), M₁.Nonempty ∧ M₂.Nonempty ∧ M = M₁.disjointSum M₂ hdj

theorem Matroid.disjointSum_not_connected {α : Type u_1} {M₁ M₂ : Matroid α} (h₁ : M₁.Nonempty) (h₂ : M₂.Nonempty) (hdj : Disjoint M₁.E M₂.E) :

¬(M₁.disjointSum M₂ hdj).Connected

theorem Matroid.cSet_antitone {α : Type u_1} [DecidablePred Set.Infinite] {Cs : ℕ → Set α} {e : ℕ → α} :

Antitone (Matroid.cSet✝ Cs e)

theorem Matroid.cSet_subset_range {α : Type u_1} [DecidablePred Set.Infinite] (Cs : ℕ → Set α) (e : ℕ → α) (i : ℕ) :

Matroid.cSet✝ Cs e i ⊆ Set.range Cs

theorem Matroid.X_monotone {α : Type u_1} [DecidablePred Set.Infinite] (Cs : ℕ → Set α) (e : ℕ → α) :

Monotone (Matroid.X✝ Cs e)

theorem Matroid.cSet_infinite {α : Type u_1} [DecidablePred Set.Infinite] (Cs : ℕ ↪ Set α) (e : ℕ → α) (i : ℕ) :

(Matroid.cSet✝ (⇑Cs) e i).Infinite

theorem Matroid.cSet_inter_image_Iic {α : Type u_1} [DecidablePred Set.Infinite] {Cs : ℕ ↪ Set α} {e : ℕ → α} {i : ℕ} {C : Set α} (heC : e 0 ∈ C) (hC : C ∈ Matroid.cSet✝ (⇑Cs) e i) :

C ∩ e '' Set.Iic i = Matroid.X✝ (⇑Cs) e i

theorem Matroid.Connected.finite_of_finitary_of_cofinitary {α : Type u_2} {M : Matroid α} (hM : M.Connected) [M.Finitary] [M✶.Finitary] :

Every connected, finitary, cofinitary matroid is finite

theorem Matroid.ConnectedTo.delete_or_contract {α : Type u_1} {M : Matroid α} {x y e : α} (hM : M.ConnectedTo x y) (hxe : x ≠ e) (hye : y ≠ e) :

(M.delete {e}).ConnectedTo x y ∨ (M.contract {e}).ConnectedTo x y

theorem Matroid.Connected.delete_or_contract {α : Type u_1} {M : Matroid α} (hM : M.Connected) (hnt : M.E.Nontrivial) (e : α) :

(M.delete {e}).Connected ∨ (M.contract {e}).Connected