Loogle!

Result

Found 238 declarations mentioning Matroid.closure. Of these, only the first 200 are shown.

• Matroid.closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) (X : Set α) : Set α
• Matroid.isFlat_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} (X : Set α) : M.IsFlat (M.closure X)
• Matroid.closure_univ 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) : M.closure Set.univ = M.E
• Matroid.closure_ground 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) : M.closure M.E = M.E
• Matroid.loopyOn_closure_eq 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (E X : Set α) : (Matroid.loopyOn E).closure X = E
• Matroid.emptyOn_closure_eq 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (X : Set α) : (Matroid.emptyOn α).closure X = ∅
• Matroid.closure_subset_ground 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) (X : Set α) : M.closure X ⊆ M.E
• Matroid.Indep.isBasis_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {I : Set α} (hI : M.Indep I) : M.IsBasis I (M.closure I)
• Matroid.IsFlat.closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {F : Set α} (hF : M.IsFlat F) : M.closure F = F
• Matroid.isFlat_iff_closure_eq 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {F : Set α} : M.IsFlat F ↔ M.closure F = F
• Matroid.closure_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) (X : Set α) : M.closure (M.closure X) = M.closure X
• Matroid.IsBase.closure_eq 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {B : Set α} (hB : M.IsBase B) : M.closure B = M.E
• Matroid.Spanning.closure_eq 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {S : Set α} (self : M.Spanning S) : M.closure S = M.E
• Matroid.IsBasis.isBasis_closure_right 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X I : Set α} (h : M.IsBasis I X) : M.IsBasis I (M.closure X)
• Matroid.IsBasis'.isBasis_closure_right 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X I : Set α} (h : M.IsBasis' I X) : M.IsBasis I (M.closure X)
• Matroid.freeOn_closure_eq 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (E X : Set α) : (Matroid.freeOn E).closure X = X ∩ E
• Matroid.IsBasis.subset_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X I : Set α} (h : M.IsBasis I X) : X ⊆ M.closure I
• Matroid.ext_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M₁ M₂ : Matroid α} (h : ∀ (X : Set α), M₁.closure X = M₂.closure X) : M₁ = M₂
• Matroid.inter_ground_subset_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) (X : Set α) : X ∩ M.E ⊆ M.closure X
• Matroid.IsBasis.closure_eq_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X I : Set α} (h : M.IsBasis I X) : M.closure I = M.closure X
• Matroid.IsBasis'.closure_eq_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X I : Set α} (h : M.IsBasis' I X) : M.closure I = M.closure X
• Matroid.closure_inter_ground 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) (X : Set α) : M.closure (X ∩ M.E) = M.closure X
• Matroid.isBase_iff_indep_closure_eq 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {B : Set α} : M.IsBase B ↔ M.Indep B ∧ M.closure B = M.E
• Matroid.Indep.isBase_of_ground_subset_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {I : Set α} (hI : M.Indep I) (h : M.E ⊆ M.closure I) : M.IsBase I
• Matroid.subset_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) (X : Set α) (hX : X ⊆ M.E := by aesop_mat) : X ⊆ M.closure X
• Matroid.Indep.isBase_iff_ground_subset_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {I : Set α} (hI : M.Indep I) : M.IsBase I ↔ M.E ⊆ M.closure I
• Matroid.IsBasis.closure_eq_right 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X I : Set α} (h : M.IsBasis I (M.closure X)) : M.closure I = M.closure X
• Matroid.closure_empty_eq_ground_iff 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} : M.closure ∅ = M.E ↔ M = Matroid.loopyOn M.E
• Matroid.closure_subset_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {X Y : Set α} (M : Matroid α) (h : X ⊆ Y) : M.closure X ⊆ M.closure Y
• Matroid.mem_ground_of_mem_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X : Set α} {e : α} (he : e ∈ M.closure X) : e ∈ M.E
• Matroid.Coindep.closure_compl 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X : Set α} (hX : M.Coindep X) : M.closure (M.E \ X) = M.E
• Matroid.closure_spanning_iff 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {S : Set α} (hS : S ⊆ M.E := by aesop_mat) : M.Spanning (M.closure S) ↔ M.Spanning S
• Matroid.ground_subset_closure_iff 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X : Set α} : M.E ⊆ M.closure X ↔ M.closure X = M.E
• Matroid.IsBase.closure_of_superset 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X B : Set α} (hB : M.IsBase B) (hBX : B ⊆ X) : M.closure X = M.E
• Matroid.Spanning.closure_eq_of_superset 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {S T : Set α} (hS : M.Spanning S) (hST : S ⊆ T) : M.closure T = M.E
• Matroid.Spanning.mk 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {S : Set α} (closure_eq : M.closure S = M.E) (subset_ground : S ⊆ M.E) : M.Spanning S
• Matroid.closure_empty_union_closure_eq 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) (X : Set α) : M.closure ∅ ∪ M.closure X = M.closure X
• Matroid.closure_union_closure_empty_eq 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) (X : Set α) : M.closure X ∪ M.closure ∅ = M.closure X
• Matroid.empty_isBasis_iff 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X : Set α} : M.IsBasis ∅ X ↔ X ⊆ M.closure ∅
• Matroid.isBasis'_iff_isBasis_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X I : Set α} : M.IsBasis' I X ↔ M.IsBasis I (M.closure X) ∧ I ⊆ X
• Matroid.closure_subset_closure_of_subset_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X Y : Set α} (hXY : X ⊆ M.closure Y) : M.closure X ⊆ M.closure Y
• Matroid.spanning_iff 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) (S : Set α) : M.Spanning S ↔ M.closure S = M.E ∧ S ⊆ M.E
• Matroid.closure_iUnion_closure_eq_closure_iUnion 📋 Mathlib.Combinatorics.Matroid.Closure
  {ι : Type u_1} {α : Type u_2} (M : Matroid α) (Xs : ι → Set α) : M.closure (⋃ i, M.closure (Xs i)) = M.closure (⋃ i, Xs i)
