Documentation

Matroid.Tame

def Matroid.IsCrossing {α : Type u_1} (M : Matroid α) (X : Set α) :

A Crossing is the intersection of a circuit and a cocircuit.

Equations

M.IsCrossing X = ∃ (C : Set α) (K : Set α), M.IsCircuit C ∧ M.IsCocircuit K ∧ X = C ∩ K

Instances For

theorem Matroid.IsCrossing.dual {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.IsCrossing X) :

M✶.IsCrossing X

theorem Matroid.IsCrossing.of_dual {α : Type u_1} {M : Matroid α} {X : Set α} (h : M✶.IsCrossing X) :

@[simp]

theorem Matroid.isCrossing_dual_iff {α : Type u_1} {M : Matroid α} {X : Set α} :

M✶.IsCrossing X ↔ M.IsCrossing X

theorem Matroid.IsCrossing.subset_ground {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.IsCrossing X) :

X ⊆ M.E

theorem Matroid.IsCrossing.encard_ne_one {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.IsCrossing X) :

theorem Matroid.IsCrossing.of_contract {α : Type u_1} {M : Matroid α} {C X : Set α} (hC : (M.contract C).IsCrossing X) :

theorem Matroid.IsCrossing.of_delete {α : Type u_1} {M : Matroid α} {X D : Set α} (hD : (M.delete D).IsCrossing X) :

theorem Matroid.IsCrossing.of_isMinor {α : Type u_1} {M : Matroid α} {X : Set α} {N : Matroid α} (hX : N.IsCrossing X) (hNM : N ≤m M) :

theorem Matroid.Iso.isCrossing_image {α : Type u_3} {β : Type u_4} {M : Matroid α} {N : Matroid β} {X : Set ↑M.E} (i : M ≂ N) (hX : M.IsCrossing (Subtype.val '' X)) :

N.IsCrossing (Subtype.val '' ⇑i '' X)

theorem Matroid.IsCircuit.isCrossing_inter {α : Type u_1} {M : Matroid α} {C K : Set α} (hC : M.IsCircuit C) (hK : M.IsCocircuit K) :

M.IsCrossing (C ∩ K)

theorem Matroid.IsCocircuit.isCrossing_inter {α : Type u_1} {M : Matroid α} {C K : Set α} (hK : M.IsCocircuit K) (hC : M.IsCircuit C) :

M.IsCrossing (K ∩ C)

theorem Matroid.IsCircuit.isCrossing_of_isCocircuit {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) (hC' : M.IsCocircuit C) :

class Matroid.Tame {α : Type u_1} (M : Matroid α) :

A tame matroid is one whose circuit-cocircuit intersections (aka crossings) are all finite.

forall_isCrossing_finite ⦃X : Set α⦄ : M.IsCrossing X → X.Finite

Instances

theorem Matroid.IsCrossing.finite {α : Type u_1} {M : Matroid α} {X : Set α} [M.Tame] (h : M.IsCrossing X) :

theorem Matroid.IsCircuit.inter_finite_of_isCocircuit {α : Type u_1} {M : Matroid α} {C K : Set α} [M.Tame] (hC : M.IsCircuit C) (hK : M.IsCocircuit K) :

(C ∩ K).Finite

theorem Matroid.Tame.dual {α : Type u_1} {M : Matroid α} (h : M.Tame) :

theorem Matroid.tame_dual {α : Type u_1} (M : Matroid α) [M.Tame] :

@[simp]

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

M✶.Tame ↔ M.Tame

instance Matroid.instTameOfDual {α : Type u_1} {M : Matroid α} [M✶.Tame] :

instance Matroid.instTameDelete {α : Type u_1} {M : Matroid α} [M.Tame] (D : Set α) :

(M.delete D).Tame

instance Matroid.instTameContract {α : Type u_1} {M : Matroid α} [M.Tame] (C : Set α) :

(M.contract C).Tame

instance Matroid.instTameOfFinitary {α : Type u_1} {M : Matroid α} [M.Finitary] :

instance Matroid.instTameOfFinitaryDual {α : Type u_1} {M : Matroid α} [M✶.Finitary] :

theorem Matroid.Tame.minor {α : Type u_1} {N M : Matroid α} (h : M.Tame) (hNM : N ≤m M) :

theorem Matroid.IsSparsePaving.rankFinite_or_rankFinite_dual {α : Type u_1} {M : Matroid α} [M.Tame] (h : M.IsSparsePaving) :

M.RankFinite ∨ M✶.RankFinite

Every tame sparse paving matroid has finite rank or corank. I am not sure if this is true or not for just Paving.