Documentation

Matroid.Closure

theorem Matroid.isBase_iff_indep_spanning {α : Type u_1} {M : Matroid α} {B : Set α} :

M.IsBase B ↔ M.Indep B ∧ M.Spanning B

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

M.Coindep X ↔ X ⊆ M.closure (M.E \ X)

theorem Matroid.Spanning.rankFinite_of_finite {α : Type u_1} {M : Matroid α} {S : Set α} (hS : M.Spanning S) (hSfin : S.Finite) :

theorem Matroid.IsRestriction.closure_subset_closure {α : Type u_1} {M N : Matroid α} (h : M.IsRestriction N) (X : Set α) :

M.closure X ⊆ N.closure X

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

M.Spanning ∅ ↔ ∃ (E : Set α), M = loopyOn E

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

M.Spanning ∅ ↔ M = loopyOn M.E

theorem Matroid.spanning_dual_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hXE : X ⊆ M.E := by aesop_mat) :

M✶.Spanning X ↔ M.Indep (M.E \ X)

theorem Matroid.spanning_compl_dual_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hXE : X ⊆ M.E := by aesop_mat) :

M✶.Spanning (M.E \ X) ↔ M.Indep X

theorem Matroid.map_spanning_iff {α : Type u_1} {M : Matroid α} {β : Type u_2} {X : Set β} {f : α → β} (hf : Set.InjOn f M.E) :

(M.map f hf).Spanning X ↔ ∃ (X₀ : Set α), M.Spanning X₀ ∧ X = f '' X₀

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

isRestriction : N.IsRestriction M
spanning : M.Spanning N.E

Instances For

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

N.IsSpanningRestriction M ↔ N.IsRestriction M ∧ M.Spanning N.E

def Matroid.«term_≤sr_» :

Lean.TrailingParserDescr

Equations

Matroid.«term_≤sr_» = Lean.ParserDescr.trailingNode `Matroid.«term_≤sr_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤sr ") (Lean.ParserDescr.cat `term 51))

Instances For

theorem Matroid.IsSpanningRestriction.subset {α : Type u_1} {M N : Matroid α} (h : N.IsSpanningRestriction M) :

N.E ⊆ M.E

theorem Matroid.IsSpanningRestriction.refl {α : Type u_1} {M : Matroid α} :

M.IsSpanningRestriction M

theorem Matroid.IsSpanningRestriction.spanning_of_spanning {α : Type u_1} {M N : Matroid α} {X : Set α} (h : N.IsSpanningRestriction M) (hX : N.Spanning X) :

theorem Matroid.IsSpanningRestriction.spanning_iff {α : Type u_1} {M N : Matroid α} {X : Set α} (h : N.IsSpanningRestriction M) :

N.Spanning X ↔ M.Spanning X ∧ X ⊆ N.E

theorem Matroid.IsSpanningRestriction.trans {α : Type u_1} {M₁ M₂ M₃ : Matroid α} (h : M₁.IsSpanningRestriction M₂) (h' : M₂.IsSpanningRestriction M₃) :

M₁.IsSpanningRestriction M₃

theorem Matroid.IsSpanningRestriction.exists_eq_restrict {α : Type u_1} {M N : Matroid α} (h : N.IsSpanningRestriction M) :

∃ (R : Set α), M.Spanning R ∧ N = M.restrict R

@[simp]

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

(M.restrict X).IsSpanningRestriction M ↔ M.Spanning X

theorem Matroid.IsSpanningRestriction.isBase_iff {α : Type u_1} {M N : Matroid α} (h : N.IsSpanningRestriction M) {B : Set α} (hBE : B ⊆ N.E := by aesop_mat) :

M.IsBase B ↔ N.IsBase B

theorem Matroid.IsSpanningRestriction.isBase_of_isBase {α : Type u_1} {M N : Matroid α} {B : Set α} (h : N.IsSpanningRestriction M) (hB : N.IsBase B) :

theorem Matroid.Spanning.restrict_isSpanningRestriction {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.Spanning X) :

(M.restrict X).IsSpanningRestriction M

theorem Matroid.ext_closure' {α : Type u_1} {M N : Matroid α} (hE : M.E = N.E) (hX : ∀ X ⊆ M.E, M.closure X = N.closure X) :

M = N

@[simp]

theorem Matroid.closure_union_inter_ground {α : Type u_1} (M : Matroid α) (X Y : Set α) :

M.closure (X ∪ Y ∩ M.E) = M.closure (X ∪ Y)

@[simp]

theorem Matroid.closure_inter_ground_union {α : Type u_1} (M : Matroid α) (X Y : Set α) :

M.closure (X ∩ M.E ∪ Y) = M.closure (X ∪ Y)

@[simp]

theorem Matroid.closure_insert_inter_ground {α : Type u_1} (M : Matroid α) (e : α) (X : Set α) :

M.closure (insert e (X ∩ M.E)) = M.closure (insert e X)