Loop

📁 Source: Mathlib/Combinatorics/Matroid/Loop.lean

Statistics

Metric	Count
Definitions `IsColoop`, `IsLoop`, `IsNonloop`, `Loopless`, `coloops`, `loops`, `removeLoops`	7
Theorems `disjoint_loops`, `eq_empty_of_subset_loops`, `isNonloop`, `isNonloop_of_mem`, `coloops_subset`, `isColoop_iff_forall_notMem_fundCircuit`, `mem_of_isColoop`, `inter_coloops_subset`, `inter_coloops_subset`, `disjoint_coloops`, `isNonloop_of_mem`, `isNonloop_of_mem_of_one_lt_card`, `not_isColoop_of_mem`, `isNonloop_of_mem`, `diff_not_spanning`, `dual_isLoop`, `insert_indep_of_indep`, `isCocircuit`, `isNonloop`, `mem_closure_iff_mem`, `mem_ground`, `mem_of_isBase`, `mem_of_mem_closure`, `notMem_closure_of_notMem`, `notMem_isCircuit`, `loops_subset`, `closure`, `dep`, `dep_of_mem`, `dual_isColoop`, `eq_of_isCircuit_mem`, `isCircuit`, `isLoop_isRestriction`, `mem_closure`, `mem_ground`, `mem_of_isFlat`, `notMem_of_indep`, `not_indep_of_mem`, `not_isColoop`, `not_isNonloop`, `of_isRestriction`, `closure_eq_closure_iff_eq_or_dep`, `closure_eq_closure_iff_isCircuit_of_ne`, `closure_eq_of_mem_closure`, `exists_mem_isBase`, `exists_mem_isCocircuit`, `indep`, `isNonloop_of_mem_closure`, `mem_closure_comm`, `mem_closure_singleton`, `mem_ground`, `not_isLoop`, `of_isRestriction`, `of_restrict`, `rankPos`, `removeLoops_isNonloop`, `isLoop_iff`, `isRestriction_removeLoops`, `loopless`, `ground_eq`, `loops_eq_empty`, `closure_diff_eq_of_subset_coloops`, `closure_diff_loops_eq`, `closure_disjoint_coloops_of_disjoint_coloops`, `closure_disjoint_of_disjoint_of_subset_coloops`, `closure_empty`, `closure_eq_loops_of_subset`, `closure_eq_of_subset_coloops`, `closure_insert_isColoop_eq`, `closure_inter_coloops_eq`, `closure_inter_eq_of_subset_coloops`, `closure_inter_setOf_isNonloop_eq`, `closure_loops`, `closure_loops_union_eq`, `closure_union_coloops_eq`, `closure_union_eq_of_subset_coloops`, `closure_union_loops_eq`, `coloops_indep`, `coloops_subset_ground`, `comap_isLoop_iff`, `comap_isNonloop_iff`, `comap_loops`, `compl_loops_eq`, `diff_coloops_indep_iff`, `diff_indep_iff_indep_of_subset_coloops`, `dual_coloops`, `dual_isColoop_iff_isLoop`, `dual_isLoop_iff_isColoop`, `dual_loops`, `eq_loopyOn_iff_loops`, `eq_loopyOn_iff_loops_eq`, `eq_restrict_removeLoops`, `exists_isNonloop`, `exists_mem_isCircuit_of_not_isColoop`, `ext_indep_disjoint_loops_coloops`, `freeOn_isNonloop_iff`, `freeOn_not_isLoop`, `indep_singleton`, `instRankPosOfNonemptyOfLoopless`, `isBasis_iff_empty_of_subset_loops`, `isBasis_loops_iff`, `isColoop_iff_diff_closure`, `isColoop_iff_diff_not_spanning`, `isColoop_iff_forall_mem_closure_iff_mem`, `isColoop_iff_forall_mem_closure_iff_mem'`, `isColoop_iff_forall_mem_compl_isCircuit`, `isColoop_iff_forall_mem_isBase`, `isColoop_iff_forall_notMem_isCircuit`, `isColoop_iff_mem_coloops`, `isColoop_iff_notMem_closure_compl`, `isColoop_tfae`, `isLoop_iff`, `isLoop_iff_closure_eq_loops`, `isLoop_iff_closure_eq_loops_and_mem_ground`, `isLoop_iff_forall_mem_compl_isBase`, `isLoop_iff_forall_notMem_isBase`, `isLoop_of_not_isNonloop`, `isLoop_or_isNonloop`, `isLoop_tfae`, `isNonloop_iff`, `isNonloop_iff_mem_compl_loops`, `isNonloop_iff_notMem_loops`, `isNonloop_iff_restrict_of_mem`, `isNonloop_of_loopless`, `isNonloop_of_notMem_closure`, `isNonloop_of_not_isLoop`, `loopless_iff`, `loopless_iff_forall_isCircuit`, `loopless_iff_forall_isNonloop`, `loopless_iff_forall_not_isLoop`, `loops_eq_empty`, `loops_subset_ground`, `loopyOn_isLoop_iff`, `loopyOn_isLoopless_iff`, `mapEmbedding_isLoop_iff`, `map_isLoop_iff`, `map_loops`, `not_isLoop`, `not_isLoop_iff`, `not_isNonloop_iff`, `not_isNonloop_iff_closure`, `removeLoops_eq_restrict`, `removeLoops_eq_self`, `removeLoops_eq_self_iff`, `removeLoops_ground_eq`, `removeLoops_idem`, `removeLoops_indep_eq`, `removeLoops_isBase_eq`, `removeLoops_isBasis'_eq`, `removeLoops_isNonloop_eq`, `removeLoops_isRestriction`, `removeLoops_loopless`, `removeLoops_mono_isRestriction`, `removeLoops_restrict_eq_restrict`, `restrict_isColoop_iff`, `restrict_isLoop_iff`, `restrict_isNonloop_iff`, `restrict_loops_eq`, `restrict_loops_eq'`, `restrict_subset_loops_eq`, `restrict_univ_removeLoops_eq`, `setOf_isNonloop_eq`, `singleton_dep`, `singleton_isCircuit`, `singleton_isCocircuit`, `singleton_not_indep`, `subsingleton_indep`, `union_coloops_indep_iff`, `union_indep_iff_indep_of_subset_coloops`, `uniqueBaseOn_isLoop_iff`, `uniqueBaseOn_isNonloop_iff`	171
Total	178

Matroid

Definitions