• Matroid.comap_closure_eq 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {β : Type u_3} (M : Matroid β) (f : α → β) (X : Set α) : (M.comap f).closure X = f ⁻¹' M.closure (f '' X)
• Matroid.spanning_iff_closure_eq 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {S : Set α} (hS : S ⊆ M.E := by aesop_mat) : M.Spanning S ↔ M.closure S = M.E
• Matroid.Indep.closure_eq_setOfPred_isBasis_insert 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {I : Set α} (hI : M.Indep I) : M.closure I = {x | M.IsBasis I (insert x I)}
• Matroid.Indep.closure_eq_setOf_isBasis_insert 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {I : Set α} (hI : M.Indep I) : M.closure I = {x | M.IsBasis I (insert x I)}
• Matroid.exists_isBasis_inter_ground_isBasis_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) (X : Set α) : ∃ I, M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)
• Matroid.Indep.closure_inter_eq_self_of_subset 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {I J : Set α} (hI : M.Indep I) (hJI : J ⊆ I) : M.closure J ∩ I = J
• Matroid.closure_union_closure_left_eq 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) (X Y : Set α) : M.closure (M.closure X ∪ Y) = M.closure (X ∪ Y)
• Matroid.closure_union_closure_right_eq 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) (X Y : Set α) : M.closure (X ∪ M.closure Y) = M.closure (X ∪ Y)
• Matroid.mem_closure_self 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) (e : α) (he : e ∈ M.E := by aesop_mat) : e ∈ M.closure {e}
• Matroid.spanning_iff_ground_subset_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {S : Set α} (hS : S ⊆ M.E := by aesop_mat) : M.Spanning S ↔ M.E ⊆ M.closure S
• Matroid.Indep.isBasis_of_subset_of_subset_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X I : Set α} (hI : M.Indep I) (hIX : I ⊆ X) (hXI : X ⊆ M.closure I) : M.IsBasis I X
• Matroid.closure_insert_closure_eq_closure_insert 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) (e : α) (X : Set α) : M.closure (insert e (M.closure X)) = M.closure (insert e X)
• Matroid.isBasis_union_iff_indep_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X I : Set α} : M.IsBasis I (I ∪ X) ↔ M.Indep I ∧ X ⊆ M.closure I
• Matroid.notMem_of_mem_diff_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X : Set α} {e : α} (he : e ∈ M.E \ M.closure X) : e ∉ X
• Matroid.notMem_of_mem_sdiff_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X : Set α} {e : α} (he : e ∈ M.E \ M.closure X) : e ∉ X
• Matroid.Indep.insert_isBasis_iff_mem_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) : M.IsBasis I (insert e I) ↔ e ∈ M.closure I
• Matroid.closure_insert_eq_of_mem_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X : Set α} {e : α} (he : e ∈ M.closure X) : M.closure (insert e X) = M.closure X
• Matroid.subset_closure_of_subset 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {X Y : Set α} (M : Matroid α) (hXY : X ⊆ Y) (hY : Y ⊆ M.E := by aesop_mat) : X ⊆ M.closure Y
• Matroid.subset_closure_of_subset' 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {X Y : Set α} (M : Matroid α) (hXY : X ⊆ Y) (hX : X ⊆ M.E := by aesop_mat) : X ⊆ M.closure Y
• Matroid.closure_closure_union_closure_eq_closure_union 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) (X Y : Set α) : M.closure (M.closure X ∪ M.closure Y) = M.closure (X ∪ Y)
• Matroid.isBasis_iff_indep_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X I : Set α} : M.IsBasis I X ↔ M.Indep I ∧ X ⊆ M.closure I ∧ I ⊆ X
• Matroid.isBasis_iff_indep_subset_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X I : Set α} : M.IsBasis I X ↔ M.Indep I ∧ I ⊆ X ∧ X ⊆ M.closure I
• Matroid.mem_closure_of_mem 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {X : Set α} {e : α} (M : Matroid α) (h : e ∈ X) (hX : X ⊆ M.E := by aesop_mat) : e ∈ M.closure X
• Matroid.IsBasis.eq_of_closure_subset 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X I J : Set α} (hI : M.IsBasis I X) (hJI : J ⊆ I) (hJ : X ⊆ M.closure J) : J = I
• Matroid.mem_closure_of_mem' 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {X : Set α} {e : α} (M : Matroid α) (heX : e ∈ X) (h : e ∈ M.E := by aesop_mat) : e ∈ M.closure X
• Matroid.isBasis_iff_isBasis_closure_of_subset' 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X I : Set α} (hIX : I ⊆ X) : M.IsBasis I X ↔ M.IsBasis I (M.closure X) ∧ X ⊆ M.E
• Matroid.closure_def 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) (X : Set α) : M.closure X = ⋂₀ {F | M.IsFlat F ∧ X ∩ M.E ⊆ F}
• Matroid.closure_iInter_eq_iInter_closure_of_iUnion_indep 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {ι : Sort u_3} [hι : Nonempty ι] (Is : ι → Set α) (h : M.Indep (⋃ i, Is i)) : M.closure (⋂ i, Is i) = ⋂ i, M.closure (Is i)
• Matroid.coindep_iff_closure_compl_eq_ground 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X : Set α} (hK : X ⊆ M.E := by aesop_mat) : M.Coindep X ↔ M.closure (M.E \ X) = M.E
• Matroid.isBasis_iff_isBasis_closure_of_subset 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X I : Set α} (hIX : I ⊆ X) (hX : X ⊆ M.E := by aesop_mat) : M.IsBasis I X ↔ M.IsBasis I (M.closure X)
• Matroid.map_closure_eq 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {β : Type u_3} (M : Matroid α) (f : α → β) (hf : Set.InjOn f M.E) (X : Set β) : (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)
• Matroid.Indep.insert_dep_iff 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) : M.Dep (insert e I) ↔ e ∈ M.closure I \ I
• Matroid.Indep.inter_isBasis_closure_iff_subset_closure_inter 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {I X : Set α} (hI : M.Indep I) : M.IsBasis (X ∩ I) X ↔ X ⊆ M.closure (X ∩ I)
• Matroid.IsBasis.closure_inter_isBasis_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X I : Set α} (h : M.IsBasis (X ∩ I) X) (hI : M.Indep I) : M.IsBasis (M.closure X ∩ I) (M.closure X)
• Matroid.closure_diff_eq_self 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X Y : Set α} (h : Y ⊆ M.closure (X \ Y)) : M.closure (X \ Y) = M.closure X
• Matroid.closure_sdiff_eq_self 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X Y : Set α} (h : Y ⊆ M.closure (X \ Y)) : M.closure (X \ Y) = M.closure X
• Matroid.restrict_spanning_iff' 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {R S : Set α} : (M.restrict R).Spanning S ↔ R ∩ M.E ⊆ M.closure S ∧ S ⊆ R
• Matroid.closure_def' 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) (X : Set α) (hX : X ⊆ M.E := by aesop_mat) : M.closure X = ⋂₀ {F | M.IsFlat F ∧ X ⊆ F}
• Matroid.closure_subset_closure_iff_subset_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X Y : Set α} (hX : X ⊆ M.E := by aesop_mat) : M.closure X ⊆ M.closure Y ↔ X ⊆ M.closure Y
• Matroid.indep_iff_forall_closure_diff_ne 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {I : Set α} : M.Indep I ↔ ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
• Matroid.indep_iff_forall_closure_sdiff_ne 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {I : Set α} : M.Indep I ↔ ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
• Matroid.uniqueBaseOn_closure_eq 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (I E X : Set α) : (Matroid.uniqueBaseOn I E).closure X = X ∩ I ∩ E ∪ E \ I
• Matroid.Indep.mem_closure_iff 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {I : Set α} {x : α} (hI : M.Indep I) : x ∈ M.closure I ↔ M.Dep (insert x I) ∨ x ∈ I
• Matroid.Indep.mem_closure_iff_of_notMem 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) (heI : e ∉ I) : e ∈ M.closure I ↔ M.Dep (insert e I)
• Matroid.Indep.notMem_closure_diff_of_mem 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) (he : e ∈ I) : e ∉ M.closure (I \ {e})
• Matroid.Indep.notMem_closure_sdiff_of_mem 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) (he : e ∈ I) : e ∉ M.closure (I \ {e})
• Matroid.closure_union_congr_left 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X Y X' : Set α} (h : M.closure X = M.closure X') : M.closure (X ∪ Y) = M.closure (X' ∪ Y)
• Matroid.closure_union_congr_right 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X Y Y' : Set α} (h : M.closure Y = M.closure Y') : M.closure (X ∪ Y) = M.closure (X ∪ Y')
• Matroid.restrict_spanning_iff 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {R S : Set α} (hSR : S ⊆ R) (hR : R ⊆ M.E := by aesop_mat) : (M.restrict R).Spanning S ↔ R ⊆ M.closure S
• Matroid.Indep.closure_inter_eq_inter_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {I J : Set α} (h : M.Indep (I ∪ J)) : M.closure (I ∩ J) = M.closure I ∩ M.closure J
• Matroid.closure_insert_congr_right 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X Y : Set α} {e : α} (h : M.closure X = M.closure Y) : M.closure (insert e X) = M.closure (insert e Y)
• Matroid.closure_iUnion_congr 📋 Mathlib.Combinatorics.Matroid.Closure
  {ι : Type u_1} {α : Type u_2} {M : Matroid α} (Xs Ys : ι → Set α) (h : ∀ (i : ι), M.closure (Xs i) = M.closure (Ys i)) : M.closure (⋃ i, Xs i) = M.closure (⋃ i, Ys i)
