Circuit

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

Statistics

Metric	Count
Definitions `IsCircuit`, `IsCocircuit`, `fundCircuit`, `fundCocircuit`	4
Theorems `exists_isCircuit_subset`, `exists_isCocircuit_inter_eq_mem`, `fundCircuit_isCircuit`, `insert_isCircuit_of_forall`, `insert_isCircuit_of_forall_of_nontrivial`, `mem_fundCircuit_iff`, `compl_closure_diff_singleton_isCocircuit`, `fundCircuit_isCircuit`, `mem_fundCocircuit_iff_mem_fundCircuit`, `closure_diff_singleton_eq`, `dep`, `diff_singleton_indep`, `diff_singleton_isBasis`, `dual_rankPos`, `elimination`, `eq_fundCircuit_of_subset`, `eq_of_dep_subset`, `eq_of_not_indep_subset`, `eq_of_subset_isCircuit`, `eq_of_superset_isCircuit`, `finite`, `inter_isCocircuit_ne_singleton`, `isBasis_iff_eq_diff_singleton`, `isBasis_iff_insert_eq`, `isCircuit_restrict_of_subset`, `isCocircuit`, `isCocircuit_disjoint_or_nontrivial_inter`, `isCocircuit_inter_nontrivial`, `mem_closure_diff_singleton_of_mem`, `minimal`, `minimal_not_indep`, `nonempty`, `not_indep`, `not_ssubset`, `ssubset_indep`, `strong_elimination`, `strong_multi_elimination`, `strong_multi_elimination_insert`, `strong_multi_elimination_set`, `subset_closure_diff_singleton`, `subset_ground`, `isCircuit`, `nonempty`, `subset_ground`, `coindep_iff_forall_subset_not_isCocircuit`, `dep_iff_superset_isCircuit`, `dep_iff_superset_isCircuit'`, `dual_isCocircuit_iff`, `dual_rankPos_iff_exists_isCircuit`, `empty_not_isCircuit`, `exists_isCircuit`, `exists_isCircuit_of_mem_closure`, `exists_mem_finite_closure_of_mem_closure`, `exists_subset_finite_closure_of_subset_closure`, `ext_iff_isCircuit`, `ext_isCircuit`, `ext_isCircuit_not_indep`, `finitary_iff_forall_isCircuit_finite`, `fundCircuit_diff_eq_inter`, `fundCircuit_eq_of_mem`, `fundCircuit_eq_of_notMem_ground`, `fundCircuit_eq_sInter`, `fundCircuit_restrict`, `fundCircuit_restrict_univ`, `fundCircuit_subset_ground`, `fundCircuit_subset_insert`, `fundCocircuit_eq_of_notMem`, `fundCocircuit_eq_of_notMem_ground`, `fundCocircuit_inter_eq`, `fundCocircuit_isCocircuit`, `fundCocircuit_subset_insert_compl`, `indep_iff_forall_subset_not_isCircuit`, `indep_iff_forall_subset_not_isCircuit'`, `isCircuit_antichain`, `isCircuit_def`, `isCircuit_iff`, `isCircuit_iff_dep_forall_diff_singleton_indep`, `isCircuit_iff_forall_ssubset`, `isCircuit_iff_minimal_not_indep`, `isCocircuit_def`, `isCocircuit_iff_minimal`, `isCocircuit_iff_minimal_compl_nonspanning`, `isCocircuit_iff_minimal_compl_nonspanning'`, `mem_closure_iff_exists_isCircuit`, `mem_fundCircuit`, `mem_fundCocircuit`, `rankPos_iff_exists_isCocircuit`, `restrict_isCircuit_iff`	88
Total	92

Matroid

Definitions