Name	Category	Theorems
`IsColoop` 📖	MathDef	20 math math: `isColoop_iff_forall_mem_compl_isCircuit`, `isColoop_iff_forall_mem_closure_iff_mem`, `isColoop_iff_diff_not_spanning`, `isColoop_iff_forall_mem_closure_iff_mem'`, `IsCircuit.not_isColoop_of_mem`, `IsLoop.dual_isColoop`, `dual_isLoop_iff_isColoop`, `restrict_isColoop_iff`, `isColoop_iff_diff_closure`, `isColoop_iff_forall_mem_isBase`, `contract_isColoop_iff`, `dual_isColoop_iff_isLoop`, `delete_isColoop_iff`, `isColoop_tfae`, `IsLoop.not_isColoop`, `isColoop_iff_notMem_closure_compl`, `singleton_isCocircuit`, `IsBase.isColoop_iff_forall_notMem_fundCircuit`, `isColoop_iff_mem_coloops`, `isColoop_iff_forall_notMem_isCircuit`
`IsLoop` 📖	MathDef	30 math math: `uniqueBaseOn_isLoop_iff`, `freeOn_not_isLoop`, `map_isLoop_iff`, `isLoop_tfae`, `loopless_iff_forall_not_isLoop`, `loopyOn_isLoop_iff`, `isLoop_iff_forall_notMem_isBase`, `dual_isLoop_iff_isColoop`, `isLoop_of_not_isNonloop`, `IsColoop.dual_isLoop`, `not_isLoop`, `isLoop_iff_closure_eq_loops`, `singleton_isCircuit`, `delete_isLoop_iff`, `singleton_not_indep`, `IsNonloop.not_isLoop`, `comap_isLoop_iff`, `dual_isColoop_iff_isLoop`, `isLoop_iff_forall_mem_compl_isBase`, `not_isNonloop_iff`, `isLoop_iff`, `singleton_dep`, `isNonloop_iff`, `not_isLoop_iff`, `IsRestriction.isLoop_iff`, `isLoop_iff_closure_eq_loops_and_mem_ground`, `restrict_isLoop_iff`, `isLoop_or_isNonloop`, `contract_isLoop_iff_mem_closure`, `mapEmbedding_isLoop_iff`
`IsNonloop` 📖	CompData	37 math math: `isNonloop_iff_delete_of_notMem`, `isNonloop_of_notMem_closure`, `loopless_iff_forall_isNonloop`, `isNonloop_iff_restrict_of_mem`, `contract_isNonloop_iff`, `IsColoop.isNonloop`, `removeLoops_ground_eq`, `closure_inter_setOf_isNonloop_eq`, `delete_isNonloop_iff`, `freeOn_isNonloop_iff`, `setOf_isNonloop_eq`, `IsLoop.not_isNonloop`, `comap_isNonloop_iff`, `removeLoops_eq_restrict`, `restrict_isNonloop_iff`, `isNonloop_of_loopless`, `IsCocircuit.isNonloop_of_mem`, `isNonloop_iff_notMem_loops`, `eRk_eq_one_iff`, `exists_isNonloop`, `indep_singleton`, `isNonloop_iff_mem_compl_loops`, `not_isNonloop_iff`, `uniqueBaseOn_isNonloop_iff`, `Indep.isNonloop`, `Indep.isNonloop_of_mem`, `isNonloop_iff`, `eRk_singleton_eq_one_iff`, `removeLoops_isNonloop_eq`, `not_isLoop_iff`, `isNonloop_of_not_isLoop`, `IsCircuit.isNonloop_of_mem`, `Loopless.ground_eq`, `compl_loops_eq`, `not_isNonloop_iff_closure`, `IsCircuit.isNonloop_of_mem_of_one_lt_card`, `isLoop_or_isNonloop`
`Loopless` 📖	CompData	8 math math: `loopless_iff_forall_isNonloop`, `loopless_iff_forall_not_isLoop`, `loopyOn_isLoopless_iff`, `IsRestriction.loopless`, `loopless_iff`, `loopless_iff_forall_isCircuit`, `removeLoops_loopless`, `removeLoops_eq_self_iff`
`coloops` 📖	CompOp	15 math math: `IsBase.coloops_subset`, `IsBasis'.inter_coloops_subset`, `dual_loops`, `closure_union_coloops_eq`, `IsBasis.inter_coloops_subset`, `coloops_subset_ground`, `IsCircuit.disjoint_coloops`, `coloops_indep`, `contract_coloops_eq`, `dual_coloops`, `isColoop_tfae`, `diff_coloops_indep_iff`, `closure_inter_coloops_eq`, `isColoop_iff_mem_coloops`, `union_coloops_indep_iff`
`loops` 📖	CompOp	37 math math: `eRk_loops`, `loops_eq_empty`, `restrict_loops_eq`, `restrict_loops_eq'`, `closure_empty`, `closure_loops`, `dual_loops`, `closure_loops_union_eq`, `IsFlat.loops_subset`, `setOf_isNonloop_eq`, `isLoop_iff_closure_eq_loops`, `Loopless.loops_eq_empty`, `IsLoop.closure`, `contract_loops_eq`, `isNonloop_iff_notMem_loops`, `closure_union_loops_eq`, `delete_loops_eq_removeLoops`, `delete_loops_eq`, `closure_diff_loops_eq`, `eRk_eq_zero_iff'`, `isNonloop_iff_mem_compl_loops`, `eRk_eq_zero_iff`, `isBasis_loops_iff`, `dual_coloops`, `map_loops`, `isLoop_iff`, `loopless_iff`, `IsBasis.diff_subset_loops_contract`, `loops_subset_ground`, `eq_loopyOn_iff_loops_eq`, `Indep.disjoint_loops`, `isLoop_iff_closure_eq_loops_and_mem_ground`, `eq_loopyOn_iff_loops`, `compl_loops_eq`, `not_isNonloop_iff_closure`, `comap_loops`, `closure_eq_of_subset_coloops`
`removeLoops` 📖	CompOp	18 math math: `removeLoops_mono_isRestriction`, `removeLoops_isBasis'_eq`, `removeLoops_indep_eq`, `removeLoops_restrict_eq_restrict`, `removeLoops_ground_eq`, `IsNonloop.removeLoops_isNonloop`, `removeLoops_eq_self`, `removeLoops_isRestriction`, `removeLoops_eq_restrict`, `delete_loops_eq_removeLoops`, `eq_restrict_removeLoops`, `removeLoops_isNonloop_eq`, `removeLoops_loopless`, `restrict_univ_removeLoops_eq`, `removeLoops_eq_self_iff`, `removeLoops_idem`, `IsRestriction.isRestriction_removeLoops`, `removeLoops_isBase_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_diff_eq_of_subset_coloops` 📖	mathematical	`Set` `Set.instHasSubset` `coloops`	`closure` `Set.instSDiff`	—	`Set.inter_union_diff` `Set.union_comm` `closure_union_eq_of_subset_coloops` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.inter_subset_right` `Set.union_diff_distrib` `Set.diff_eq_empty` `Set.union_empty` `sdiff_eq_self_iff_disjoint` `Set.disjoint_iff_forall_ne` `IsColoop.mem_closure_iff_mem`
`closure_diff_loops_eq` 📖	mathematical	—	`closure` `Set` `Set.instSDiff` `loops`	—	`closure_union_loops_eq` `Set.diff_union_self` `closure_empty` `closure_union_closure_right_eq` `Set.union_empty`
`closure_disjoint_coloops_of_disjoint_coloops` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `coloops`	`closure`	—	`closure_disjoint_of_disjoint_of_subset_coloops` `Set.Subset.rfl`
`closure_disjoint_of_disjoint_of_subset_coloops` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.instHasSubset` `coloops`	`closure`	—	`Set.disjoint_iff_inter_eq_empty` `closure_inter_eq_of_subset_coloops`
`closure_empty` 📖	mathematical	—	`closure` `Set` `Set.instEmptyCollection` `loops`	—	—
`closure_eq_loops_of_subset` 📖	mathematical	`Set` `Set.instHasSubset` `loops`	`closure`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `closure_subset_closure_of_subset_closure` `closure_mono` `Set.empty_subset`
`closure_eq_of_subset_coloops` 📖	mathematical	`Set` `Set.instHasSubset` `coloops`	`closure` `Set.instUnion` `loops`	—	`Set.empty_union` `closure_union_eq_of_subset_coloops` `Set.union_comm` `closure_empty`
`closure_insert_isColoop_eq` 📖	mathematical	`IsColoop`	`closure` `Set` `Set.instInsert`	—	`Set.union_singleton` `closure_union_eq_of_subset_coloops`
`closure_inter_coloops_eq` 📖	mathematical	—	`Set` `Set.instInter` `closure` `coloops`	—	`IsColoop.mem_closure_iff_mem`
`closure_inter_eq_of_subset_coloops` 📖	mathematical	`Set` `Set.instHasSubset` `coloops`	`Set.instInter` `closure`	—	`Set.inter_eq_self_of_subset_right` `Set.inter_assoc` `closure_inter_coloops_eq`
`closure_inter_setOf_isNonloop_eq` 📖	mathematical	—	`closure` `Set` `Set.instInter` `setOf` `IsNonloop`	—	`setOf_isNonloop_eq` `Set.inter_diff_assoc` `closure_diff_loops_eq` `closure_inter_ground`
`closure_loops` 📖	mathematical	—	`closure` `loops`	—	`closure_closure`
`closure_loops_union_eq` 📖	mathematical	—	`closure` `Set` `Set.instUnion` `loops`	—	`Set.union_comm` `closure_union_loops_eq`
`closure_union_coloops_eq` 📖	mathematical	—	`closure` `Set` `Set.instUnion` `coloops`	—	`closure_union_eq_of_subset_coloops` `Set.Subset.rfl`
`closure_union_eq_of_subset_coloops` 📖	mathematical	`Set` `Set.instHasSubset` `coloops`	`closure` `Set.instUnion`	—	`closure_union_closure_left_eq` `subset_antisymm_iff` `Set.instReflSubset` `Set.instAntisymmSubset` `subset_closure` `closure_subset_ground` `coloops_subset_ground` `Set.diff_eq_empty` `Set.eq_empty_iff_forall_notMem` `mem_closure_iff_exists_isCircuit` `closure_subset_closure_of_subset_closure` `Set.singleton_union` `Disjoint.sdiff_eq_left` `Disjoint.mono_right` `IsCircuit.disjoint_coloops` `Set.diff_subset_iff` `Set.union_comm` `Set.union_assoc` `IsCircuit.mem_closure_diff_singleton_of_mem`
`closure_union_loops_eq` 📖	mathematical	—	`closure` `Set` `Set.instUnion` `loops`	—	`closure_empty` `closure_union_closure_right_eq` `Set.union_empty`
`coloops_indep` 📖	mathematical	—	`Indep` `coloops`	—	`Set.empty_union` `union_coloops_indep_iff` `empty_indep`
`coloops_subset_ground` 📖	mathematical	—	`Set` `Set.instHasSubset` `coloops` `E`	—	`IsColoop.mem_ground`
`comap_isLoop_iff` 📖	mathematical	—	`IsLoop` `comap`	—	`comap_loops`
`comap_isNonloop_iff` 📖	mathematical	—	`IsNonloop` `comap`	—	`indep_singleton` `comap_indep_iff` `Set.image_singleton` `Set.injOn_singleton`
`comap_loops` 📖	mathematical	—	`loops` `comap` `Set.preimage`	—	`loops.eq_1` `comap_closure_eq` `Set.image_empty`
`compl_loops_eq` 📖	mathematical	—	`Set` `Set.instSDiff` `E` `loops` `setOf` `IsNonloop`	—	—
`diff_coloops_indep_iff` 📖	mathematical	—	`Indep` `Set` `Set.instSDiff` `coloops`	—	`diff_indep_iff_indep_of_subset_coloops` `Set.Subset.rfl`
`diff_indep_iff_indep_of_subset_coloops` 📖	mathematical	`Set` `Set.instHasSubset` `coloops`	`Indep` `Set.instSDiff`	—	`union_indep_iff_indep_of_subset_coloops` `Set.diff_union_self`
`dual_coloops` 📖	mathematical	—	`coloops` `dual` `loops`	—	`coloops.eq_1` `dual_dual`
`dual_isColoop_iff_isLoop` 📖	mathematical	—	`IsColoop` `dual` `IsLoop`	—	`dual_dual` `IsColoop.dual_isLoop` `IsLoop.dual_isColoop`
`dual_isLoop_iff_isColoop` 📖	mathematical	—	`IsLoop` `dual` `IsColoop`	—	`dual_dual` `IsLoop.dual_isColoop` `IsColoop.dual_isLoop`
`dual_loops` 📖	mathematical	—	`loops` `dual` `coloops`	—	—
`eq_loopyOn_iff_loops` 📖	mathematical	—	`loopyOn` `loops` `E`	—	`loops.eq_1` `loopyOn_closure_eq` `closure_empty_eq_ground_iff`
`eq_loopyOn_iff_loops_eq` 📖	mathematical	—	`loopyOn` `loops` `E`	—	`loopyOn_closure_eq` `closure_empty_eq_ground_iff` `loops.eq_1`
`eq_restrict_removeLoops` 📖	mathematical	—	`restrict` `removeLoops` `E`	—	`removeLoops.eq_1` `ext_iff_indep` `Indep.isNonloop_of_mem`
`exists_isNonloop` 📖	mathematical	—	`IsNonloop`	—	`exists_isBase` `IsBase.nonempty` `Indep.isNonloop_of_mem` `IsBase.indep` `Set.Nonempty.some_mem`
`exists_mem_isCircuit_of_not_isColoop` 📖	mathematical	`Set` `Set.instMembership` `E` `IsColoop`	`IsCircuit`	—	`IsBase.fundCircuit_isCircuit`
`ext_indep_disjoint_loops_coloops` 📖	—	`E` `loops` `coloops` `Indep`	—	—	`ext_indep` `diff_coloops_indep_iff` `em` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.diff_subset` `Set.disjoint_union_right` `Set.disjoint_of_subset_left` `Set.disjoint_sdiff_left` `Set.not_disjoint_iff_nonempty_inter` `IsLoop.not_indep_of_mem` `IsLoop.not_isColoop` `isLoop_iff`
`freeOn_isNonloop_iff` 📖	mathematical	—	`IsNonloop` `freeOn` `Set` `Set.instMembership`	—	`indep_singleton` `freeOn_indep_iff` `Set.singleton_subset_iff`
`freeOn_not_isLoop` 📖	mathematical	—	`IsLoop` `freeOn`	—	`freeOn_closure_eq` `Set.empty_inter`
`indep_singleton` 📖	mathematical	—	`Indep` `Set` `Set.instSingletonSet` `IsNonloop`	—	`isNonloop_iff` `singleton_dep` `dep_iff` `not_imp_not` `Set.singleton_subset_iff` `Indep.subset_ground`
`instRankPosOfNonemptyOfLoopless` 📖	mathematical	—	`RankPos`	—	`ground_nonempty` `IsNonloop.rankPos` `isNonloop_of_loopless`
`isBasis_iff_empty_of_subset_loops` 📖	mathematical	`Set` `Set.instHasSubset` `loops`	`IsBasis` `Set.instEmptyCollection`	—	`IsBasis.isBasis_closure_right` `closure_eq_loops_of_subset`
`isBasis_loops_iff` 📖	mathematical	—	`IsBasis` `loops` `Set` `Set.instEmptyCollection`	—	`Indep.eq_empty_of_subset_loops` `IsBasis.indep` `IsBasis.subset` `Set.instReflSubset`
`isColoop_iff_diff_closure` 📖	mathematical	—	`IsColoop`	—	`isColoop_iff_diff_not_spanning` `spanning_iff_closure_eq`
`isColoop_iff_diff_not_spanning` 📖	mathematical	—	`IsColoop` `Spanning` `Set` `Set.instSDiff` `E` `Set.instSingletonSet`	—	`List.TFAE.out` `isColoop_tfae`
`isColoop_iff_forall_mem_closure_iff_mem` 📖	mathematical	—	`IsColoop` `Set` `Set.instMembership` `closure`	—	`List.TFAE.out` `isColoop_tfae`
`isColoop_iff_forall_mem_closure_iff_mem'` 📖	mathematical	—	`IsColoop` `Set` `Set.instMembership` `closure` `E`	—	`isColoop_iff_forall_mem_closure_iff_mem` `IsColoop.mem_ground` `closure_inter_ground` `Set.inter_subset_right` `Set.mem_inter_iff`
`isColoop_iff_forall_mem_compl_isCircuit` 📖	mathematical	—	`IsColoop` `Set` `Set.instMembership` `Set.instSDiff` `E`	—	`exists_isCircuit` `IsColoop.mem_ground`
`isColoop_iff_forall_mem_isBase` 📖	mathematical	—	`IsColoop` `Set` `Set.instMembership`	—	`List.TFAE.out` `isColoop_tfae`
`isColoop_iff_forall_notMem_isCircuit` 📖	mathematical	`Set` `Set.instMembership` `E`	`IsColoop`	—	`List.TFAE.out` `isColoop_tfae`
`isColoop_iff_mem_coloops` 📖	mathematical	—	`IsColoop` `Set` `Set.instMembership` `coloops`	—	—
`isColoop_iff_notMem_closure_compl` 📖	mathematical	`Set` `Set.instMembership` `E`	`IsColoop` `closure` `Set.instSDiff` `Set.instSingletonSet`	—	`isColoop_iff_diff_closure` `not_iff_not` `HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `closure_subset_ground` `eq_or_ne` `subset_closure` `Set.diff_subset`
`isColoop_tfae` 📖	mathematical	—	`List.TFAE` `IsColoop` `Set` `Set.instMembership` `coloops` `IsCocircuit` `Set.instSingletonSet` `E` `Spanning` `Set.instSDiff`	—	`singleton_isCocircuit` `sdiff_sdiff_right_self` `IsBase.compl_isBase_dual` `IsBase.compl_isBase_of_dual` `IsCircuit.inter_isCocircuit_ne_singleton` `IsCocircuit.subset_ground` `by_contra` `mem_closure_iff_exists_isCircuit` `IsBase.closure_eq` `mem_closure_of_mem'` `IsCircuit.mem_closure_diff_singleton_of_mem` `closure_subset_ground` `spanning_iff_compl_coindep` `Set.diff_subset` `dual_isLoop_iff_isColoop` `singleton_dep` `Set.diff_diff_cancel_left` `not_indep_iff` `IsColoop.mem_ground` `Set.diff_singleton_eq_self` `ground_spanning` `List.tfae_of_cycle`
`isLoop_iff` 📖	mathematical	—	`IsLoop` `Set` `Set.instMembership` `loops`	—	—
`isLoop_iff_closure_eq_loops` 📖	mathematical	`Set` `Set.instMembership` `E`	`IsLoop` `closure` `Set.instSingletonSet` `loops`	—	`isLoop_iff_closure_eq_loops_and_mem_ground`
`isLoop_iff_closure_eq_loops_and_mem_ground` 📖	mathematical	—	`IsLoop` `closure` `Set` `Set.instSingletonSet` `loops` `Set.instMembership` `E`	—	`IsLoop.closure` `IsLoop.mem_ground` `isLoop_iff` `closure_empty` `Set.singleton_subset_iff` `closure_subset_closure_iff_subset_closure` `loops.eq_1` `subset_refl` `Set.instReflSubset`
`isLoop_iff_forall_mem_compl_isBase` 📖	mathematical	—	`IsLoop` `Set` `Set.instMembership` `Set.instSDiff` `E`	—	`List.TFAE.out` `isLoop_tfae`
`isLoop_iff_forall_notMem_isBase` 📖	mathematical	`Set` `Set.instMembership` `E`	`IsLoop`	—	—
`isLoop_of_not_isNonloop` 📖	mathematical	`Set` `Set.instMembership` `E` `IsNonloop`	`IsLoop`	—	`isNonloop_iff`
`isLoop_or_isNonloop` 📖	mathematical	`Set` `Set.instMembership` `E`	`IsLoop` `IsNonloop`	—	`isNonloop_iff` `em`
`isLoop_tfae` 📖	mathematical	—	`List.TFAE` `IsLoop` `Set` `Set.instMembership` `closure` `Set.instEmptyCollection` `IsCircuit` `Set.instSingletonSet` `Dep`	—	`Indep.mem_closure_iff_of_notMem` `empty_indep` `Set.notMem_empty` `Set.instLawfulSingleton` `Indep.subset` `IsBase.indep` `Indep.exists_isBase_superset` `exists_isBase` `List.tfae_of_cycle`
`isNonloop_iff` 📖	mathematical	—	`IsNonloop` `IsLoop` `Set` `Set.instMembership` `E`	—	—
`isNonloop_iff_mem_compl_loops` 📖	mathematical	—	`IsNonloop` `Set` `Set.instMembership` `Set.instSDiff` `E` `loops`	—	`isNonloop_iff` `IsLoop.eq_1` `Set.mem_diff`
`isNonloop_iff_notMem_loops` 📖	mathematical	`Set` `Set.instMembership` `E`	`IsNonloop` `loops`	—	`isNonloop_iff` `isLoop_iff`
`isNonloop_iff_restrict_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`IsNonloop` `restrict`	—	`restrict_isNonloop_iff` `IsNonloop.of_restrict`
`isNonloop_of_loopless` 📖	mathematical	`Set` `Set.instMembership` `E`	`IsNonloop`	—	`not_isLoop_iff` `isLoop_iff` `loops_eq_empty` `Set.notMem_empty`
`isNonloop_of_notMem_closure` 📖	mathematical	`Set` `Set.instMembership` `closure` `E`	`IsNonloop`	—	`isNonloop_of_not_isLoop` `IsLoop.mem_closure`
`isNonloop_of_not_isLoop` 📖	mathematical	`Set` `Set.instMembership` `E` `IsLoop`	`IsNonloop`	—	—
`loopless_iff` 📖	mathematical	—	`Loopless` `loops` `Set` `Set.instEmptyCollection`	—	—
`loopless_iff_forall_isCircuit` 📖	mathematical	—	`Loopless` `Set.Nontrivial`	—	`IsLoop.isCircuit` `Set.Subsingleton.eq_empty_or_singleton` `IsCircuit.nonempty` `IsLoop.mem_ground` `singleton_isCircuit` `loopless_iff_forall_not_isLoop` `Mathlib.Tactic.Contrapose.contrapose_iff₁` `Mathlib.Tactic.Push.not_forall_eq`
`loopless_iff_forall_isNonloop` 📖	mathematical	—	`Loopless` `IsNonloop`	—	`isNonloop_of_loopless` `Set.subset_empty_iff` `IsNonloop.not_isLoop` `IsLoop.mem_ground`
`loopless_iff_forall_not_isLoop` 📖	mathematical	—	`Loopless` `IsLoop`	—	`not_isLoop` `loopless_iff_forall_isNonloop` `not_isLoop_iff`
`loops_eq_empty` 📖	mathematical	—	`loops` `Set` `Set.instEmptyCollection`	—	`Loopless.loops_eq_empty`
`loops_subset_ground` 📖	mathematical	—	`Set` `Set.instHasSubset` `loops` `E`	—	`closure_subset_ground`
`loopyOn_isLoop_iff` 📖	mathematical	—	`IsLoop` `loopyOn` `Set` `Set.instMembership`	—	`loopyOn_closure_eq`
`loopyOn_isLoopless_iff` 📖	mathematical	—	`Loopless` `loopyOn` `Set` `Set.instEmptyCollection`	—	—
`mapEmbedding_isLoop_iff` 📖	mathematical	—	`IsLoop` `mapEmbedding` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	—	`map_closure_eq` `Function.instEmbeddingLikeEmbedding`
`map_isLoop_iff` 📖	mathematical	`Set.InjOn` `E` `Set` `Set.instMembership`	`IsLoop` `map`	—	`isLoop_iff` `map_loops` `Set.InjOn.mem_image_iff` `loops_subset_ground`
`map_loops` 📖	mathematical	`Set.InjOn` `E`	`loops` `map` `Set.image`	—	`map_closure_eq`
`not_isLoop` 📖	mathematical	—	`IsLoop`	—	`IsNonloop.not_isLoop` `isNonloop_of_loopless` `Set.empty_inter`
`not_isLoop_iff` 📖	mathematical	`Set` `Set.instMembership` `E`	`IsLoop` `IsNonloop`	—	`IsNonloop.not_isLoop`
`not_isNonloop_iff` 📖	mathematical	`Set` `Set.instMembership` `E`	`IsNonloop` `IsLoop`	—	`not_isLoop_iff`
`not_isNonloop_iff_closure` 📖	mathematical	—	`IsNonloop` `closure` `Set` `Set.instSingletonSet` `loops`	—	`IsNonloop.mem_ground` `Set.singleton_inter_eq_empty` `Set.empty_inter`
`removeLoops_eq_restrict` 📖	mathematical	—	`removeLoops` `restrict` `setOf` `IsNonloop`	—	—
`removeLoops_eq_self` 📖	mathematical	—	`removeLoops`	—	`removeLoops.eq_1` `Loopless.ground_eq` `restrict_ground_eq_self`
`removeLoops_eq_self_iff` 📖	mathematical	—	`removeLoops` `Loopless`	—	`removeLoops_loopless` `removeLoops_eq_self`
`removeLoops_ground_eq` 📖	mathematical	—	`E` `removeLoops` `setOf` `IsNonloop`	—	—
`removeLoops_idem` 📖	mathematical	—	`removeLoops`	—	`removeLoops_eq_self` `removeLoops_loopless`
`removeLoops_indep_eq` 📖	mathematical	—	`Indep` `removeLoops`	—	`removeLoops_eq_restrict` `restrict_indep_iff` `Indep.isNonloop_of_mem`
`removeLoops_isBase_eq` 📖	mathematical	—	`IsBase` `removeLoops`	—	`isBase_iff_maximal_indep` `removeLoops_indep_eq`
`removeLoops_isBasis'_eq` 📖	mathematical	—	`IsBasis'` `removeLoops`	—	`removeLoops_indep_eq`
`removeLoops_isNonloop_eq` 📖	mathematical	—	`IsNonloop` `removeLoops`	—	`removeLoops_eq_restrict` `restrict_isNonloop_iff` `Set.mem_setOf`
`removeLoops_isRestriction` 📖	mathematical	—	`IsRestriction` `removeLoops`	—	`restrict_isRestriction` `IsNonloop.mem_ground`
`removeLoops_loopless` 📖	mathematical	—	`Loopless` `removeLoops`	—	—
`removeLoops_mono_isRestriction` 📖	mathematical	`IsRestriction`	`removeLoops`	—	`IsRestriction.isRestriction_removeLoops` `IsRestriction.trans` `removeLoops_isRestriction` `removeLoops_loopless`
`removeLoops_restrict_eq_restrict` 📖	mathematical	`Set` `Set.instHasSubset` `setOf` `IsNonloop`	`restrict` `removeLoops`	—	`removeLoops_eq_restrict` `restrict_restrict_eq`
`restrict_isColoop_iff` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`IsColoop` `restrict` `Set.instMembership` `closure` `Set.instSDiff` `Set.instSingletonSet`	—	`isColoop_iff_forall_notMem_isCircuit` `mem_closure_iff_exists_isCircuit` `restrict_isCircuit_iff` `Set.insert_diff_singleton` `Set.insert_eq_of_mem` `IsColoop.mem_ground`
`restrict_isLoop_iff` 📖	mathematical	—	`IsLoop` `restrict` `Set` `Set.instMembership` `E`	—	`restrict_closure_eq'` `Set.empty_inter`
`restrict_isNonloop_iff` 📖	mathematical	—	`IsNonloop` `restrict` `Set` `Set.instMembership`	—	`indep_singleton` `restrict_indep_iff` `Set.singleton_subset_iff`
`restrict_loops_eq` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`loops` `restrict` `Set.instInter`	—	`restrict_loops_eq'` `Set.diff_eq_empty` `Set.union_empty`
`restrict_loops_eq'` 📖	mathematical	—	`loops` `restrict` `Set` `Set.instUnion` `Set.instInter` `Set.instSDiff` `E`	—	`closure_empty` `restrict_closure_eq'` `Set.empty_inter`
`restrict_subset_loops_eq` 📖	mathematical	`Set` `Set.instHasSubset` `loops`	`restrict` `loopyOn`	—	`eq_loopyOn_iff_loops` `restrict_loops_eq'` `Set.inter_eq_self_of_subset_right` `Set.union_eq_self_of_subset_right` `Set.diff_subset` `restrict_ground_eq`
`restrict_univ_removeLoops_eq` 📖	mathematical	—	`removeLoops` `restrict` `Set.univ`	—	`removeLoops_eq_restrict` `restrict_restrict_eq` `Set.subset_univ`
`setOf_isNonloop_eq` 📖	mathematical	—	`setOf` `IsNonloop` `Set` `Set.instSDiff` `E` `loops`	—	`Set.ext` `isNonloop_iff_mem_compl_loops`
`singleton_dep` 📖	mathematical	—	`Dep` `Set` `Set.instSingletonSet` `IsLoop`	—	`List.TFAE.out` `isLoop_tfae`
`singleton_isCircuit` 📖	mathematical	—	`IsCircuit` `Set` `Set.instSingletonSet` `IsLoop`	—	`List.TFAE.out` `isLoop_tfae`
`singleton_isCocircuit` 📖	mathematical	—	`IsCocircuit` `Set` `Set.instSingletonSet` `IsColoop`	—	—
`singleton_not_indep` 📖	mathematical	`Set` `Set.instMembership` `E`	`Indep` `Set.instSingletonSet` `IsLoop`	—	`singleton_dep` `not_indep_iff`
`subsingleton_indep` 📖	mathematical	`Set.Subsingleton` `Set` `Set.instHasSubset` `E`	`Indep`	—	`Set.Subsingleton.eq_empty_or_singleton` `isNonloop_of_loopless`
`union_coloops_indep_iff` 📖	mathematical	—	`Indep` `Set` `Set.instUnion` `coloops`	—	`union_indep_iff_indep_of_subset_coloops` `Set.Subset.rfl`
`union_indep_iff_indep_of_subset_coloops` 📖	mathematical	`Set` `Set.instHasSubset` `coloops`	`Indep` `Set.instUnion`	—	`Indep.subset` `Set.subset_union_left` `Indep.exists_isBase_superset` `IsBase.indep` `Set.union_subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `IsColoop.mem_of_isBase`
`uniqueBaseOn_isLoop_iff` 📖	mathematical	—	`IsLoop` `uniqueBaseOn` `Set` `Set.instMembership` `Set.instSDiff`	—	`uniqueBaseOn_closure_eq` `Set.empty_inter` `Set.empty_union`
`uniqueBaseOn_isNonloop_iff` 📖	mathematical	—	`IsNonloop` `uniqueBaseOn` `Set` `Set.instMembership` `Set.instInter`	—	`indep_singleton` `uniqueBaseOn_indep_iff'` `Set.singleton_subset_iff`