• Matroid.closure_mono 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) : Monotone M.closure
• Matroid.restrict_closure_eq 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {X R : Set α} (M : Matroid α) (hXR : X ⊆ R) (hR : R ⊆ M.E := by aesop_mat) : (M.restrict R).closure X = M.closure X ∩ R
• Matroid.Indep.closure_iInter_eq_biInter_closure_of_forall_subset 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {ι : Sort u_3} {I : Set α} [Nonempty ι] {Js : ι → Set α} (hI : M.Indep I) (hJs : ∀ (i : ι), Js i ⊆ I) : M.closure (⋂ i, Js i) = ⋂ i, M.closure (Js i)
• Matroid.restrict_closure_eq' 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) (X R : Set α) : (M.restrict R).closure X = M.closure (X ∩ R) ∩ R ∪ R \ M.E
• Matroid.IsBasis.isBasis_of_closure_eq_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X Y I : Set α} (hI : M.IsBasis I X) (hY : I ⊆ Y) (h : M.closure X = M.closure Y) (hYE : Y ⊆ M.E := by aesop_mat) : M.IsBasis I Y
• Matroid.subset_closure_iff_forall_subset_isFlat 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {Y : Set α} (X : Set α) (hX : X ⊆ M.E := by aesop_mat) : Y ⊆ M.closure X ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F
• Matroid.mem_closure_iff_forall_mem_isFlat 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {e : α} (X : Set α) (hX : X ⊆ M.E := by aesop_mat) : e ∈ M.closure X ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → e ∈ F
• Matroid.Indep.insert_indep_iff 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) : M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
• Matroid.Indep.insert_indep_iff_of_notMem 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) (heI : e ∉ I) : M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I
• Matroid.insert_indep_iff 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} : M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)
• Matroid.closure_biUnion_closure_eq_closure_sUnion 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) (Xs : Set (Set α)) : M.closure (⋃ X ∈ Xs, M.closure X) = M.closure (⋃₀ Xs)
• Matroid.closure_diff_singleton_eq_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X : Set α} {e : α} (h : e ∈ M.closure (X \ {e})) : M.closure (X \ {e}) = M.closure X
• Matroid.closure_sdiff_singleton_eq_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X : Set α} {e : α} (h : e ∈ M.closure (X \ {e})) : M.closure (X \ {e}) = M.closure X
• Matroid.not_spanning_iff_closure_ssubset 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {S : Set α} (hS : S ⊆ M.E := by aesop_mat) : ¬M.Spanning S ↔ M.closure S ⊂ M.E
• Matroid.Indep.mem_closure_iff' 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {I : Set α} {x : α} (hI : M.Indep I) : x ∈ M.closure I ↔ x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)
• Matroid.indep_iff_forall_notMem_closure_diff' 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {I : Set α} : M.Indep I ↔ I ⊆ M.E ∧ ∀ e ∈ I, e ∉ M.closure (I \ {e})
• Matroid.indep_iff_forall_notMem_closure_sdiff' 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {I : Set α} : M.Indep I ↔ I ⊆ M.E ∧ ∀ e ∈ I, e ∉ M.closure (I \ {e})
• Matroid.indep_iff_forall_notMem_closure_diff 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {I : Set α} (hI : I ⊆ M.E := by aesop_mat) : M.Indep I ↔ ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
• Matroid.indep_iff_forall_notMem_closure_sdiff 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {I : Set α} (hI : I ⊆ M.E := by aesop_mat) : M.Indep I ↔ ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
• Matroid.mem_closure_insert 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X : Set α} {e f : α} (he : e ∉ M.closure X) (hef : e ∈ M.closure (insert f X)) : f ∈ M.closure (insert e X)
• Matroid.Indep.notMem_closure_iff_of_notMem 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) (heI : e ∉ I) (he : e ∈ M.E := by aesop_mat) : e ∉ M.closure I ↔ M.Indep (insert e I)
• Matroid.Indep.notMem_closure_iff 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) (he : e ∈ M.E := by aesop_mat) : e ∉ M.closure I ↔ M.Indep (insert e I) ∧ e ∉ I
• Matroid.IsBasis.insert_isBasis_insert_of_notMem_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X : Set α} {e : α} {I : Set α} (hIX : M.IsBasis I X) (heI : e ∉ M.closure I) (heE : e ∈ M.E := by aesop_mat) : M.IsBasis (insert e I) (insert e X)
• Matroid.Indep.closure_diff_ssubset 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X I : Set α} (hI : M.Indep I) (hX : (I ∩ X).Nonempty) : M.closure (I \ X) ⊂ M.closure I
• Matroid.Indep.closure_sdiff_ssubset 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X I : Set α} (hI : M.Indep I) (hX : (I ∩ X).Nonempty) : M.closure (I \ X) ⊂ M.closure I
• Matroid.closure_insert_congr 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X : Set α} {e f : α} (he : e ∈ M.closure (insert f X) \ M.closure X) : M.closure (insert e X) = M.closure (insert f X)
• Matroid.closure_sInter_eq_biInter_closure_of_sUnion_indep 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} (Is : Set (Set α)) (hIs : Is.Nonempty) (h : M.Indep (⋃₀ Is)) : M.closure (⋂₀ Is) = ⋂ I ∈ Is, M.closure I
• Matroid.subset_closure_diff_iff_closure_eq 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X Y : Set α} (h : Y ⊆ X) (hY : Y ⊆ M.E := by aesop_mat) : Y ⊆ M.closure (X \ Y) ↔ M.closure (X \ Y) = M.closure X
• Matroid.subset_closure_sdiff_iff_closure_eq 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X Y : Set α} (h : Y ⊆ X) (hY : Y ⊆ M.E := by aesop_mat) : Y ⊆ M.closure (X \ Y) ↔ M.closure (X \ Y) = M.closure X
• Matroid.closure_exchange 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X : Set α} {e f : α} (he : e ∈ M.closure (insert f X) \ M.closure X) : f ∈ M.closure (insert e X) \ M.closure X
• Matroid.Indep.closure_diff_singleton_ssubset 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) (he : e ∈ I) : M.closure (I \ {e}) ⊂ M.closure I
• Matroid.Indep.closure_sdiff_singleton_ssubset 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) (he : e ∈ I) : M.closure (I \ {e}) ⊂ M.closure I
• Matroid.closure_exchange_iff 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X : Set α} {e f : α} : e ∈ M.closure (insert f X) \ M.closure X ↔ f ∈ M.closure (insert e X) \ M.closure X
• Matroid.exists_of_closure_ssubset 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X Y : Set α} (hXY : M.closure X ⊂ M.closure Y) : ∃ e ∈ Y, e ∉ M.closure X
• Matroid.Indep.closure_ssubset_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {I J : Set α} (hI : M.Indep I) (hJI : J ⊂ I) : M.closure J ⊂ M.closure I
• Matroid.closure_biUnion_closure_eq_closure_biUnion 📋 Mathlib.Combinatorics.Matroid.Closure
  {ι : Type u_1} {α : Type u_2} (M : Matroid α) (Xs : ι → Set α) (A : Set ι) : M.closure (⋃ i ∈ A, M.closure (Xs i)) = M.closure (⋃ i ∈ A, Xs i)