Name	Category	Theorems
`IsCircuit` 📖	MathDef	32 math math: `isLoop_tfae`, `Indep.insert_isCircuit_of_forall`, `dual_rankPos_iff_exists_isCircuit`, `indep_iff_forall_subset_not_isCircuit`, `circuit_iff_delete_of_disjoint`, `dep_iff_superset_isCircuit'`, `restrict_isCircuit_iff`, `isCocircuit_def`, `singleton_isCircuit`, `Dep.exists_isCircuit_subset`, `isCircuit_iff_dep_forall_diff_singleton_indep`, `Indep.insert_isCircuit_of_forall_of_nontrivial`, `dual_isCocircuit_iff`, `isCircuit_def`, `IsBase.fundCircuit_isCircuit`, `exists_isCircuit`, `isCircuit_iff_forall_ssubset`, `exists_isCircuit_of_mem_closure`, `isCircuit_iff_minimal_not_indep`, `IsNonloop.closure_eq_closure_iff_isCircuit_of_ne`, `isCircuit_antichain`, `IsLoop.isCircuit`, `IsCocircuit.isCircuit`, `exists_mem_isCircuit_of_not_isColoop`, `dep_iff_superset_isCircuit`, `empty_not_isCircuit`, `Indep.fundCircuit_isCircuit`, `isCircuit_iff`, `delete_isCircuit_iff`, `ext_iff_isCircuit`, `mem_closure_iff_exists_isCircuit`, `indep_iff_forall_subset_not_isCircuit'`
`IsCocircuit` 📖	MathDef	16 math math: `isCocircuit_iff_minimal_compl_nonspanning`, `contract_isCocircuit_iff`, `coindep_iff_forall_subset_not_isCocircuit`, `IsCircuit.isCocircuit`, `IsBase.compl_closure_diff_singleton_isCocircuit`, `isCocircuit_def`, `Indep.exists_isCocircuit_inter_eq_mem`, `dual_isCocircuit_iff`, `rankPos_iff_exists_isCocircuit`, `isColoop_tfae`, `isCocircuit_iff_minimal`, `fundCocircuit_isCocircuit`, `singleton_isCocircuit`, `isCocircuit_iff_minimal_compl_nonspanning'`, `IsColoop.isCocircuit`, `IsNonloop.exists_mem_isCocircuit`
`fundCircuit` 📖	CompOp	15 math math: `IsCircuit.eq_fundCircuit_of_subset`, `Indep.mem_fundCircuit_iff`, `fundCircuit_subset_ground`, `fundCircuit_restrict`, `fundCircuit_eq_sInter`, `fundCircuit_diff_eq_inter`, `fundCircuit_restrict_univ`, `fundCircuit_eq_of_mem`, `IsBase.fundCircuit_isCircuit`, `fundCircuit_eq_of_notMem_ground`, `IsBase.isColoop_iff_forall_notMem_fundCircuit`, `IsBase.mem_fundCocircuit_iff_mem_fundCircuit`, `Indep.fundCircuit_isCircuit`, `fundCircuit_subset_insert`, `mem_fundCircuit`
`fundCocircuit` 📖	CompOp	7 math math: `fundCocircuit_subset_insert_compl`, `mem_fundCocircuit`, `fundCocircuit_isCocircuit`, `fundCocircuit_inter_eq`, `fundCocircuit_eq_of_notMem_ground`, `IsBase.mem_fundCocircuit_iff_mem_fundCircuit`, `fundCocircuit_eq_of_notMem`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coindep_iff_forall_subset_not_isCocircuit` 📖	mathematical	—	`Coindep` `IsCocircuit` `Set` `Set.instHasSubset` `E`	—	`indep_iff_forall_subset_not_isCircuit'`
`dep_iff_superset_isCircuit` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`Dep` `IsCircuit`	—	`Dep.exists_isCircuit_subset` `Dep.superset` `IsCircuit.dep`
`dep_iff_superset_isCircuit'` 📖	mathematical	—	`Dep` `Set` `Set.instHasSubset` `IsCircuit` `E`	—	`Dep.exists_isCircuit_subset` `Dep.subset_ground` `Dep.superset` `IsCircuit.dep`
`dual_isCocircuit_iff` 📖	mathematical	—	`IsCocircuit` `dual` `IsCircuit`	—	`isCocircuit_def` `dual_dual`
`dual_rankPos_iff_exists_isCircuit` 📖	mathematical	—	`RankPos` `dual` `IsCircuit`	—	`rankPos_iff` `dual_isBase_iff` `Set.diff_empty` `not_iff_comm` `ground_indep_iff_isBase` `indep_iff_forall_subset_not_isCircuit` `Set.instReflSubset` `IsCircuit.subset_ground`
`empty_not_isCircuit` 📖	mathematical	—	`IsCircuit` `Set` `Set.instEmptyCollection`	—	`IsCircuit.nonempty`
`exists_isCircuit` 📖	mathematical	—	`IsCircuit`	—	`dual_rankPos_iff_exists_isCircuit`
`exists_isCircuit_of_mem_closure` 📖	mathematical	`Set` `Set.instMembership` `closure`	`Set.instHasSubset` `Set.instInsert` `IsCircuit`	—	`exists_isBasis'` `HasSubset.Subset.trans` `Set.instIsTransSubset` `fundCircuit_subset_insert` `Set.insert_subset_insert` `IsBasis'.subset` `Indep.fundCircuit_isCircuit` `IsBasis'.indep` `IsBasis'.closure_eq_closure` `Set.notMem_subset` `mem_fundCircuit`
`exists_mem_finite_closure_of_mem_closure` 📖	mathematical	`Set` `Set.instMembership` `closure`	`Set.instHasSubset` `Set.Finite` `Indep`	—	`exists_isBasis` `HasSubset.Subset.trans` `Set.instIsTransSubset` `IsBasis.subset` `Set.Finite.subset` `Set.finite_singleton` `IsBasis.indep` `IsBasis.subset_closure` `exists_isCircuit_of_mem_closure` `Set.Finite.diff` `IsCircuit.finite` `IsCircuit.diff_singleton_indep` `IsCircuit.mem_closure_diff_singleton_of_mem`
`exists_subset_finite_closure_of_subset_closure` 📖	mathematical	`Set` `Set.instHasSubset` `closure`	`Set.Finite` `Indep`	—	`Set.Finite.induction_on_subset` `exists_mem_finite_closure_of_mem_closure` `Set.union_subset` `Set.Finite.union` `Set.insert_subset` `closure_mono` `Set.subset_union_left` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.subset_union_right` `exists_isBasis'` `IsBasis'.subset` `Set.Finite.subset` `IsBasis'.indep` `IsBasis'.closure_eq_closure`
`ext_iff_isCircuit` 📖	mathematical	—	`E` `IsCircuit`	—	`ext_isCircuit`
`ext_isCircuit` 📖	—	`E` `IsCircuit`	—	—	`em` `IsCircuit.subset_ground` `LE.le.trans_eq` `ext_indep` `indep_iff_forall_subset_not_isCircuit`
`ext_isCircuit_not_indep` 📖	—	`E` `Indep`	—	—	`ext_isCircuit` `Dep.exists_isCircuit_subset` `not_indep_iff` `IsCircuit.eq_of_not_indep_subset`
`finitary_iff_forall_isCircuit_finite` 📖	mathematical	—	`Finitary` `Set.Finite`	—	`IsCircuit.finite` `indep_iff_not_dep` `Dep.exists_isCircuit_subset` `Dep.not_indep` `IsCircuit.dep` `Indep.subset_ground` `Set.finite_singleton`
`fundCircuit_diff_eq_inter` 📖	mathematical	`Set` `Set.instMembership`	`Set.instSDiff` `fundCircuit` `Set.instSingletonSet` `Set.instInter`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Set.subset_inter` `Set.diff_subset` `Set.subset_diff_singleton` `Set.inter_subset_left`
`fundCircuit_eq_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`fundCircuit` `Set.instSingletonSet`	—	`Set.singleton_subset_iff` `Set.Subset.rfl` `Set.instReflSubset` `Set.instAntisymmSubset`
`fundCircuit_eq_of_notMem_ground` 📖	mathematical	`Set` `Set.instMembership` `E`	`fundCircuit` `Set.instSingletonSet`	—	`closure_inter_ground` `Set.singleton_inter_eq_empty` `Set.empty_subset` `Eq.subset` `Set.instReflSubset` `Set.instAntisymmSubset`
`fundCircuit_eq_sInter` 📖	mathematical	`Set` `Set.instMembership` `closure`	`fundCircuit` `Set.instInsert` `Set.sInter` `setOf` `Set.instHasSubset`	—	`fundCircuit.eq_1` `closure_subset_closure_iff_subset_closure` `mem_ground_of_mem_closure` `Set.inter_eq_self_of_subset_right` `Set.sInter_subset_of_mem` `Set.instReflSubset`
`fundCircuit_restrict` 📖	mathematical	`Set` `Set.instHasSubset` `Set.instMembership` `E`	`fundCircuit` `restrict`	—	`restrict_closure_eq` `subset_antisymm` `Set.instAntisymmSubset` `Set.insert_subset_insert` `Set.inter_subset_inter` `subset_refl` `Set.instReflSubset` `Set.sInter_subset_sInter` `Set.setOf_subset_setOf_of_imp` `Mathlib.Tactic.GCongr.and_right_mono` `restrict_closure_eq'` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.inter_subset_inter_left` `Set.inter_eq_self_of_subset_left` `Set.subset_union_left` `closure_subset_closure_of_subset_closure` `subset_trans` `mem_closure_of_mem'` `Set.mem_singleton`
`fundCircuit_restrict_univ` 📖	mathematical	—	`fundCircuit` `restrict` `Set.univ`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.subset_inter` `closure_subset_ground` `Set.union_inter_distrib_right` `Set.diff_inter_self` `Set.union_empty` `Set.subset_union_left` `restrict_closure_eq'` `Set.inter_univ`
`fundCircuit_subset_ground` 📖	mathematical	`Set` `Set.instMembership` `E` `Set.instHasSubset`	`fundCircuit`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `fundCircuit_subset_insert` `Set.insert_subset`
`fundCircuit_subset_insert` 📖	mathematical	—	`Set` `Set.instHasSubset` `fundCircuit` `Set.instInsert`	—	`Set.insert_subset_insert` `Set.inter_subset_left`
`fundCocircuit_eq_of_notMem` 📖	mathematical	`Set` `Set.instMembership`	`fundCocircuit` `Set.instSingletonSet`	—	`fundCocircuit.eq_1` `fundCircuit_eq_of_mem` `fundCocircuit_eq_of_notMem_ground`
`fundCocircuit_eq_of_notMem_ground` 📖	mathematical	`Set` `Set.instMembership` `E`	`fundCocircuit` `Set.instSingletonSet`	—	`fundCocircuit.eq_1` `fundCircuit_eq_of_notMem_ground`
`fundCocircuit_inter_eq` 📖	mathematical	`Set` `Set.instMembership`	`Set.instInter` `fundCocircuit` `Set.instSingletonSet`	—	`subset_antisymm` `Set.instAntisymmSubset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.inter_subset_inter_left` `fundCocircuit_subset_insert_compl` `instIsEmptyFalse` `Set.singleton_subset_iff` `mem_fundCocircuit`
`fundCocircuit_isCocircuit` 📖	mathematical	`Set` `Set.instMembership` `IsBase`	`IsCocircuit` `fundCocircuit`	—	`Indep.fundCircuit_isCircuit` `IsBase.indep` `IsBase.compl_isBase_dual` `IsBase.closure_eq` `dual_ground` `IsBase.subset_ground`
`fundCocircuit_subset_insert_compl` 📖	mathematical	—	`Set` `Set.instHasSubset` `fundCocircuit` `Set.instInsert` `Set.instSDiff` `E`	—	`fundCircuit_subset_insert`
`indep_iff_forall_subset_not_isCircuit` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`Indep` `IsCircuit`	—	`indep_iff_forall_subset_not_isCircuit'`
`indep_iff_forall_subset_not_isCircuit'` 📖	mathematical	—	`Indep` `IsCircuit` `Set` `Set.instHasSubset` `E`	—	—
`isCircuit_antichain` 📖	mathematical	—	`IsAntichain` `Set` `Set.instHasSubset` `setOf` `IsCircuit`	—	`Minimal.eq_of_subset` `IsCircuit.minimal` `IsCircuit.dep`
`isCircuit_def` 📖	mathematical	—	`IsCircuit` `Minimal` `Set` `Set.instLE` `Dep`	—	—
`isCircuit_iff` 📖	mathematical	—	`IsCircuit` `Dep`	—	—
`isCircuit_iff_dep_forall_diff_singleton_indep` 📖	mathematical	—	`IsCircuit` `Dep` `Indep` `Set` `Set.instSDiff` `Set.instSingletonSet`	—	`isCircuit_iff_minimal_not_indep` `Set.minimal_iff_forall_diff_singleton` `Indep.subset` `not_indep_iff` `IsCircuit.subset_ground` `Dep.subset_ground`
`isCircuit_iff_forall_ssubset` 📖	mathematical	—	`IsCircuit` `Dep` `Indep`	—	`IsCircuit.eq_1` `Set.minimal_iff_forall_ssubset` `not_dep_iff` `HasSubset.Subset.trans` `Set.instIsTransSubset` `HasSSubset.SSubset.subset` `Set.instIsNonstrictStrictOrderSubsetSSubset` `Dep.subset_ground` `Indep.not_dep`
`isCircuit_iff_minimal_not_indep` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`IsCircuit` `Minimal` `Set.instLE` `Indep`	—	`IsCircuit.minimal_not_indep` `not_indep_iff` `Minimal.prop` `Eq.le` `Minimal.eq_of_superset` `Dep.not_indep`
`isCocircuit_def` 📖	mathematical	—	`IsCocircuit` `IsCircuit` `dual`	—	—
`isCocircuit_iff_minimal` 📖	mathematical	—	`IsCocircuit` `Minimal` `Set` `Set.instLE`	—	`dual_dep_iff_forall` `isCocircuit_def` `isCircuit_def` `minimal_iff_minimal_of_imp_of_forall` `Set.inter_subset_left` `Set.inter_assoc` `Set.inter_eq_self_of_subset_right` `IsBase.subset_ground` `Set.inter_subset_right`
`isCocircuit_iff_minimal_compl_nonspanning` 📖	mathematical	—	`IsCocircuit` `Minimal` `Set` `Set.instLE` `Spanning` `Set.instSDiff` `E`	—	`spanning_iff_exists_isBase_subset` `IsBase.subset_ground` `Set.inter_comm` `isCocircuit_iff_minimal`
`isCocircuit_iff_minimal_compl_nonspanning'` 📖	mathematical	—	`IsCocircuit` `Minimal` `Set` `Set.instLE` `Spanning` `Set.instSDiff` `E` `Set.instHasSubset`	—	`isCocircuit_iff_minimal_compl_nonspanning` `minimal_iff_minimal_of_imp_of_forall` `Set.inter_subset_left` `Set.diff_inter_self_eq_diff` `Set.inter_subset_right`
`mem_closure_iff_exists_isCircuit` 📖	mathematical	`Set` `Set.instMembership`	`closure` `Set.instHasSubset` `Set.instInsert` `IsCircuit`	—	`exists_isCircuit_of_mem_closure` `Set.mem_of_mem_of_subset` `IsCircuit.mem_closure_diff_singleton_of_mem` `closure_subset_closure`
`mem_fundCircuit` 📖	mathematical	—	`Set` `Set.instMembership` `fundCircuit`	—	`Set.mem_insert`
`mem_fundCocircuit` 📖	mathematical	—	`Set` `Set.instMembership` `fundCocircuit`	—	`Set.mem_insert`
`rankPos_iff_exists_isCocircuit` 📖	mathematical	—	`RankPos` `IsCocircuit`	—	`dual_dual` `dual_rankPos_iff_exists_isCircuit`
`restrict_isCircuit_iff` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`IsCircuit` `restrict`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `IsCircuit.isCircuit_restrict_of_subset`