Matroid.Indep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_loops` 📖	mathematical	`Matroid.Indep`	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Matroid.loops`	—	`by_contra` `Set.not_disjoint_iff` `Matroid.IsLoop.notMem_of_indep`
`eq_empty_of_subset_loops` 📖	mathematical	`Matroid.Indep` `Set` `Set.instHasSubset` `Matroid.loops`	`Set.instEmptyCollection`	—	`Set.eq_empty_iff_forall_notMem` `Matroid.IsLoop.notMem_of_indep`
`isNonloop` 📖	mathematical	`Matroid.Indep` `Set` `Set.instSingletonSet`	`Matroid.IsNonloop`	—	`Matroid.indep_singleton`
`isNonloop_of_mem` 📖	mathematical	`Matroid.Indep` `Set` `Set.instMembership`	`Matroid.IsNonloop`	—	`Matroid.not_isLoop_iff` `subset_ground` `Matroid.IsLoop.notMem_of_indep`

Matroid.IsBase

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coloops_subset` 📖	mathematical	`Matroid.IsBase`	`Set` `Set.instHasSubset` `Matroid.coloops`	—	`Matroid.IsColoop.mem_of_isBase`
`isColoop_iff_forall_notMem_fundCircuit` 📖	mathematical	`Matroid.IsBase` `Set` `Set.instMembership`	`Matroid.IsColoop` `Matroid.fundCircuit`	—	`Matroid.IsColoop.notMem_isCircuit` `fundCircuit_isCircuit` `em` `Matroid.subset_closure` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.diff_subset` `subset_ground` `Matroid.IsCircuit.mem_closure_diff_singleton_of_mem` `Matroid.mem_fundCircuit` `Matroid.closure_subset_closure` `Set.subset_diff_singleton` `Matroid.fundCircuit_subset_insert` `Matroid.isColoop_iff_notMem_closure_compl` `Set.notMem_subset` `Matroid.closure_subset_closure_of_subset_closure` `Matroid.Indep.notMem_closure_diff_of_mem` `indep`
`mem_of_isColoop` 📖	mathematical	`Matroid.IsBase` `Matroid.IsColoop`	`Set` `Set.instMembership`	—	`Matroid.isColoop_iff_forall_mem_isBase`