• Matroid.Indep.union_indep_iff_forall_notMem_closure_left 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {I J : Set α} (hI : M.Indep I) (hJ : M.Indep J) : M.Indep (I ∪ J) ↔ ∀ e ∈ I \ J, e ∉ M.closure (I \ {e} ∪ J)
• Matroid.Indep.union_indep_iff_forall_notMem_closure_right 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {I J : Set α} (hI : M.Indep I) (hJ : M.Indep J) : M.Indep (I ∪ J) ↔ ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
• Matroid.mem_closure_diff_singleton_iff_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X : Set α} {e : α} (he : e ∈ X) (heE : e ∈ M.E := by aesop_mat) : e ∈ M.closure (X \ {e}) ↔ M.closure (X \ {e}) = M.closure X
• Matroid.mem_closure_sdiff_singleton_iff_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X : Set α} {e : α} (he : e ∈ X) (heE : e ∈ M.E := by aesop_mat) : e ∈ M.closure (X \ {e}) ↔ M.closure (X \ {e}) = M.closure X
• Matroid.IsBase.exchange_base_of_notMem_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {e f : α} {B : Set α} (hB : M.IsBase B) (he : e ∈ B) (hf : f ∉ M.closure (B \ {e})) (hfE : f ∈ M.E := by aesop_mat) : M.IsBase (insert f (B \ {e}))
• Matroid.indep_iff_forall_closure_ssubset_of_ssubset 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {I : Set α} (hI : I ⊆ M.E := by aesop_mat) : M.Indep I ↔ ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
• Matroid.Indep.closure_sInter_eq_biInter_closure_of_forall_subset 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {I : Set α} {Js : Set (Set α)} (hI : M.Indep I) (hne : Js.Nonempty) (hIs : ∀ J ∈ Js, J ⊆ I) : M.closure (⋂₀ Js) = ⋂ J ∈ Js, M.closure J
• Matroid.IsBase.isBase_insert_diff_of_mem_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {e f : α} {B : Set α} (hB : M.IsBase B) (he : e ∈ M.closure (insert f B \ {e})) (heB : e ∈ insert f B) : M.IsBase (insert f B \ {e})
• Matroid.IsBase.isBase_insert_sdiff_of_mem_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {e f : α} {B : Set α} (hB : M.IsBase B) (he : e ∈ M.closure (insert f B \ {e})) (heB : e ∈ insert f B) : M.IsBase (insert f B \ {e})
• Matroid.Indep.closure_insert_diff_eq_of_mem_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {e f : α} {I : Set α} (hI : M.Indep I) (hf : f ∈ M.closure I) (he : e ∈ M.closure (insert f I \ {e})) : M.closure (insert f I \ {e}) = M.closure I
• Matroid.Indep.closure_insert_sdiff_eq_of_mem_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {e f : α} {I : Set α} (hI : M.Indep I) (hf : f ∈ M.closure I) (he : e ∈ M.closure (insert f I \ {e})) : M.closure (insert f I \ {e}) = M.closure I
• Matroid.Indep.indep_insert_diff_of_mem_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {e f : α} {I : Set α} (hI : M.Indep I) (hfI : f ∈ M.closure I) (he : e ∈ M.closure (insert f I \ {e})) (heI : e ∈ insert f I) : M.Indep (insert f I \ {e})
• Matroid.Indep.indep_insert_sdiff_of_mem_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {e f : α} {I : Set α} (hI : M.Indep I) (hfI : f ∈ M.closure I) (he : e ∈ M.closure (insert f I \ {e})) (heI : e ∈ insert f I) : M.Indep (insert f I \ {e})
• Matroid.closure_biUnion_congr 📋 Mathlib.Combinatorics.Matroid.Closure
  {ι : Type u_1} {α : Type u_2} (M : Matroid α) (Xs Ys : ι → Set α) (A : Set ι) (h : ∀ i ∈ A, M.closure (Xs i) = M.closure (Ys i)) : M.closure (⋃ i ∈ A, Xs i) = M.closure (⋃ i ∈ A, Ys i)