Matroid.Dep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isCircuit_subset` 📖	mathematical	`Matroid.Dep`	`Set` `Set.instHasSubset` `Matroid.IsCircuit`	—	`Matroid.exists_isBasis` `subset_ground` `Set.exists_of_ssubset` `HasSubset.Subset.ssubset_of_ne` `Set.instIsNonstrictStrictOrderSubsetSSubset` `Set.instAntisymmSubset` `Matroid.IsBasis.subset` `Matroid.Indep.not_dep` `Matroid.IsBasis.indep` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Matroid.fundCircuit_subset_insert` `Set.insert_subset` `Matroid.Indep.fundCircuit_isCircuit` `Matroid.IsBasis.subset_closure`

Matroid.Indep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isCocircuit_inter_eq_mem` 📖	mathematical	`Matroid.Indep` `Set` `Set.instMembership`	`Matroid.IsCocircuit` `Set.instInter` `Set.instSingletonSet`	—	`exists_isBase_superset` `Matroid.fundCocircuit_isCocircuit` `subset_antisymm_iff` `Set.instReflSubset` `Set.instAntisymmSubset` `Set.subset_inter_iff` `Set.singleton_subset_iff` `Matroid.mem_fundCocircuit` `Matroid.fundCocircuit_inter_eq` `Set.inter_subset_inter_right`
`fundCircuit_isCircuit` 📖	mathematical	`Matroid.Indep` `Set` `Set.instMembership` `Matroid.closure`	`Matroid.IsCircuit` `Matroid.fundCircuit`	—	`Set.sInter_subset_of_mem` `Set.instReflSubset` `Matroid.fundCircuit_eq_sInter` `insert_isCircuit_of_forall` `subset` `closure_sInter_eq_biInter_closure_of_forall_subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.diff_subset`
`insert_isCircuit_of_forall` 📖	mathematical	`Matroid.Indep` `Set` `Set.instMembership` `Matroid.closure` `Set.instSDiff` `Set.instSingletonSet`	`Matroid.IsCircuit` `Set.instInsert`	—	`Matroid.isCircuit_iff_dep_forall_diff_singleton_indep` `insert_dep_iff` `Set.insert_diff_of_mem` `Set.diff_singleton_eq_self` `Set.insert_diff_singleton_comm` `insert_indep_iff_of_notMem` `diff` `Matroid.mem_ground_of_mem_closure`
`insert_isCircuit_of_forall_of_nontrivial` 📖	mathematical	`Matroid.Indep` `Set.Nontrivial` `Set` `Set.instMembership` `Matroid.closure` `Set.instSDiff` `Set.instSingletonSet`	`Matroid.IsCircuit` `Set.instInsert`	—	`insert_isCircuit_of_forall` `Set.Nontrivial.exists_ne` `Matroid.mem_closure_of_mem'`
`mem_fundCircuit_iff` 📖	mathematical	`Matroid.Indep` `Set` `Set.instMembership` `Matroid.closure`	`Matroid.fundCircuit` `Set.instSDiff` `Set.instInsert` `Set.instSingletonSet`	—	`eq_or_ne` `Set.insert_diff_of_mem` `diff` `Set.diff_subset` `by_contra` `Matroid.closure_subset_closure` `Set.subset_diff_singleton` `Matroid.fundCircuit_eq_sInter` `Set.insert_diff_singleton_comm` `insert_indep_iff` `Matroid.mem_ground_of_mem_closure`

