Documentation

Matroid.Loop

source
instance Matroid.instGroundedPredIdIsLoop :
GroundedPred fun {α : Type u_3} => IsLoop
source
instance Matroid.instGroundedPredIdIsColoop :
GroundedPred fun {α : Type u_3} => IsColoop
source
instance Matroid.instGroundedPredIdIsNonloop :
GroundedPred fun {α : Type u_3} => IsNonloop
source
instance Matroid.InvariantFun.isLoop :
InvariantFun (fun {α : Type u_3} => IsLoop) fun {β : Type u_4} => IsLoop
source
instance Matroid.InvariantFun.isNonLoop :
InvariantFun (fun {α : Type u_3} => IsNonloop) fun {β : Type u_4} => IsNonloop
source
instance Matroid.InvariantFun.IsColoop :
InvariantFun (fun {α : Type u_3} => Matroid.IsColoop) fun {β : Type u_4} => Matroid.IsColoop
source
@[simp]
theorem Matroid.isFlat_loops {α : Type u_1} (M : Matroid α) :
M.IsFlat M.loops
source
def Matroid.IsNonColoop {α : Type u_1} (M : Matroid α) (e : α) :
Prop

A non-coloop of M is a nonloop of M✶.

Equations
Instances For
    source
    theorem Matroid.IsNonColoop.mem_ground {α : Type u_1} {M : Matroid α} {e : α} (h : M.IsNonColoop e) :
    e ∈ M.E
    source
    theorem Matroid.IsNonColoop.not_isColoop {α : Type u_1} {M : Matroid α} {e : α} (h : M.IsNonColoop e) :
    ¬M.IsColoop e
    source
    theorem Matroid.IsColoop.not_isNonColoop {α : Type u_1} {M : Matroid α} {e : α} (h : M.IsColoop e) :
    ¬M.IsNonColoop e
    source
    instance Matroid.instGroundedPredIdIsNonColoop :
    GroundedPred fun {α : Type u_3} => IsNonColoop
    source
    instance Matroid.InvariantFun.IsNonColoop :
    InvariantFun (fun {α : Type u_3} => Matroid.IsNonColoop) fun {β : Type u_4} => Matroid.IsNonColoop
    source
    @[simp]
    theorem Matroid.isLoop_map_iff {α : Type u_1} {M : Matroid α} {β : Type u_3} {f : α → β} {x : α} (hf : Set.InjOn f M.E) (hx : x ∈ M.E) :
    (M.map f hf).IsLoop (f x) ↔ M.IsLoop x
    source
    @[simp]
    theorem Matroid.isNonloop_map_iff {α : Type u_1} {M : Matroid α} {β : Type u_3} {f : α → β} {x : α} (hf : Set.InjOn f M.E) (hx : x ∈ M.E) :
    (M.map f hf).IsNonloop (f x) ↔ M.IsNonloop x
    source
    @[simp]
    theorem Matroid.isColoop_map_iff {α : Type u_1} {M : Matroid α} {β : Type u_3} {f : α → β} {x : α} (hf : Set.InjOn f M.E) (hx : x ∈ M.E) :
    (M.map f hf).IsColoop (f x) ↔ M.IsColoop x
    source
    @[simp]
    theorem Matroid.isNonColoop_map_iff {α : Type u_1} {M : Matroid α} {β : Type u_3} {f : α → β} {x : α} (hf : Set.InjOn f M.E) (hx : x ∈ M.E) :
    (M.map f hf).IsNonColoop (f x) ↔ M.IsNonColoop x
    source
    @[simp]
    theorem Matroid.isNonColoop_dual {α : Type u_1} {M : Matroid α} {e : α} :
    M✶.IsNonColoop e ↔ M.IsNonloop e
    source
    @[simp]
    theorem Matroid.isNonloop_dual {α : Type u_1} {M : Matroid α} {e : α} :
    M✶.IsNonloop e ↔ M.IsNonColoop e
    source
    theorem Matroid.IsNonColoop.isNonloop_dual {α : Type u_1} {M : Matroid α} {e : α} :
    M.IsNonColoop e → M✶.IsNonloop e

    Alias of the reverse direction of Matroid.isNonloop_dual.

    source
    theorem Matroid.not_isColoop_iff {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :
    ¬M.IsColoop e ↔ M.IsNonColoop e
    source
    theorem Matroid.not_isNonColoop_iff {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :
    ¬M.IsNonColoop e ↔ M.IsColoop e
    source
    theorem Matroid.isNonColoop_iff {α : Type u_1} {M : Matroid α} {e : α} :
    M.IsNonColoop e ↔ ¬M.IsColoop e ∧ e ∈ M.E
    source
    theorem Matroid.IsNonColoop.coindep {α : Type u_1} {M : Matroid α} {e : α} (h : M.IsNonColoop e) :
    M.Coindep {e}
    source
    theorem Matroid.IsNonColoop.exists_isBase_notMem {α : Type u_1} {M : Matroid α} {e : α} (h : M.IsNonColoop e) :
    ∃ (B : Set α), M.IsBase B ∧ e ∉ B
    source
    theorem Matroid.IsLoop.isNonColoop {α : Type u_1} {M : Matroid α} {e : α} (h : M.IsLoop e) :
    M.IsNonColoop e
    source
    theorem Matroid.coindep_singleton {α : Type u_1} {M : Matroid α} {e : α} :
    M.Coindep {e} ↔ M.IsNonColoop e
    source
    theorem Matroid.isColoop_or_isNonColoop {α : Type u_1} (M : Matroid α) (e : α) (he : e ∈ M.E := by aesop_mat) :
    M.IsColoop e ∨ M.IsNonColoop e
    source
    class Matroid.Coloopless {α : Type u_1} (M : Matroid α) :
    Prop

    A matroid is coloopless if its dual is loopless.

    Instances
      source
      theorem Matroid.coloopless_iff {α : Type u_1} (M : Matroid α) :
      M.Coloopless ↔ M✶.Loopless
      source
      instance Matroid.dual_loopless {α : Type u_1} {M : Matroid α} [M.Coloopless] :
      M✶.Loopless
      source
      instance Matroid.dual_coloopless {α : Type u_1} {M : Matroid α} [M.Loopless] :
      M✶.Coloopless
      source
      theorem Matroid.coloopless_iff_forall {α : Type u_1} {M : Matroid α} :
      M.Coloopless ↔ ∀ e ∈ M.E, M.IsNonColoop e
      source
      @[simp]
      theorem Matroid.coloops_eq_empty {α : Type u_1} (M : Matroid α) [M.Coloopless] :
      M.coloops = ∅
      source
      theorem Matroid.Coloopless.coloops_eq_empty {α : Type u_1} {M : Matroid α} (hM : M.Coloopless) :
      M.coloops = ∅
      source
      theorem Matroid.coloops_eq_empty_iff {α : Type u_1} {M : Matroid α} :
      M.coloops = ∅ ↔ M.Coloopless
      source
      @[simp]
      theorem Matroid.dual_loopless_iff {α : Type u_1} {M : Matroid α} :
      M✶.Loopless ↔ M.Coloopless
      source
      @[simp]
      theorem Matroid.dual_coloopless_iff {α : Type u_1} {M : Matroid α} :
      M✶.Coloopless ↔ M.Loopless
      source
      theorem Matroid.isNonColoop_of_mem {α : Type u_1} {M : Matroid α} {e : α} [M.Coloopless] (he : e ∈ M.E) :
      M.IsNonColoop e
      source
      theorem Matroid.Loopless.subsingleton_indep {α : Type u_1} {M : Matroid α} {X : Set α} (hM : M.Loopless) (hX : X.Subsingleton) (hXE : X ⊆ M.E := by aesop_mat) :
      M.Indep X
      source
      theorem Matroid.Coloopless.subsingleton_coindep {α : Type u_1} {M : Matroid α} {X : Set α} (hM : M.Coloopless) (hX : X.Subsingleton) (hXE : X ⊆ M.E := by aesop_mat) :
      M.Coindep X
      source
      @[simp]
      theorem Matroid.mem_loops_iff {α : Type u_1} {M : Matroid α} {e : α} :
      e ∈ M.loops ↔ M.IsLoop e
      source
      @[simp]
      theorem Matroid.disjointSigma_isLoop_iff {α : Type u_1} {e : α} {ι : Type u_3} {M : ι → Matroid α} (hdj : Pairwise (Function.onFun Disjoint fun (i : ι) => (M i).E)) :
      (Matroid.disjointSigma M hdj).IsLoop e ↔ ∃ (i : ι), (M i).IsLoop e
      source
      @[simp]
      theorem Matroid.disjointSigma_isNonloop_iff {α : Type u_1} {e : α} {ι : Type u_3} {M : ι → Matroid α} (hdj : Pairwise (Function.onFun Disjoint fun (i : ι) => (M i).E)) :
      (Matroid.disjointSigma M hdj).IsNonloop e ↔ ∃ (i : ι), (M i).IsNonloop e
      source
      @[simp]
      theorem Matroid.disjointSum_isNonloop_iff {α : Type u_1} {e : α} {M N : Matroid α} (hMN : Disjoint M.E N.E) :
      (M.disjointSum N hMN).IsNonloop e ↔ M.IsNonloop e ∨ N.IsNonloop e
      source
      @[simp]
      theorem Matroid.disjointSum_isLoop_iff {α : Type u_1} {e : α} {M N : Matroid α} (hMN : Disjoint M.E N.E) :
      (M.disjointSum N hMN).IsLoop e ↔ M.IsLoop e ∨ N.IsLoop e
      source
      @[simp]
      theorem Matroid.disjointSigma_loops {α : Type u_1} {ι : Type u_3} {M : ι → Matroid α} (hdj : Pairwise (Function.onFun Disjoint fun (i : ι) => (M i).E)) :
      (Matroid.disjointSigma M hdj).loops = ⋃ (i : ι), (M i).loops
      source
      @[simp]
      theorem Matroid.disjointSum_loops {α : Type u_1} {M N : Matroid α} (hMN : Disjoint M.E N.E) :
      (M.disjointSum N hMN).loops = M.loops ∪ N.loops
      source
      @[simp]
      theorem Matroid.sigma_loops_eq {ι : Type u_3} {α : ι → Type u_4} {M : (i : ι) → Matroid (α i)} :
      (Matroid.sigma M).loops = ⋃ (i : ι), Sigma.mk i '' (M i).loops
      source
      @[simp]
      theorem Matroid.sum_loops_eq {α : Type u_1} {β : Type u_2} (M : Matroid α) (N : Matroid β) :
      (M.sum N).loops = Sum.inl '' M.loops ∪ Sum.inr '' N.loops
      source
      theorem Matroid.loops_disjoint_setOf_isNonloop {α : Type u_1} (M : Matroid α) :
      Disjoint M.loops {e : α | M.IsNonloop e}
      source
      theorem Matroid.loops_disjoint_coloops {α : Type u_1} (M : Matroid α) :
      Disjoint M.loops M.coloops
      source
      theorem Matroid.Loopless.isNonloop_of_mem {α : Type u_1} {M : Matroid α} {e : α} (h : M.Loopless) (he : e ∈ M.E) :
      M.IsNonloop e

      a version of isNonloop_of_loopless that works with dot notation

      source
      theorem Matroid.Coloopless.isNonColoop_of_mem {α : Type u_1} {M : Matroid α} {e : α} (hM : M.Coloopless) (he : e ∈ M.E) :
      M.IsNonColoop e
      source
      theorem Matroid.Loopless.not_isLoop {α : Type u_1} {M : Matroid α} (h : M.Loopless) (e : α) :
      ¬M.IsLoop e
      source
      theorem Matroid.removeLoops_ground_eq_diff {α : Type u_1} {M : Matroid α} :
      M.removeLoops.E = M.E \ M.loops
      source
      instance Matroid.removeLoops_rankPos {α : Type u_1} {M : Matroid α} [M.RankPos] :
      M.removeLoops.RankPos
      source
      def Matroid.removeColoops {α : Type u_1} (M : Matroid α) :
      Matroid α

      remove the coloops of a matroid M.

      Equations
      Instances For
        source
        theorem Matroid.removeLoops_dual {α : Type u_1} {M : Matroid α} :
        M.removeLoops✶ = M✶.removeColoops
        source
        theorem Matroid.removeColoops_dual {α : Type u_1} {M : Matroid α} :
        M.removeColoops✶ = M✶.removeLoops
        source
        @[simp]
        theorem Matroid.removeColoops_coloops {α : Type u_1} {M : Matroid α} :
        M.removeColoops.coloops = ∅
        source
        theorem Matroid.union_dep_iff_dep_of_subset_coloops {α : Type u_1} {M : Matroid α} {D X : Set α} (hX : X ⊆ M.coloops) :
        M.Dep (D ∪ X) ↔ M.Dep D
        source
        theorem Matroid.diff_dep_iff_dep_of_subset_coloops {α : Type u_1} {M : Matroid α} {D X : Set α} (hX : X ⊆ M.coloops) :
        M.Dep (D \ X) ↔ M.Dep D
        source
        @[simp]
        theorem Matroid.removeColoops_eq_self {α : Type u_1} (M : Matroid α) [M.Coloopless] :
        M.removeColoops = M
        source
        instance Matroid.removeColoops_coloopless {α : Type u_1} (M : Matroid α) :
        M.removeColoops.Coloopless
        source
        @[simp]
        theorem Matroid.union_coloops_dep_iff {α : Type u_1} {M : Matroid α} {X : Set α} :
        M.Dep (X ∪ M.coloops) ↔ M.Dep X
        source
        theorem Matroid.union_coindep_iff_coindep_of_subset_loops {α : Type u_1} {M : Matroid α} {I X : Set α} (hX : X ⊆ M.loops) :
        M.Coindep (I ∪ X) ↔ M.Coindep I
        source
        @[simp]
        theorem Matroid.union_loops_coindep_iff {α : Type u_1} {M : Matroid α} {X : Set α} :
        M.Coindep (X ∪ M.loops) ↔ M.Coindep X
        source
        theorem Matroid.union_codep_iff_codep_of_subset_loops {α : Type u_1} {M : Matroid α} {I X : Set α} (hX : X ⊆ M.loops) :
        M.Codep (I ∪ X) ↔ M.Codep I
        source
        @[simp]
        theorem Matroid.union_loops_codep_iff {α : Type u_1} {M : Matroid α} {X : Set α} :
        M.Codep (X ∪ M.loops) ↔ M.Codep X
        source
        theorem Matroid.eRk_union_eq_of_subset_coloops {α : Type u_1} {M : Matroid α} {K : Set α} (X : Set α) (hK : K ⊆ M.coloops) :
        M.eRk (X ∪ K) = M.eRk X + (K \ X).encard
        source
        @[simp]
        theorem Matroid.loops_indep_iff {α : Type u_1} {M : Matroid α} :
        M.Indep M.loops ↔ M.Loopless
        source
        @[simp]
        theorem Matroid.loops_dep_iff {α : Type u_1} {M : Matroid α} :
        M.Dep M.loops ↔ M.loops.Nonempty
        source
        @[simp]
        theorem Matroid.coloops_coindep_iff {α : Type u_1} {M : Matroid α} :
        M.Coindep M.coloops ↔ M✶.Loopless
        source
        @[simp]
        theorem Matroid.coloops_codep_iff {α : Type u_1} {M : Matroid α} :
        M.Codep M.coloops ↔ M.coloops.Nonempty
        source
        @[simp]
        theorem Matroid.closure_coloops {α : Type u_1} (M : Matroid α) :
        M.closure M.coloops = M.coloops ∪ M.loops
        source
        @[simp]
        theorem Matroid.loops_subset_closure {α : Type u_1} (M : Matroid α) (X : Set α) :
        M.loops ⊆ M.closure X
        source
        def Matroid.IsLoopEquiv {α : Type u_1} (M : Matroid α) (X Y : Set α) :
        Prop

        Two sets are IsLoopEquiv in M if their symmetric difference contains only loops.

        Equations
        Instances For
          source
          theorem Matroid.isLoopEquiv_iff_union_eq_union {α : Type u_1} {M : Matroid α} {X Y : Set α} :
          M.IsLoopEquiv X Y ↔ X ∪ M.loops = Y ∪ M.loops
          source
          theorem Matroid.IsLoopEquiv.union_eq_union {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsLoopEquiv X Y) :
          X ∪ M.loops = Y ∪ M.loops
          source
          theorem Matroid.IsLoopEquiv.diff_eq_diff {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsLoopEquiv X Y) :
          X \ M.loops = Y \ M.loops
          source
          theorem Matroid.IsLoopEquiv.rfl {α : Type u_1} (M : Matroid α) {X : Set α} :
          M.IsLoopEquiv X X
          source
          theorem Matroid.IsLoopEquiv.symm {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsLoopEquiv X Y) :
          M.IsLoopEquiv Y X
          source
          theorem Matroid.IsLoopEquiv.comm {α : Type u_1} {M : Matroid α} {X Y : Set α} :
          M.IsLoopEquiv X Y ↔ M.IsLoopEquiv Y X
          source
          theorem Matroid.IsLoopEquiv.trans {α : Type u_1} {M : Matroid α} {X Y Z : Set α} (hXY : M.IsLoopEquiv X Y) (hYZ : M.IsLoopEquiv Y Z) :
          M.IsLoopEquiv X Z
          source
          theorem Matroid.IsLoopEquiv.diff_subset_loops {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsLoopEquiv X Y) :
          X \ Y ⊆ M.loops
          source
          theorem Matroid.IsLoopEquiv.symmDiff_subset_loops {α : Type u_1} {M : Matroid α} {X Y : Set α} :
          M.IsLoopEquiv X Y ↔ symmDiff X Y ⊆ M.loops
          source
          theorem Matroid.isLoopEquiv_union {α : Type u_1} {M : Matroid α} {L : Set α} (X : Set α) (hL : L ⊆ M.loops) :
          M.IsLoopEquiv X (X ∪ L)
          source
          theorem Matroid.isLoopEquiv_diff {α : Type u_1} {M : Matroid α} {L : Set α} (X : Set α) (hL : L ⊆ M.loops) :
          M.IsLoopEquiv X (X \ L)
          source
          theorem Matroid.isLoopEquiv_union_diff {α : Type u_1} {M : Matroid α} {L L' : Set α} (X : Set α) (hL : L ⊆ M.loops) (hL' : L' ⊆ M.loops) :
          M.IsLoopEquiv X ((X ∪ L) \ L')
          source
          theorem Matroid.isLoopEquiv_union_loops {α : Type u_1} (M : Matroid α) (X : Set α) :
          M.IsLoopEquiv X (X ∪ M.loops)
          source
          theorem Matroid.isLoopEquiv_diff_loops {α : Type u_1} (M : Matroid α) (X : Set α) :
          M.IsLoopEquiv X (X \ M.loops)
          source
          theorem Matroid.IsLoopEquiv.exists_diff_union_loops {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsLoopEquiv X Y) :
          ∃ (L : Set α) (L' : Set α), L ⊆ M.loops ∧ L' ⊆ M.loops ∧ Y = (X ∪ L) \ L'
          source
          theorem Matroid.IsLoopEquiv.subset_union_loops {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsLoopEquiv X Y) :
          Y ⊆ X ∪ M.loops
          source
          theorem Matroid.IsLoopEquiv.closure_eq_closure {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsLoopEquiv X Y) :
          M.closure X = M.closure Y
          source
          theorem Matroid.IsLoopEquiv.subset_ground {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsLoopEquiv X Y) (hX : X ⊆ M.E := by aesop_mat) :
          Y ⊆ M.E
          source
          theorem Matroid.IsLoopEquiv.inter_eq_of_indep {α : Type u_1} {M : Matroid α} {I X Y : Set α} (h : M.IsLoopEquiv X Y) (hI : M.Indep I) :
          X ∩ I = Y ∩ I
          source
          theorem Matroid.IsLoopEquiv.subset_iff_of_indep {α : Type u_1} {M : Matroid α} {I X Y : Set α} (h : M.IsLoopEquiv X Y) (hI : M.Indep I) :
          I ⊆ X ↔ I ⊆ Y
          source
          theorem Matroid.IsLoopEquiv.isBasis_iff {α : Type u_1} {M : Matroid α} {I X Y : Set α} (h : M.IsLoopEquiv X Y) :
          M.IsBasis I X ↔ M.IsBasis I Y
          source
          theorem Matroid.isBasis_union_iff_isBasis_of_subset_loops {α : Type u_1} {M : Matroid α} {L I X : Set α} (hL : L ⊆ M.loops) :
          M.IsBasis I (X ∪ L) ↔ M.IsBasis I X
          source
          theorem Matroid.isBasis_diff_iff_isBasis_of_subset_loops {α : Type u_1} {M : Matroid α} {L I X : Set α} (hL : L ⊆ M.loops) :
          M.IsBasis I (X \ L) ↔ M.IsBasis I X
          source
          theorem Matroid.closure_union_eq_closure_of_subset_loops {α : Type u_1} {Y : Set α} (M : Matroid α) (X : Set α) (hY : Y ⊆ M.loops) :
          M.closure (X ∪ Y) = M.closure X
          source
          theorem Matroid.closure_diff_eq_closure_of_subset_loops {α : Type u_1} {Y : Set α} (M : Matroid α) (X : Set α) (hY : Y ⊆ M.loops) :
          M.closure (X \ Y) = M.closure X
          source
          instance Matroid.freeOn_loopless {α : Type u_1} (E : Set α) :
          (freeOn E).Loopless
          source
          instance Matroid.loopless_dual_loopyOn {α : Type u_1} {E : Set α} :
          (loopyOn E)✶.Loopless
          source
          @[simp]
          theorem Matroid.OnUniv.toIsNonloop {α : Type u_1} {M : Matroid α} [M.Loopless] [M.OnUniv] (e : α) :
          M.IsNonloop e
          source
          @[simp]
          theorem Matroid.one_lt_girth_iff {α : Type u_1} {M : Matroid α} :
          1 < M.girth ↔ M.Loopless
          source
          @[simp]
          theorem Matroid.two_le_girth_iff {α : Type u_1} {M : Matroid α} :
          2 ≤ M.girth ↔ M.Loopless
          source
          @[simp]
          theorem Matroid.removeLoops_isNonloop_iff {α : Type u_1} {M : Matroid α} {e : α} :
          M.removeLoops.IsNonloop e ↔ M.IsNonloop e
          source
          @[simp]
          theorem Matroid.removeLoops_removeLoops {α : Type u_1} {M : Matroid α} :
          M.removeLoops.removeLoops = M.removeLoops
          source
          @[simp]
          theorem Matroid.removeColoops_removeColoops {α : Type u_1} {M : Matroid α} :
          M.removeColoops.removeColoops = M.removeColoops
          source
          @[simp]
          theorem Matroid.loopyOn_loops {α : Type u_1} (E : Set α) :
          (loopyOn E).loops = E
          source
          @[simp]
          theorem Matroid.loopyOn_coloops {α : Type u_1} (E : Set α) :
          (loopyOn E).coloops = ∅
          source
          instance Matroid.loopyOn_coloopless {α : Type u_1} {E : Set α} :
          (loopyOn E).Coloopless
          source
          instance Matroid.emptyOn_coloopless {α : Type u_3} :
          (emptyOn α).Coloopless
          source
          @[simp]
          theorem Matroid.loopyOn_not_isNonloop {α : Type u_1} (E : Set α) (e : α) :
          ¬(loopyOn E).IsNonloop e
          source
          @[simp]
          theorem Matroid.removeLoops_isColoop_eq {α : Type u_1} (M : Matroid α) :
          M.removeLoops.IsColoop = M.IsColoop
          source
          @[simp]
          theorem Matroid.removeLoops_coloops_eq {α : Type u_1} (M : Matroid α) :
          M.removeLoops.coloops = M.coloops
          source
          @[simp]
          theorem Matroid.removeColoops_loops_eq {α : Type u_1} (M : Matroid α) :
          M.removeColoops.loops = M.loops
          source
          @[simp]
          theorem Matroid.loopyOn_removeLoops {α : Type u_1} (E : Set α) :
          (loopyOn E).removeLoops = emptyOn α
          source
          @[simp]
          theorem Matroid.loopyOn_removeColoops {α : Type u_1} (E : Set α) :
          (loopyOn E).removeColoops = loopyOn E
          source
          @[simp]
          theorem Matroid.freeOn_removeColoops {α : Type u_1} (E : Set α) :
          (freeOn E).removeColoops = emptyOn α
          source
          theorem Matroid.restrict_removeLoops {α : Type u_1} {M : Matroid α} (R : Set α) :
          (M.restrict R).removeLoops = (M.restrict (R ∩ M.E)).removeLoops
          source
          @[simp]
          theorem Matroid.disjointSigma_removeLoops {α : Type u_1} {ι : Type u_3} (M : ι → Matroid α) (hdj : Pairwise (Function.onFun Disjoint fun (i : ι) => (M i).E)) :
          (Matroid.disjointSigma M hdj).removeLoops = Matroid.disjointSigma (fun (i : ι) => (M i).removeLoops) ⋯
          source
          @[simp]
          theorem Matroid.disjointSum_removeLoops {α : Type u_1} {M N : Matroid α} (hMN : Disjoint M.E N.E) :
          (M.disjointSum N hMN).removeLoops = M.removeLoops.disjointSum N.removeLoops ⋯
          source
          @[simp]
          theorem Matroid.disjointSigma_removeColoops {α : Type u_1} {ι : Type u_3} (M : ι → Matroid α) (hdj : Pairwise (Function.onFun Disjoint fun (i : ι) => (M i).E)) :
          (Matroid.disjointSigma M hdj).removeColoops = Matroid.disjointSigma (fun (i : ι) => (M i).removeColoops) ⋯
          source
          @[simp]
          theorem Matroid.disjointSum_removeColoops {α : Type u_1} {M N : Matroid α} (hMN : Disjoint M.E N.E) :
          (M.disjointSum N hMN).removeColoops = M.removeColoops.disjointSum N.removeColoops ⋯
          source
          theorem Matroid.eq_uniqueBaseOn_of_loops_union_coloops {α : Type u_1} {M : Matroid α} (hE : M.E = M.loops ∪ M.coloops) :
          M = uniqueBaseOn M.coloops M.E
          source
          theorem Matroid.exists_eq_uniqueBaseOn_of_loops_union_coloops {α : Type u_1} {M : Matroid α} (hE : M.E = M.loops ∪ M.coloops) :
          ∃ (B : Set α) (E : Set α), B ⊆ E ∧ M = uniqueBaseOn B E
          source
          theorem Matroid.exists_eq_uniqueBaseOn_or_removeColoops_rankPos {α : Type u_1} (M : Matroid α) :
          (∃ (B : Set α) (E : Set α), B ⊆ E ∧ M = uniqueBaseOn B E) ∨ M.removeColoops.RankPos
          source
          theorem Matroid.uniqueBaseOn_loops_eq {α : Type u_1} (I E : Set α) :
          (uniqueBaseOn I E).loops = E \ I
          source
          @[simp]
          theorem Matroid.uniqueBaseOn_coloops_eq' {α : Type u_1} (I E : Set α) :
          (uniqueBaseOn I E).coloops = I ∩ E
          source
          theorem Matroid.uniqueBaseOn_coloops_eq {α : Type u_1} {I E : Set α} (h : I ⊆ E) :
          (uniqueBaseOn I E).coloops = I
          source
          theorem Matroid.IsNonloop.isNonloop_of_isRestriction_of_mem {α : Type u_1} {M N : Matroid α} {e : α} (he : M.IsNonloop e) (hNM : N.IsRestriction M) (heN : e ∈ N.E) :
          N.IsNonloop e
          source
          theorem Matroid.IsRestriction.isNonloop_iff {α : Type u_1} {M N : Matroid α} {e : α} (hNM : N.IsRestriction M) :
          N.IsNonloop e ↔ M.IsNonloop e ∧ e ∈ N.E
          source
          theorem Matroid.IsLoop.isLoop_of_isRestriction_of_mem {α : Type u_1} {M N : Matroid α} {e : α} (he : M.IsLoop e) (hNM : N.IsRestriction M) (heN : e ∈ N.E) :
          N.IsLoop e
          source
          def Matroid.loopComap {α : Type u_3} {β : Type u_4} (M : Matroid β) (f : α → Option β) :
          Matroid α

          Given a function f : α → Option β and a matroid M on type β, the Matroid α obtained by pulling back M along f, and setting every e with f e = none to be a loop

          Equations
          Instances For
            source
            @[simp]
            theorem Matroid.loopComap_ground_eq {α : Type u_1} {β : Type u_2} (M : Matroid β) (f : α → Option β) :
            (M.loopComap f).E = f ⁻¹' insert none (some '' M.E)
            source
            theorem Matroid.loopComap_indep_iff {α : Type u_1} {β : Type u_2} {I : Set α} {M : Matroid β} {f : α → Option β} :
            (M.loopComap f).Indep I ↔ ∃ (I₀ : Set β), M.Indep I₀ ∧ Set.BijOn f I (some '' I₀)
            source
            theorem Matroid.loopComap_closure_eq {α : Type u_1} {β : Type u_2} (M : Matroid β) (f : α → Option β) (X : Set α) :
            (M.loopComap f).closure X = f ⁻¹' some '' M.closure (some ⁻¹' f '' X) ∪ f ⁻¹' {none}
            source
            theorem Matroid.loopComap_subset_loops_preimage_none {α : Type u_1} {β : Type u_2} (M : Matroid β) (f : α → Option β) :
            f ⁻¹' {none} ⊆ (M.loopComap f).loops