• Matroid.IsBasis.isBasis_insert_diff_of_mem_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X : Set α} {e f : α} {B : Set α} (hB : M.IsBasis B X) (he : e ∈ M.closure (insert f B \ {e})) (heB : e ∈ insert f B) (hfX : f ∈ X) : M.IsBasis (insert f B \ {e}) X
• Matroid.IsBasis.isBasis_insert_sdiff_of_mem_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {X : Set α} {e f : α} {B : Set α} (hB : M.IsBasis B X) (he : e ∈ M.closure (insert f B \ {e})) (heB : e ∈ insert f B) (hfX : f ∈ X) : M.IsBasis (insert f B \ {e}) X
• Matroid.Indep.insert_diff_indep_iff 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {e f : α} {I : Set α} (hI : M.Indep (I \ {e})) (heI : e ∈ I) : M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
• Matroid.Indep.insert_sdiff_indep_iff 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {e f : α} {I : Set α} (hI : M.Indep (I \ {e})) (heI : e ∈ I) : M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
• Matroid.closure_biInter_eq_biInter_closure_of_biUnion_indep 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} {M : Matroid α} {ι : Type u_4} {A : Set ι} (hA : A.Nonempty) {I : ι → Set α} (h : M.Indep (⋃ i ∈ A, I i)) : M.closure (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.closure (I i)
• Matroid.closure_eq_subtypeClosure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) (X : Set α) : M.closure X = ↑(M.subtypeClosure ⟨X ∩ M.E, ⋯⟩)
• Matroid.IsRkFinite.closure 📋 Mathlib.Combinatorics.Matroid.Rank.Finite
  {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.IsRkFinite X) : M.IsRkFinite (M.closure X)