Matroid.IsBase

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compl_closure_diff_singleton_isCocircuit` 📖	mathematical	`Matroid.IsBase` `Set` `Set.instMembership`	`Matroid.IsCocircuit` `Set.instSDiff` `Matroid.E` `Matroid.closure` `Set.instSingletonSet`	—	`Matroid.isCocircuit_iff_minimal_compl_nonspanning` `minimal_subset_iff` `Set.diff_diff_cancel_left` `Matroid.closure_subset_ground` `Matroid.closure_spanning_iff` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.diff_subset` `subset_ground` `Matroid.isBase_iff_minimal_spanning` `Minimal.notMem_of_prop_diff_singleton` `HasSubset.Subset.antisymm'` `Set.instAntisymmSubset` `Set.diff_subset_comm` `by_contra` `exchange_base_of_notMem_closure` `Matroid.Spanning.superset` `spanning` `Set.insert_subset` `Matroid.subset_closure` `Set.subset_diff` `Disjoint.symm`
`fundCircuit_isCircuit` 📖	mathematical	`Matroid.IsBase` `Set` `Set.instMembership` `Matroid.E`	`Matroid.IsCircuit` `Matroid.fundCircuit`	—	`Matroid.Indep.fundCircuit_isCircuit` `indep` `closure_eq`
`mem_fundCocircuit_iff_mem_fundCircuit` 📖	mathematical	`Matroid.IsBase`	`Set` `Set.instMembership` `Matroid.fundCocircuit` `Matroid.fundCircuit`	—	`eq_or_ne` `compl_isBase_dual` `em'` `Matroid.fundCircuit_eq_of_notMem_ground` `Matroid.fundCocircuit.eq_1` `Matroid.fundCircuit_eq_of_mem` `Matroid.fundCocircuit_subset_insert_compl` `Matroid.Indep.mem_fundCircuit_iff` `indep` `closure_eq` `compl_isBase_of_dual` `exchange_isBase_of_indep'` `Matroid.Indep.subset` `Set.diff_diff_right` `Set.inter_eq_self_of_subset_right` `Set.union_singleton` `Set.insert_comm` `Set.diff_diff` `Set.diff_diff_cancel_left` `subset_ground` `Set.insert_diff_self_of_mem` `Set.instReflSubset` `Matroid.dual_dual` `sdiff_sdiff_right_self`