Matroid.IsBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inter_coloops_subset` 📖	mathematical	`Matroid.IsBasis`	`Set` `Set.instHasSubset` `Set.instInter` `Matroid.coloops`	—	`Matroid.IsBasis'.inter_coloops_subset` `isBasis'`

Matroid.IsBasis'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inter_coloops_subset` 📖	mathematical	`Matroid.IsBasis'`	`Set` `Set.instHasSubset` `Set.instInter` `Matroid.coloops`	—	`Matroid.IsColoop.mem_closure_iff_mem` `Matroid.IsBasis.closure_eq_right` `isBasis_closure_right`

Matroid.IsCircuit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_coloops` 📖	mathematical	`Matroid.IsCircuit`	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Matroid.coloops`	—	`Set.disjoint_right` `Matroid.IsColoop.notMem_isCircuit`
`isNonloop_of_mem` 📖	mathematical	`Matroid.IsCircuit` `Set.Nontrivial` `Set` `Set.instMembership`	`Matroid.IsNonloop`	—	`Matroid.isNonloop_of_not_isLoop` `subset_ground` `Matroid.IsLoop.eq_of_isCircuit_mem`
`isNonloop_of_mem_of_one_lt_card` 📖	mathematical	`Matroid.IsCircuit` `ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Set.encard` `Set` `Set.instMembership`	`Matroid.IsNonloop`	—	`Matroid.isNonloop_of_not_isLoop` `subset_ground` `LT.lt.ne` `Set.encard_singleton` `Matroid.IsLoop.eq_of_isCircuit_mem`
`not_isColoop_of_mem` 📖	mathematical	`Matroid.IsCircuit` `Set` `Set.instMembership`	`Matroid.IsColoop`	—	`Matroid.IsColoop.notMem_isCircuit`