• Matroid.isRkFinite_closure_iff 📋 Mathlib.Combinatorics.Matroid.Rank.Finite
  {α : Type u_1} {M : Matroid α} {X : Set α} : M.IsRkFinite (M.closure X) ↔ M.IsRkFinite X
• Matroid.IsCircuit.subset_closure_diff_singleton 📋 Mathlib.Combinatorics.Matroid.Circuit
  {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) (e : α) : C ⊆ M.closure (C \ {e})
• Matroid.IsCircuit.subset_closure_sdiff_singleton 📋 Mathlib.Combinatorics.Matroid.Circuit
  {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) (e : α) : C ⊆ M.closure (C \ {e})
• Matroid.IsCircuit.closure_diff_singleton_eq 📋 Mathlib.Combinatorics.Matroid.Circuit
  {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) (e : α) : M.closure (C \ {e}) = M.closure C
• Matroid.IsCircuit.closure_sdiff_singleton_eq 📋 Mathlib.Combinatorics.Matroid.Circuit
  {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) (e : α) : M.closure (C \ {e}) = M.closure C
• Matroid.Indep.fundCircuit_isCircuit 📋 Mathlib.Combinatorics.Matroid.Circuit
  {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} (hI : M.Indep I) (hecl : e ∈ M.closure I) (heI : e ∉ I) : M.IsCircuit (M.fundCircuit e I)