Matroid.IsCircuit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_diff_singleton_eq` 📖	mathematical	`Matroid.IsCircuit`	`Matroid.closure` `Set` `Set.instSDiff` `Set.instSingletonSet`	—	`em` `Matroid.IsBasis.closure_eq_closure` `diff_singleton_isBasis` `Set.diff_singleton_eq_self`
`dep` 📖	mathematical	`Matroid.IsCircuit`	`Matroid.Dep`	—	`Minimal.prop`
`diff_singleton_indep` 📖	mathematical	`Matroid.IsCircuit` `Set` `Set.instMembership`	`Matroid.Indep` `Set.instSDiff` `Set.instSingletonSet`	—	`ssubset_indep` `Set.diff_singleton_ssubset`
`diff_singleton_isBasis` 📖	mathematical	`Matroid.IsCircuit` `Set` `Set.instMembership`	`Matroid.IsBasis` `Set.instSDiff` `Set.instSingletonSet`	—	`Set.insert_eq_of_mem` `Set.insert_diff_singleton` `Matroid.Indep.isBasis_insert_iff` `diff_singleton_indep` `dep`
`dual_rankPos` 📖	mathematical	`Matroid.IsCircuit`	`Matroid.RankPos` `Matroid.dual`	—	`Matroid.dual_rankPos_iff_exists_isCircuit`
`elimination` 📖	mathematical	`Matroid.IsCircuit`	`Set` `Set.instHasSubset` `Set.instSDiff` `Set.instUnion` `Set.instSingletonSet`	—	`eq_of_subset_isCircuit` `Set.not_subset` `strong_elimination` `Set.subset_diff_singleton` `Set.subset_union_right` `Set.subset_union_left`
`eq_fundCircuit_of_subset` 📖	mathematical	`Matroid.IsCircuit` `Matroid.Indep` `Set` `Set.instHasSubset` `Set.instInsert`	`Matroid.fundCircuit`	—	`Set.subset_insert_iff` `not_indep` `Matroid.Indep.subset` `Matroid.IsBasis.subset_closure` `diff_singleton_isBasis` `Matroid.closure_subset_closure` `Matroid.fundCircuit_eq_sInter` `Set.insert_subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.sInter_subset_of_mem` `Set.diff_subset` `eq_of_superset_isCircuit` `Matroid.Indep.fundCircuit_isCircuit` `Matroid.Indep.mem_closure_iff` `Matroid.Dep.superset` `dep` `subset_ground` `Matroid.Indep.subset_ground` `Set.insert_eq_of_mem` `Set.instReflSubset`
`eq_of_dep_subset` 📖	—	`Matroid.IsCircuit` `Matroid.Dep` `Set` `Set.instHasSubset`	—	—	`eq_of_not_indep_subset` `Matroid.Dep.not_indep`
`eq_of_not_indep_subset` 📖	—	`Matroid.IsCircuit` `Matroid.Indep` `Set` `Set.instHasSubset`	—	—	`eq_of_le_of_not_lt` `ssubset_indep`
`eq_of_subset_isCircuit` 📖	—	`Matroid.IsCircuit` `Set` `Set.instHasSubset`	—	—	`eq_of_dep_subset` `dep`
`eq_of_superset_isCircuit` 📖	—	`Matroid.IsCircuit` `Set` `Set.instHasSubset`	—	—	`eq_of_subset_isCircuit`
`finite` 📖	mathematical	`Matroid.IsCircuit`	`Set.Finite`	—	`Matroid.Dep.not_indep` `dep` `Mathlib.Tactic.Push.not_forall_eq` `Matroid.indep_iff_forall_finite_subset_indep` `eq_of_not_indep_subset`
`inter_isCocircuit_ne_singleton` 📖	—	`Matroid.IsCircuit` `Matroid.IsCocircuit`	—	—	`Eq.subset` `Set.instReflSubset` `Set.diff_singleton_ssubset` `Matroid.spanning_iff_ground_subset_closure` `Matroid.Spanning.closure_eq` `Set.diff_diff_eq_sdiff_union` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.inter_subset_left` `subset_ground` `Matroid.closure_subset_closure` `Set.subset_union_left` `Set.union_assoc` `Set.singleton_union` `Set.insert_eq_of_mem` `Matroid.closure_union_congr_right` `closure_diff_singleton_eq` `Set.union_eq_self_of_subset_right` `Set.diff_self_inter` `Set.diff_subset_diff_left` `subset_refl`
`isBasis_iff_eq_diff_singleton` 📖	mathematical	`Matroid.IsCircuit`	`Matroid.IsBasis` `Set` `Set.instMembership` `Set.instSDiff` `Set.instSingletonSet`	—	`Set.exists_of_ssubset` `HasSubset.Subset.ssubset_of_ne` `Set.instIsNonstrictStrictOrderSubsetSSubset` `Set.instAntisymmSubset` `Matroid.IsBasis.subset` `Matroid.Dep.not_indep` `dep` `Matroid.IsBasis.indep` `Matroid.IsBasis.eq_of_subset_indep` `diff_singleton_indep` `Set.subset_diff_singleton` `Set.diff_subset` `diff_singleton_isBasis`
`isBasis_iff_insert_eq` 📖	mathematical	`Matroid.IsCircuit`	`Matroid.IsBasis` `Set` `Set.instMembership` `Set.instSDiff` `Set.instInsert`	—	`isBasis_iff_eq_diff_singleton` `Eq.subset` `Set.instReflSubset` `Set.insert_diff_singleton` `Set.insert_eq_of_mem` `Set.insert_diff_self_of_notMem`
`isCircuit_restrict_of_subset` 📖	mathematical	`Matroid.IsCircuit` `Set` `Set.instHasSubset`	`Matroid.restrict`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset`
`isCocircuit` 📖	mathematical	`Matroid.IsCircuit`	`Matroid.IsCocircuit` `Matroid.dual`	—	`Matroid.isCocircuit_def` `Matroid.dual_dual`
`isCocircuit_disjoint_or_nontrivial_inter` 📖	mathematical	`Matroid.IsCircuit` `Matroid.IsCocircuit`	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.Nontrivial` `Set.instInter`	—	`Set.disjoint_iff_inter_eq_empty` `Set.nonempty_iff_ne_empty` `isCocircuit_inter_nontrivial`
`isCocircuit_inter_nontrivial` 📖	mathematical	`Matroid.IsCircuit` `Matroid.IsCocircuit` `Set.Nonempty` `Set` `Set.instInter`	`Set.Nontrivial`	—	`Set.nontrivial_iff_ne_singleton` `inter_isCocircuit_ne_singleton`
`mem_closure_diff_singleton_of_mem` 📖	mathematical	`Matroid.IsCircuit` `Set` `Set.instMembership`	`Matroid.closure` `Set.instSDiff` `Set.instSingletonSet`	—	`subset_closure_diff_singleton`
`minimal` 📖	mathematical	`Matroid.IsCircuit`	`Minimal` `Set` `Set.instLE` `Matroid.Dep`	—	—
`minimal_not_indep` 📖	mathematical	`Matroid.IsCircuit`	`Minimal` `Set` `Set.instLE` `Matroid.Indep`	—	`not_indep` `ssubset_indep`
`nonempty` 📖	mathematical	`Matroid.IsCircuit`	`Set.Nonempty`	—	`Matroid.Dep.nonempty` `dep`
`not_indep` 📖	mathematical	`Matroid.IsCircuit`	`Matroid.Indep`	—	`Matroid.Dep.not_indep` `dep`
`not_ssubset` 📖	mathematical	`Matroid.IsCircuit`	`Set` `Set.instHasSSubset`	—	`HasSSubset.SSubset.ne` `Set.instIrreflSSubset` `eq_of_dep_subset` `dep` `HasSSubset.SSubset.subset` `Set.instIsNonstrictStrictOrderSubsetSSubset`
`ssubset_indep` 📖	mathematical	`Matroid.IsCircuit` `Set` `Set.instHasSSubset`	`Matroid.Indep`	—	`Matroid.not_dep_iff` `HasSubset.Subset.trans` `Set.instIsTransSubset` `HasSSubset.SSubset.subset` `Set.instIsNonstrictStrictOrderSubsetSSubset` `subset_ground` `HasSSubset.SSubset.ne` `Set.instIrreflSSubset` `Matroid.isCircuit_iff`
`strong_elimination` 📖	mathematical	`Matroid.IsCircuit` `Set` `Set.instMembership`	`Set.instHasSubset` `Set.instSDiff` `Set.instUnion` `Set.instSingletonSet`	—	`strong_multi_elimination` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.diff_subset_diff` `Set.range_const` `Set.instReflSubset`
`strong_multi_elimination` 📖	mathematical	`Matroid.IsCircuit` `Set` `Set.instMembership`	`Set.instHasSubset` `Set.instSDiff` `Set.instUnion` `Set.iUnion` `Set.range`	—	`strong_multi_elimination_insert` `Set.insert_diff_singleton` `Set.insert_eq_of_mem` `Set.diff_union_self` `Set.union_eq_self_of_subset_right` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.union_subset` `Set.diff_subset_diff_left` `Set.subset_union_left` `Set.iUnion_subset` `Set.subset_diff` `Set.diff_subset` `Set.subset_union_of_subset_right` `Set.subset_iUnion` `Set.disjoint_iff_forall_ne`
`strong_multi_elimination_insert` 📖	mathematical	`Set` `Set.instMembership` `Matroid.IsCircuit` `Set.instInsert` `Set.instUnion` `Set.range`	`Set.instHasSubset` `Set.iUnion`	—	`isEmpty_or_nonempty` `Set.iUnion_of_empty` `Set.union_empty` `Set.instReflSubset` `Set.range_eq_empty` `Set.insert_diff_of_mem` `Set.diff_singleton_eq_self` `closure_diff_singleton_eq` `Matroid.closure_union_congr_left` `Matroid.closure_iUnion_congr` `Set.iUnion_insert_eq_range_union_iUnion` `Set.union_right_comm` `Set.mem_of_mem_of_subset` `mem_closure_diff_singleton_of_mem` `Matroid.closure_subset_closure` `subset_trans` `Set.instIsTransSubset` `Set.union_diff_distrib` `Set.union_comm` `Set.union_subset_union_left` `Set.diff_subset` `Set.subset_union_left` `Matroid.mem_closure_iff_exists_isCircuit` `Set.insert_eq_of_mem` `Set.insert_diff_singleton` `Set.insert_union`
`strong_multi_elimination_set` 📖	mathematical	`Matroid.IsCircuit` `Set` `Set.instHasSubset` `Set.instMembership` `Set.instInter` `Set.instSingletonSet`	`Set.instSDiff` `Set.instUnion` `Set.sUnion`	—	`strong_multi_elimination` `Set.singleton_subset_iff` `Set.subset_inter` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.diff_subset_diff` `Set.union_subset_union_right` `Set.iUnion_coe_set` `Set.iUnion_congr_Prop` `Set.subset_sUnion_of_mem` `Subtype.range_coe_subtype` `Set.instReflSubset` `Function.sometimes_spec`
`subset_closure_diff_singleton` 📖	mathematical	`Matroid.IsCircuit`	`Set` `Set.instHasSubset` `Matroid.closure` `Set.instSDiff` `Set.instSingletonSet`	—	`closure_diff_singleton_eq` `Matroid.subset_closure` `subset_ground`
`subset_ground` 📖	mathematical	`Matroid.IsCircuit`	`Set` `Set.instHasSubset` `Matroid.E`	—	`Matroid.Dep.subset_ground` `dep`

Matroid.IsCocircuit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCircuit` 📖	mathematical	`Matroid.IsCocircuit`	`Matroid.IsCircuit` `Matroid.dual`	—	—
`nonempty` 📖	mathematical	`Matroid.IsCocircuit`	`Set.Nonempty`	—	`Matroid.IsCircuit.nonempty` `isCircuit`
`subset_ground` 📖	mathematical	`Matroid.IsCocircuit`	`Set` `Set.instHasSubset` `Matroid.E`	—	`Matroid.IsCircuit.subset_ground` `isCircuit`

---

← Back to Index