Matroid.IsCocircuit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNonloop_of_mem` 📖	mathematical	`Matroid.IsCocircuit` `Set` `Set.instMembership`	`Matroid.IsNonloop`	—	`Matroid.not_isLoop_iff` `subset_ground` `Matroid.singleton_isCircuit` `Set.Nontrivial.exists_ne` `Matroid.IsCircuit.isCocircuit_inter_nontrivial` `Set.singleton_inter_of_mem`

Matroid.IsColoop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diff_not_spanning` 📖	mathematical	`Matroid.IsColoop`	`Matroid.Spanning` `Set` `Set.instSDiff` `Matroid.E` `Set.instSingletonSet`	—	`Matroid.isColoop_iff_diff_not_spanning`
`dual_isLoop` 📖	mathematical	`Matroid.IsColoop`	`Matroid.IsLoop` `Matroid.dual`	—	—
`insert_indep_of_indep` 📖	mathematical	`Matroid.IsColoop` `Matroid.Indep`	`Set` `Set.instInsert`	—	`em` `Set.insert_eq_of_mem` `Matroid.Indep.notMem_closure_iff_of_notMem` `mem_ground` `notMem_closure_of_notMem`
`isCocircuit` 📖	mathematical	`Matroid.IsColoop`	`Matroid.IsCocircuit` `Set` `Set.instSingletonSet`	—	`Matroid.IsLoop.isCircuit`
`isNonloop` 📖	mathematical	`Matroid.IsColoop`	`Matroid.IsNonloop`	—	`Matroid.exists_isBase` `Matroid.Indep.isNonloop_of_mem` `Matroid.IsBase.indep` `Matroid.isColoop_iff_forall_mem_isBase`
`mem_closure_iff_mem` 📖	mathematical	`Matroid.IsColoop`	`Set` `Set.instMembership` `Matroid.closure`	—	`Matroid.isColoop_iff_forall_mem_closure_iff_mem`
`mem_ground` 📖	mathematical	`Matroid.IsColoop`	`Set` `Set.instMembership` `Matroid.E`	—	`Matroid.IsLoop.mem_ground`
`mem_of_isBase` 📖	mathematical	`Matroid.IsColoop` `Matroid.IsBase`	`Set` `Set.instMembership`	—	`Matroid.isColoop_iff_forall_mem_isBase`
`mem_of_mem_closure` 📖	—	`Matroid.IsColoop` `Set` `Set.instMembership` `Matroid.closure`	—	—	`mem_closure_iff_mem`
`notMem_closure_of_notMem` 📖	mathematical	`Matroid.IsColoop` `Set` `Set.instMembership`	`Matroid.closure`	—	`mem_closure_iff_mem`
`notMem_isCircuit` 📖	mathematical	`Matroid.IsColoop` `Matroid.IsCircuit`	`Set` `Set.instMembership`	—	`Matroid.IsNonloop.not_isLoop` `Matroid.IsCocircuit.isNonloop_of_mem` `Matroid.IsCircuit.isCocircuit`