• Matroid.IsCircuit.mem_closure_diff_singleton_of_mem 📋 Mathlib.Combinatorics.Matroid.Circuit
  {α : Type u_1} {M : Matroid α} {C : Set α} {e : α} (hC : M.IsCircuit C) (heC : e ∈ C) : e ∈ M.closure (C \ {e})
• Matroid.IsCircuit.mem_closure_sdiff_singleton_of_mem 📋 Mathlib.Combinatorics.Matroid.Circuit
  {α : Type u_1} {M : Matroid α} {C : Set α} {e : α} (hC : M.IsCircuit C) (heC : e ∈ C) : e ∈ M.closure (C \ {e})
• Matroid.IsBase.compl_closure_diff_singleton_isCocircuit 📋 Mathlib.Combinatorics.Matroid.Circuit
  {α : Type u_1} {M : Matroid α} {e : α} {B : Set α} (hB : M.IsBase B) (he : e ∈ B) : M.IsCocircuit (M.E \ M.closure (B \ {e}))
• Matroid.IsBase.compl_closure_sdiff_singleton_isCocircuit 📋 Mathlib.Combinatorics.Matroid.Circuit
  {α : Type u_1} {M : Matroid α} {e : α} {B : Set α} (hB : M.IsBase B) (he : e ∈ B) : M.IsCocircuit (M.E \ M.closure (B \ {e}))
• Matroid.exists_mem_finite_closure_of_mem_closure 📋 Mathlib.Combinatorics.Matroid.Circuit
  {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} [M.Finitary] (he : e ∈ M.closure X) : ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I
• Matroid.exists_subset_finite_closure_of_subset_closure 📋 Mathlib.Combinatorics.Matroid.Circuit
  {α : Type u_1} {M : Matroid α} {X Y : Set α} [M.Finitary] (hX : X.Finite) (hXY : X ⊆ M.closure Y) : ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I
• Matroid.fundCircuit_eq_sInter 📋 Mathlib.Combinatorics.Matroid.Circuit
  {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} (he : e ∈ M.closure I) : M.fundCircuit e I = insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J})
• Matroid.exists_isCircuit_of_mem_closure 📋 Mathlib.Combinatorics.Matroid.Circuit
  {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (he : e ∈ M.closure X) (heX : e ∉ X) : ∃ C ⊆ insert e X, M.IsCircuit C ∧ e ∈ C
• Matroid.mem_closure_iff_exists_isCircuit 📋 Mathlib.Combinatorics.Matroid.Circuit
  {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (he : e ∉ X) : e ∈ M.closure X ↔ ∃ C ⊆ insert e X, M.IsCircuit C ∧ e ∈ C
• Matroid.Indep.mem_fundCircuit_iff 📋 Mathlib.Combinatorics.Matroid.Circuit
  {α : Type u_1} {M : Matroid α} {I : Set α} {e x : α} (hI : M.Indep I) (hecl : e ∈ M.closure I) (heI : e ∉ I) : x ∈ M.fundCircuit e I ↔ M.Indep (insert e I \ {x})
• Matroid.Indep.insert_isCircuit_of_forall_of_nontrivial 📋 Mathlib.Combinatorics.Matroid.Circuit
  {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} (hI : M.Indep I) (hInt : I.Nontrivial) (he : e ∈ M.closure I) (h : ∀ f ∈ I, e ∉ M.closure (I \ {f})) : M.IsCircuit (insert e I)
• Matroid.Indep.insert_isCircuit_of_forall 📋 Mathlib.Combinatorics.Matroid.Circuit
  {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} (hI : M.Indep I) (heI : e ∉ I) (he : e ∈ M.closure I) (h : ∀ f ∈ I, e ∉ M.closure (I \ {f})) : M.IsCircuit (insert e I)
• Matroid.closure_loops 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} (M : Matroid α) : M.closure M.loops = M.loops
• Matroid.closure_empty 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} (M : Matroid α) : M.closure ∅ = M.loops
• Matroid.IsLoop.mem_closure 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsLoop e) (X : Set α) : e ∈ M.closure X
• Matroid.closure_diff_loops_eq 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} (M : Matroid α) (X : Set α) : M.closure (X \ M.loops) = M.closure X
• Matroid.closure_eq_loops_of_subset 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} {M : Matroid α} {X : Set α} (h : X ⊆ M.loops) : M.closure X = M.loops
• Matroid.closure_loops_union_eq 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} (M : Matroid α) (X : Set α) : M.closure (M.loops ∪ X) = M.closure X
• Matroid.closure_sdiff_loops_eq 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} (M : Matroid α) (X : Set α) : M.closure (X \ M.loops) = M.closure X
• Matroid.closure_union_loops_eq 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} (M : Matroid α) (X : Set α) : M.closure (X ∪ M.loops) = M.closure X
• Matroid.IsLoop.closure 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsLoop e) : M.closure {e} = M.loops
• Matroid.not_isNonloop_iff_closure 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} {M : Matroid α} {e : α} : ¬M.IsNonloop e ↔ M.closure {e} = M.loops
• Matroid.closure_inter_setOfPred_isNonloop_eq 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} (M : Matroid α) (X : Set α) : M.closure (X ∩ {e | M.IsNonloop e}) = M.closure X
• Matroid.closure_inter_setOf_isNonloop_eq 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} (M : Matroid α) (X : Set α) : M.closure (X ∩ {e | M.IsNonloop e}) = M.closure X
• Matroid.closure_inter_coloops_eq 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} (M : Matroid α) (X : Set α) : M.closure X ∩ M.coloops = X ∩ M.coloops
• Matroid.IsColoop.mem_of_mem_closure 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (he : M.IsColoop e) (heX : e ∈ M.closure X) : e ∈ X
• Matroid.closure_eq_of_subset_coloops 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} {M : Matroid α} {K : Set α} (hK : K ⊆ M.coloops) : M.closure K = K ∪ M.loops
• Matroid.IsColoop.mem_closure_iff_mem 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (he : M.IsColoop e) : e ∈ M.closure X ↔ e ∈ X
• Matroid.IsNonloop.isNonloop_of_mem_closure 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} {M : Matroid α} {e f : α} (he : M.IsNonloop e) (hef : e ∈ M.closure {f}) : M.IsNonloop f
• Matroid.isColoop_iff_forall_mem_closure_iff_mem 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} {M : Matroid α} {e : α} : M.IsColoop e ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
• Matroid.IsColoop.notMem_closure_of_notMem 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (he : M.IsColoop e) (hX : e ∉ X) : e ∉ M.closure X
• Matroid.closure_union_coloops_eq 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} (M : Matroid α) (X : Set α) : M.closure (X ∪ M.coloops) = M.closure X ∪ M.coloops
• Matroid.isColoop_iff_diff_closure 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} {M : Matroid α} {e : α} : M.IsColoop e ↔ M.closure (M.E \ {e}) ≠ M.E
• Matroid.isColoop_iff_sdiff_closure 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} {M : Matroid α} {e : α} : M.IsColoop e ↔ M.closure (M.E \ {e}) ≠ M.E
• Matroid.isNonloop_of_notMem_closure 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (h : e ∉ M.closure X) (he : e ∈ M.E := by aesop_mat) : M.IsNonloop e
• Matroid.closure_insert_isColoop_eq 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} {M : Matroid α} {e : α} (X : Set α) (he : M.IsColoop e) : M.closure (insert e X) = insert e (M.closure X)
• Matroid.closure_inter_eq_of_subset_coloops 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} {M : Matroid α} {K : Set α} (X : Set α) (hK : K ⊆ M.coloops) : M.closure X ∩ K = X ∩ K
• Matroid.isLoop_iff_closure_eq_loops_and_mem_ground 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} {M : Matroid α} {e : α} : M.IsLoop e ↔ M.closure {e} = M.loops ∧ e ∈ M.E
• Matroid.isLoop_iff_closure_eq_loops 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) : M.IsLoop e ↔ M.closure {e} = M.loops
• Matroid.closure_diff_eq_of_subset_coloops 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} {M : Matroid α} {K : Set α} (X : Set α) (hK : K ⊆ M.coloops) : M.closure (X \ K) = M.closure X \ K
• Matroid.closure_sdiff_eq_of_subset_coloops 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} {M : Matroid α} {K : Set α} (X : Set α) (hK : K ⊆ M.coloops) : M.closure (X \ K) = M.closure X \ K
• Matroid.closure_union_eq_of_subset_coloops 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} {M : Matroid α} {K : Set α} (X : Set α) (hK : K ⊆ M.coloops) : M.closure (X ∪ K) = M.closure X ∪ K

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c