Matroid.IsFlat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`loops_subset` 📖	mathematical	`Matroid.IsFlat`	`Set` `Set.instHasSubset` `Matroid.loops`	—	`Matroid.IsLoop.mem_of_isFlat`

Matroid.IsLoop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure` 📖	mathematical	`Matroid.IsLoop`	`Matroid.closure` `Set` `Set.instSingletonSet` `Matroid.loops`	—	`Matroid.closure_eq_loops_of_subset` `Set.singleton_subset_iff`
`dep` 📖	mathematical	`Matroid.IsLoop`	`Matroid.Dep` `Set` `Set.instSingletonSet`	—	`Matroid.singleton_dep`
`dep_of_mem` 📖	mathematical	`Matroid.IsLoop` `Set` `Set.instMembership` `Set.instHasSubset` `Matroid.E`	`Matroid.Dep`	—	`Matroid.Dep.superset` `dep` `Set.singleton_subset_iff`
`dual_isColoop` 📖	mathematical	`Matroid.IsLoop`	`Matroid.IsColoop` `Matroid.dual`	—	`Matroid.IsColoop.eq_1` `Matroid.dual_dual`
`eq_of_isCircuit_mem` 📖	mathematical	`Matroid.IsLoop` `Matroid.IsCircuit` `Set` `Set.instMembership`	`Set.instSingletonSet`	—	`Matroid.IsCircuit.eq_of_subset_isCircuit` `isCircuit` `Set.singleton_subset_iff`
`isCircuit` 📖	mathematical	`Matroid.IsLoop`	`Matroid.IsCircuit` `Set` `Set.instSingletonSet`	—	`Matroid.singleton_isCircuit`
`isLoop_isRestriction` 📖	—	`Matroid.IsLoop` `Matroid.IsRestriction` `Set` `Set.instMembership` `Matroid.E`	—	—	`Matroid.IsRestriction.isLoop_iff`
`mem_closure` 📖	mathematical	`Matroid.IsLoop`	`Set` `Set.instMembership` `Matroid.closure`	—	`Matroid.closure_mono` `Set.empty_subset`
`mem_ground` 📖	mathematical	`Matroid.IsLoop`	`Set` `Set.instMembership` `Matroid.E`	—	`Matroid.closure_subset_ground`
`mem_of_isFlat` 📖	mathematical	`Matroid.IsLoop` `Matroid.IsFlat`	`Set` `Set.instMembership`	—	`mem_closure` `Matroid.IsFlat.closure`
`notMem_of_indep` 📖	mathematical	`Matroid.IsLoop` `Matroid.Indep`	`Set` `Set.instMembership`	—	`not_indep_of_mem`
`not_indep_of_mem` 📖	mathematical	`Matroid.IsLoop` `Set` `Set.instMembership`	`Matroid.Indep`	—	`Matroid.Dep.not_indep` `dep` `Matroid.Indep.subset` `Set.singleton_subset_iff`
`not_isColoop` 📖	mathematical	`Matroid.IsLoop`	`Matroid.IsColoop`	—	`Matroid.dual_isLoop_iff_isColoop` `Matroid.IsNonloop.not_isLoop` `Matroid.IsColoop.isNonloop` `Matroid.dual_dual`
`not_isNonloop` 📖	mathematical	`Matroid.IsLoop`	`Matroid.IsNonloop`	—	`Matroid.IsNonloop.not_isLoop`
`of_isRestriction` 📖	—	`Matroid.IsLoop` `Matroid.IsRestriction`	—	—	`Matroid.IsRestriction.isLoop_iff`

Matroid.IsNonloop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_eq_closure_iff_eq_or_dep` 📖	mathematical	`Matroid.IsNonloop`	`Matroid.closure` `Set` `Set.instSingletonSet` `Matroid.Indep` `Set.instInsert`	—	`eq_or_ne` `closure_eq_closure_iff_isCircuit_of_ne` `mem_ground` `Set.pair_diff_left` `Matroid.indep_singleton` `Set.pair_diff_right`
`closure_eq_closure_iff_isCircuit_of_ne` 📖	mathematical	`Matroid.IsNonloop`	`Matroid.closure` `Set` `Set.instSingletonSet` `Matroid.IsCircuit` `Set.instInsert`	—	`isNonloop_of_mem_closure` `Matroid.mem_closure_self` `mem_ground` `Matroid.isCircuit_iff_dep_forall_diff_singleton_indep` `Matroid.dep_iff` `Set.insert_subset_iff` `Set.singleton_subset_iff` `Matroid.Indep.insert_indep_iff_of_notMem` `Set.pair_diff_left` `Set.pair_diff_right` `Matroid.IsCircuit.closure_diff_singleton_eq`
`closure_eq_of_mem_closure` 📖	—	`Matroid.IsNonloop` `Set` `Set.instMembership` `Matroid.closure` `Set.instSingletonSet`	—	—	`Matroid.closure_closure` `Set.insert_eq_of_mem` `Matroid.closure_insert_closure_eq_closure_insert` `mem_closure_singleton` `Set.pair_comm`
`exists_mem_isBase` 📖	mathematical	`Matroid.IsNonloop`	`Matroid.IsBase` `Set` `Set.instMembership`	—	`Matroid.Indep.exists_isBase_superset` `Matroid.indep_singleton`
`exists_mem_isCocircuit` 📖	mathematical	`Matroid.IsNonloop`	`Matroid.IsCocircuit` `Set` `Set.instMembership`	—	`exists_mem_isBase` `Matroid.fundCocircuit_isCocircuit` `Matroid.mem_fundCocircuit`
`indep` 📖	mathematical	`Matroid.IsNonloop`	`Matroid.Indep` `Set` `Set.instSingletonSet`	—	`Matroid.indep_singleton`
`isNonloop_of_mem_closure` 📖	—	`Matroid.IsNonloop` `Set` `Set.instMembership` `Matroid.closure` `Set.instSingletonSet`	—	—	`Matroid.isNonloop_iff` `not_isLoop` `Matroid.isLoop_iff` `em` `Matroid.closure_loops` `Set.insert_eq_of_mem` `Mathlib.Tactic.Push.not_and_eq` `Matroid.closure_insert_congr_right` `Set.instLawfulSingleton` `Matroid.closure_inter_ground` `Set.inter_comm` `Set.inter_singleton_eq_empty` `Matroid.loops.eq_1`
`mem_closure_comm` 📖	mathematical	`Matroid.IsNonloop`	`Set` `Set.instMembership` `Matroid.closure` `Set.instSingletonSet`	—	`mem_closure_singleton`
`mem_closure_singleton` 📖	—	`Matroid.IsNonloop` `Set` `Set.instMembership` `Matroid.closure` `Set.instSingletonSet`	—	—	`Set.union_empty` `Set.singleton_union` `Matroid.closure_exchange` `Matroid.isNonloop_iff_notMem_loops` `mem_ground`
`mem_ground` 📖	mathematical	`Matroid.IsNonloop`	`Set` `Set.instMembership` `Matroid.E`	—	—
`not_isLoop` 📖	mathematical	`Matroid.IsNonloop`	`Matroid.IsLoop`	—	—
`of_isRestriction` 📖	—	`Matroid.IsNonloop` `Matroid.IsRestriction`	—	—	`of_restrict`
`of_restrict` 📖	—	`Matroid.IsNonloop` `Matroid.restrict`	—	—	`Matroid.restrict_isNonloop_iff`
`rankPos` 📖	mathematical	`Matroid.IsNonloop`	`Matroid.RankPos`	—	`Matroid.Indep.rankPos_of_nonempty` `indep` `Set.singleton_nonempty`
`removeLoops_isNonloop` 📖	mathematical	`Matroid.IsNonloop`	`Matroid.removeLoops`	—	`Matroid.removeLoops_isNonloop_eq`

Matroid.IsRestriction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLoop_iff` 📖	mathematical	`Matroid.IsRestriction`	`Matroid.IsLoop` `Set` `Set.instMembership` `Matroid.E`	—	—
`isRestriction_removeLoops` 📖	mathematical	`Matroid.IsRestriction`	`Matroid.removeLoops`	—	`exists_eq_restrict` `of_subset` `Matroid.IsNonloop.of_restrict` `Matroid.isNonloop_of_loopless`
`loopless` 📖	mathematical	`Matroid.IsRestriction`	`Matroid.Loopless`	—	`Matroid.loopless_iff` `Matroid.restrict_loops_eq` `Matroid.loops_eq_empty` `Set.empty_inter`

Matroid.Loopless

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ground_eq` 📖	mathematical	—	`Matroid.E` `setOf` `Matroid.IsNonloop`	—	`Set.ext` `Matroid.isNonloop_of_loopless` `Matroid.IsNonloop.mem_ground`
`loops_eq_empty` 📖	mathematical	—	`Matroid.loops` `Set` `Set.instEmptyCollection`	—	—

---

← Back to Index