Closure

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

Statistics

Metric	Count
Definitions `IsFlat`, `Spanning`, `closure`, `subtypeClosure`	4
Theorems `closure_compl`, `compl_spanning`, `closure_diff_singleton_ssubset`, `closure_diff_ssubset`, `closure_eq_setOf_isBasis_insert`, `closure_iInter_eq_biInter_closure_of_forall_subset`, `closure_insert_diff_eq_of_mem_closure`, `closure_inter_eq_inter_closure`, `closure_inter_eq_self_of_subset`, `closure_sInter_eq_biInter_closure_of_forall_subset`, `closure_ssubset_closure`, `eq_of_spanning_subset`, `exists_isBase_subset_spanning`, `indep_insert_diff_of_mem_closure`, `insert_dep_iff`, `insert_diff_indep_iff`, `insert_indep_iff`, `insert_indep_iff_of_notMem`, `insert_isBasis_iff_mem_closure`, `inter_isBasis_biInter`, `inter_isBasis_closure_iff_subset_closure_inter`, `inter_isBasis_iInter`, `inter_isBasis_sInter`, `isBase_iff_ground_subset_closure`, `isBase_of_ground_subset_closure`, `isBase_of_spanning`, `isBasis_closure`, `isBasis_of_subset_of_subset_closure`, `mem_closure_iff`, `mem_closure_iff'`, `mem_closure_iff_of_notMem`, `notMem_closure_diff_of_mem`, `notMem_closure_iff`, `notMem_closure_iff_of_notMem`, `union_indep_iff_forall_notMem_closure_left`, `union_indep_iff_forall_notMem_closure_right`, `closure_eq`, `closure_of_superset`, `eq_of_superset_spanning`, `exchange_base_of_notMem_closure`, `isBase_insert_diff_of_mem_closure`, `spanning`, `spanning_of_superset`, `closure_eq_closure`, `isBasis_closure_right`, `closure_eq_closure`, `closure_eq_right`, `closure_inter_isBasis_closure`, `eq_of_closure_subset`, `insert_isBasis_insert_of_notMem_closure`, `isBase_of_spanning`, `isBasis_closure_right`, `isBasis_insert_diff_of_mem_closure`, `isBasis_of_closure_eq_closure`, `spanning_iff_spanning`, `subset_closure`, `closure`, `iInter`, `subset_ground`, `subset_of_isBasis_of_isBasis`, `isBase_iff_of_spanning`, `closure_eq`, `closure_eq_of_superset`, `compl_coindep`, `exists_isBase_subset`, `isBase_of_indep`, `isBase_of_minimal`, `isBase_restrict_iff`, `subset_ground`, `superset`, `union_left`, `union_right`, `closure_biInter_eq_biInter_closure_of_biUnion_indep`, `closure_biUnion_closure_eq_closure_biUnion`, `closure_biUnion_closure_eq_closure_sUnion`, `closure_biUnion_congr`, `closure_closure`, `closure_closure_union_closure_eq_closure_union`, `closure_def`, `closure_def'`, `closure_diff_eq_self`, `closure_diff_singleton_eq_closure`, `closure_empty_eq_ground_iff`, `closure_empty_union_closure_eq`, `closure_eq_subtypeClosure`, `closure_exchange`, `closure_exchange_iff`, `closure_ground`, `closure_iInter_eq_iInter_closure_of_iUnion_indep`, `closure_iUnion_closure_eq_closure_iUnion`, `closure_iUnion_congr`, `closure_insert_closure_eq_closure_insert`, `closure_insert_congr`, `closure_insert_congr_right`, `closure_insert_eq_of_mem_closure`, `closure_inter_ground`, `closure_mono`, `closure_sInter_eq_biInter_closure_of_sUnion_indep`, `closure_spanning_iff`, `closure_subset_closure`, `closure_subset_closure_iff_subset_closure`, `closure_subset_closure_of_subset_closure`, `closure_subset_ground`, `closure_union_closure_empty_eq`, `closure_union_closure_left_eq`, `closure_union_closure_right_eq`, `closure_union_congr_left`, `closure_union_congr_right`, `closure_univ`, `coindep_iff_closure_compl_eq_ground`, `coindep_iff_compl_spanning`, `comap_closure_eq`, `emptyOn_closure_eq`, `empty_isBasis_iff`, `exists_isBasis_inter_ground_isBasis_closure`, `exists_of_closure_ssubset`, `ext_closure`, `ext_spanning`, `freeOn_closure_eq`, `ground_isFlat`, `ground_spanning`, `ground_subset_closure_iff`, `indep_iff_forall_closure_diff_ne`, `indep_iff_forall_closure_ssubset_of_ssubset`, `indep_iff_forall_notMem_closure_diff`, `indep_iff_forall_notMem_closure_diff'`, `insert_indep_iff`, `instNonemptyElemSetSetOfAndIsFlatSubsetInterE`, `inter_ground_subset_closure`, `isBase_iff_indep_closure_eq`, `isBase_iff_minimal_spanning`, `isBasis'_iff_isBasis_closure`, `isBasis_iff_indep_closure`, `isBasis_iff_indep_subset_closure`, `isBasis_iff_isBasis_closure_of_subset`, `isBasis_iff_isBasis_closure_of_subset'`, `isBasis_union_iff_indep_closure`, `isClosed_iff_isFlat`, `isFlat_closure`, `isFlat_iff`, `isFlat_iff_closure_eq`, `isFlat_iff_isClosed`, `loopyOn_closure_eq`, `loopyOn_spanning_iff`, `map_closure_eq`, `mem_closure_diff_singleton_iff_closure`, `mem_closure_iff_forall_mem_isFlat`, `mem_closure_insert`, `mem_closure_of_mem`, `mem_closure_of_mem'`, `mem_closure_self`, `mem_ground_of_mem_closure`, `notMem_of_mem_diff_closure`, `not_spanning_iff_closure_ssubset`, `restrict_closure_eq`, `restrict_closure_eq'`, `restrict_spanning_iff`, `restrict_spanning_iff'`, `spanning_iff`, `spanning_iff_closure_eq`, `spanning_iff_compl_coindep`, `spanning_iff_exists_isBase_subset`, `spanning_iff_exists_isBase_subset'`, `spanning_iff_ground_subset_closure`, `subset_closure`, `subset_closure_diff_iff_closure_eq`, `subset_closure_iff_forall_subset_isFlat`, `subset_closure_of_subset`, `subset_closure_of_subset'`, `uniqueBaseOn_closure_eq`	170
Total	174

Matroid

Definitions

Name	Category	Theorems
`IsFlat` 📖	CompData	11 math math: `instNonemptyElemSetSetOfAndIsFlatSubsetInterE`, `AlgebraicIndependent.matroid_isFlat_of_subsingleton`, `isClosed_iff_isFlat`, `isFlat_closure`, `isFlat_iff_closure_eq`, `ground_isFlat`, `closure_def'`, `closure_def`, `AlgebraicIndependent.matroid_isFlat_iff`, `isFlat_iff_isClosed`, `isFlat_iff`
`Spanning` 📖	CompData	30 math math: `isCocircuit_iff_minimal_compl_nonspanning`, `loopyOn_spanning_iff`, `spanning_iff_compl_coindep`, `Coindep.compl_spanning`, `IsBase.spanning_of_superset`, `isColoop_iff_diff_not_spanning`, `spanning_iff_exists_isBase_subset`, `not_spanning_iff_closure_ssubset`, `AlgebraicIndependent.matroid_spanning_iff`, `Coindep.delete_spanning_iff`, `IsBasis.spanning_iff_spanning`, `restrict_spanning_iff`, `IsBase.spanning`, `AlgebraicIndependent.matroid_spanning_iff_of_subsingleton`, `spanning_iff_eRk_le'`, `closure_spanning_iff`, `restrict_spanning_iff'`, `spanning_iff`, `contract_spanning_iff`, `spanning_iff_closure_eq`, `spanning_iff_exists_isBase_subset'`, `isColoop_tfae`, `contract_spanning_iff'`, `isBase_iff_minimal_spanning`, `ground_spanning`, `isCocircuit_iff_minimal_compl_nonspanning'`, `spanning_iff_ground_subset_closure`, `coindep_iff_compl_spanning`, `spanning_iff_eRk_le`, `IsColoop.diff_not_spanning`
`closure` 📖	CompOp	165 math math: `eRk_insert_closure_eq`, `exists_isBasis_inter_ground_isBasis_closure`, `cRk_union_closure_left_eq`, `Indep.mem_closure_iff`, `IsBasis'.closure_eq_closure`, `Indep.mem_closure_iff'`, `closure_subset_closure_iff_subset_closure`, `IsCircuit.mem_closure_diff_singleton_of_mem`, `isBasis_iff_isBasis_closure_of_subset`, `isRkFinite_closure_iff`, `inter_ground_subset_closure`, `closure_iUnion_closure_eq_closure_iUnion`, `isColoop_iff_forall_mem_closure_iff_mem`, `IsRkFinite.closure_eq_closure_of_subset_of_forall_insert`, `IsNonloop.closure_eq_closure_iff_eq_or_dep`, `IsCircuit.closure_diff_singleton_eq`, `coindep_iff_closure_compl_eq_ground`, `closure_biInter_eq_biInter_closure_of_biUnion_indep`, `subset_closure_diff_iff_closure_eq`, `insert_indep_iff`, `closure_univ`, `isLoop_tfae`, `isColoop_iff_forall_mem_closure_iff_mem'`, `not_spanning_iff_closure_ssubset`, `closure_subset_ground`, `closure_empty`, `Indep.isBasis_closure`, `eRk_union_closure_left_eq`, `closure_loops`, `contract_isNonloop_iff`, `restrict_spanning_iff`, `closure_insert_closure_eq_closure_insert`, `subset_closure_iff_forall_subset_isFlat`, `restrict_closure_eq`, `closure_eq_loops_of_subset`, `delete_closure_eq`, `cRk_closure`, `closure_loops_union_eq`, `isBasis_iff_indep_subset_closure`, `closure_eq_subtypeClosure`, `closure_union_coloops_eq`, `closure_inter_setOf_isNonloop_eq`, `closure_mono`, `Indep.union_indep_iff_forall_notMem_closure_left`, `closure_spanning_iff`, `Spanning.closure_eq`, `restrict_spanning_iff'`, `emptyOn_closure_eq`, `contract_closure_eq`, `Indep.insert_indep_iff`, `closure_union_closure_left_eq`, `restrict_isColoop_iff`, `subset_closure`, `Indep.notMem_closure_iff`, `spanning_iff`, `isFlat_closure`, `isFlat_iff_closure_eq`, `closure_union_eq_of_subset_coloops`, `Indep.closure_diff_singleton_ssubset`, `IsBase.compl_closure_diff_singleton_isCocircuit`, `indep_iff_forall_closure_ssubset_of_ssubset`, `mem_closure_of_mem'`, `cRk_union_closure_eq`, `closure_closure`, `Indep.closure_eq_setOf_isBasis_insert`, `IsBase.closure_eq`, `closure_disjoint_of_disjoint_of_subset_coloops`, `comap_closure_eq`, `closure_insert_isColoop_eq`, `closure_union_closure_empty_eq`, `Indep.closure_diff_ssubset`, `delete_closure_eq_of_disjoint`, `cRk_insert_closure_eq`, `Indep.insert_dep_iff`, `closure_ground`, `Indep.insert_isBasis_iff_mem_closure`, `closure_union_closure_right_eq`, `closure_inter_eq_of_subset_coloops`, `isLoop_iff_closure_eq_loops`, `closure_subset_closure`, `closure_def'`, `closure_iInter_eq_iInter_closure_of_iUnion_indep`, `IsLoop.closure`, `IsBasis.isBasis_closure_right`, `subset_closure_of_subset`, `IsBasis.closure_inter_isBasis_closure`, `closure_def`, `contract_loops_eq`, `mem_closure_self`, `closure_union_loops_eq`, `map_closure_eq`, `closure_exchange_iff`, `eRk_eq_one_iff`, `closure_diff_eq_of_subset_coloops`, `indep_iff_forall_notMem_closure_diff'`, `Indep.notMem_closure_diff_of_mem`, `Indep.closure_iInter_eq_biInter_closure_of_forall_subset`, `freeOn_closure_eq`, `IsColoop.notMem_closure_of_notMem`, `closure_diff_loops_eq`, `Indep.closure_inter_eq_self_of_subset`, `ground_subset_closure_iff`, `spanning_iff_closure_eq`, `mem_closure_of_mem`, `closure_inter_ground`, `IsRkFinite.closure`, `Spanning.closure_eq_of_superset`, `Indep.notMem_closure_iff_of_notMem`, `delete_isColoop_iff`, `eRk_union_closure_right_eq`, `mem_closure_iff_forall_mem_isFlat`, `loopyOn_closure_eq`, `Indep.mem_closure_iff_of_notMem`, `isBase_iff_indep_closure_eq`, `IsNonloop.mem_closure_comm`, `isColoop_iff_notMem_closure_compl`, `Indep.isBase_iff_ground_subset_closure`, `contract_closure_eq_contract_delete`, `Indep.inter_isBasis_closure_iff_subset_closure_inter`, `IsNonloop.closure_eq_closure_iff_isCircuit_of_ne`, `restrict_closure_eq'`, `closure_empty_eq_ground_iff`, `AlgebraicIndependent.matroid_closure_eq`, `Coindep.closure_compl`, `Indep.closure_ssubset_closure`, `IsBase.closure_of_superset`, `isBasis_iff_isBasis_closure_of_subset'`, `empty_isBasis_iff`, `IsRkFinite.closure_eq_closure_of_subset_of_eRk_ge_eRk`, `closure_disjoint_coloops_of_disjoint_coloops`, `Indep.insert_diff_indep_iff`, `isBasis_union_iff_indep_closure`, `indep_iff_forall_notMem_closure_diff`, `closure_inter_coloops_eq`, `IsLoop.mem_closure`, `Indep.union_indep_iff_forall_notMem_closure_right`, `eRk_le_one_iff`, `AlgebraicIndependent.matroid_closure_of_subsingleton`, `closure_closure_union_closure_eq_closure_union`, `isBasis'_iff_isBasis_closure`, `spanning_iff_ground_subset_closure`, `IsBasis.subset_closure`, `IsCircuit.subset_closure_diff_singleton`, `subset_closure_of_subset'`, `closure_biUnion_closure_eq_closure_biUnion`, `cRk_union_closure_right_eq`, `closure_sInter_eq_biInter_closure_of_sUnion_indep`, `isBasis_iff_indep_closure`, `isLoop_iff_closure_eq_loops_and_mem_ground`, `IsColoop.mem_closure_iff_mem`, `IsFlat.closure`, `Indep.closure_inter_eq_inter_closure`, `uniqueBaseOn_closure_eq`, `mem_closure_iff_exists_isCircuit`, `not_isNonloop_iff_closure`, `Indep.closure_sInter_eq_biInter_closure_of_forall_subset`, `contract_isLoop_iff_mem_closure`, `closure_biUnion_closure_eq_closure_sUnion`, `eRk_closure_eq`, `closure_empty_union_closure_eq`, `IsBasis'.isBasis_closure_right`, `mem_closure_diff_singleton_iff_closure`, `IsBasis.closure_eq_closure`, `closure_eq_of_subset_coloops`, `Indep.insert_indep_iff_of_notMem`
`subtypeClosure` 📖	CompOp	3 math math: `isClosed_iff_isFlat`, `closure_eq_subtypeClosure`, `isFlat_iff_isClosed`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_biInter_eq_biInter_closure_of_biUnion_indep` 📖	mathematical	`Set.Nonempty` `Indep` `Set.iUnion` `Set` `Set.instMembership`	`closure` `Set.iInter`	—	`Set.Nonempty.coe_sort` `Set.iInter_coe_set` `Set.iInter_congr_Prop` `closure_iInter_eq_iInter_closure_of_iUnion_indep` `Set.iUnion_coe_set` `Set.iUnion_congr_Prop`
`closure_biUnion_closure_eq_closure_biUnion` 📖	mathematical	—	`closure` `Set.iUnion` `Set` `Set.instMembership`	—	`Set.biUnion_eq_iUnion` `closure_iUnion_closure_eq_closure_iUnion`
`closure_biUnion_closure_eq_closure_sUnion` 📖	mathematical	—	`closure` `Set.iUnion` `Set` `Set.instMembership` `Set.sUnion`	—	`Set.sUnion_eq_iUnion` `Set.biUnion_eq_iUnion` `closure_iUnion_closure_eq_closure_iUnion`
`closure_biUnion_congr` 📖	mathematical	`closure`	`Set.iUnion` `Set` `Set.instMembership`	—	`closure_biUnion_closure_eq_closure_biUnion` `Set.iUnion₂_congr`
`closure_closure` 📖	mathematical	—	`closure`	—	`HasSubset.Subset.antisymm'` `Set.instAntisymmSubset` `subset_closure` `closure_subset_ground` `Set.subset_sInter` `HasSubset.Subset.trans` `Set.instIsTransSubset` `closure_subset_closure` `Set.sInter_subset_of_mem` `Eq.subset` `Set.instReflSubset` `IsFlat.closure`
`closure_closure_union_closure_eq_closure_union` 📖	mathematical	—	`closure` `Set` `Set.instUnion`	—	`Set.union_eq_iUnion` `closure_iUnion_closure_eq_closure_iUnion`
`closure_def` 📖	mathematical	—	`closure` `Set.sInter` `setOf` `Set` `IsFlat` `Set.instHasSubset` `Set.instInter` `E`	—	—
`closure_def'` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`closure` `Set.sInter` `setOf` `IsFlat`	—	`closure.eq_1` `Set.inter_eq_self_of_subset_left`
`closure_diff_eq_self` 📖	—	`Set` `Set.instHasSubset` `closure` `Set.instSDiff`	—	—	`Set.diff_union_inter` `closure_union_closure_left_eq` `Set.union_eq_self_of_subset_right` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.inter_subset_right` `closure_closure`
`closure_diff_singleton_eq_closure` 📖	—	`Set` `Set.instMembership` `closure` `Set.instSDiff` `Set.instSingletonSet`	—	—	`closure_diff_eq_self`
`closure_empty_eq_ground_iff` 📖	mathematical	—	`closure` `Set` `Set.instEmptyCollection` `E` `loopyOn`	—	`ext_closure` `subset_antisymm` `Set.instAntisymmSubset` `loopyOn_closure_eq` `closure_mono` `Set.empty_subset` `loopyOn_ground`
`closure_empty_union_closure_eq` 📖	mathematical	—	`Set` `Set.instUnion` `closure` `Set.instEmptyCollection`	—	`Set.union_eq_self_of_subset_left` `closure_subset_closure` `Set.empty_subset`
`closure_eq_subtypeClosure` 📖	mathematical	—	`closure` `Set` `Set.instMembership` `Set.Iic` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `E` `DFunLike.coe` `ClosureOperator` `Set.Elem` `Subtype.preorder` `ClosureOperator.instFunLike` `subtypeClosure` `Set.instInter` `Set.inter_subset_right`	—	`ground_isFlat` `Set.inter_subset_right` `IsFlat.subset_ground` `Set.Iic.coe_iInf`
`closure_exchange` 📖	—	`Set` `Set.instMembership` `Set.instSDiff` `closure` `Set.instInsert`	—	—	`mem_closure_insert` `Set.notMem_empty` `Set.diff_self` `closure_insert_eq_of_mem_closure`
`closure_exchange_iff` 📖	mathematical	—	`Set` `Set.instMembership` `Set.instSDiff` `closure` `Set.instInsert`	—	`closure_exchange`
`closure_ground` 📖	mathematical	—	`closure` `E`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `closure_subset_ground` `subset_closure` `Set.instReflSubset`
`closure_iInter_eq_iInter_closure_of_iUnion_indep` 📖	mathematical	`Indep` `Set.iUnion`	`closure` `Set.iInter`	—	`Set.iInter_congr_Prop` `Set.iInter_exists` `Set.iInter_iInter_eq'` `Indep.closure_sInter_eq_biInter_closure_of_forall_subset` `Set.range_nonempty`
`closure_iUnion_closure_eq_closure_iUnion` 📖	mathematical	—	`closure` `Set.iUnion`	—	`Set.inter_subset_right` `closure_eq_subtypeClosure` `Set.iUnion_inter` `Set.Iic.coe_iInf` `Set.Iic.coe_iSup` `ClosureOperator.closure_iSup_closure`
`closure_iUnion_congr` 📖	mathematical	`closure`	`Set.iUnion`	—	`closure_iUnion_closure_eq_closure_iUnion` `closure_closure`
`closure_insert_closure_eq_closure_insert` 📖	mathematical	—	`closure` `Set` `Set.instInsert`	—	`closure_union_closure_right_eq`
`closure_insert_congr` 📖	—	`Set` `Set.instMembership` `Set.instSDiff` `closure` `Set.instInsert`	—	—	`closure_exchange` `closure_closure` `Set.insert_eq_of_mem` `closure_insert_closure_eq_closure_insert` `Set.insert_comm`
`closure_insert_congr_right` 📖	mathematical	`closure`	`Set` `Set.instInsert`	—	`closure_union_congr_left`
`closure_insert_eq_of_mem_closure` 📖	mathematical	`Set` `Set.instMembership` `closure`	`Set.instInsert`	—	`closure_insert_closure_eq_closure_insert` `Set.insert_eq_of_mem` `closure_closure`
`closure_inter_ground` 📖	mathematical	—	`closure` `Set` `Set.instInter` `E`	—	`Set.inter_assoc` `Set.inter_self`
`closure_mono` 📖	mathematical	—	`Monotone` `Set` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `closure`	—	`closure_subset_closure`
`closure_sInter_eq_biInter_closure_of_sUnion_indep` 📖	mathematical	`Set.Nonempty` `Set` `Indep` `Set.sUnion`	`closure` `Set.sInter` `Set.iInter` `Set.instMembership`	—	`Indep.closure_sInter_eq_biInter_closure_of_forall_subset` `Set.subset_sUnion_of_mem`
`closure_spanning_iff` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`Spanning` `closure`	—	`spanning_iff_closure_eq` `closure_subset_ground` `closure_closure`
`closure_subset_closure` 📖	mathematical	`Set` `Set.instHasSubset`	`closure`	—	`Set.subset_sInter` `Set.sInter_subset_of_mem` `subset_trans` `Set.instIsTransSubset` `Set.inter_subset_inter_left`
`closure_subset_closure_iff_subset_closure` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`closure`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure` `closure_subset_closure_of_subset_closure`
`closure_subset_closure_of_subset_closure` 📖	—	`Set` `Set.instHasSubset` `closure`	—	—	`LE.le.trans_eq` `closure_subset_closure` `closure_closure`
`closure_subset_ground` 📖	mathematical	—	`Set` `Set.instHasSubset` `closure` `E`	—	`Set.sInter_subset_of_mem` `ground_isFlat` `Set.inter_subset_right`
`closure_union_closure_empty_eq` 📖	mathematical	—	`Set` `Set.instUnion` `closure` `Set.instEmptyCollection`	—	`Set.union_eq_self_of_subset_right` `closure_subset_closure` `Set.empty_subset`
`closure_union_closure_left_eq` 📖	mathematical	—	`closure` `Set` `Set.instUnion`	—	`closure_closure_union_closure_eq_closure_union` `closure_closure`
`closure_union_closure_right_eq` 📖	mathematical	—	`closure` `Set` `Set.instUnion`	—	`closure_closure_union_closure_eq_closure_union` `closure_closure`
`closure_union_congr_left` 📖	mathematical	`closure`	`Set` `Set.instUnion`	—	`closure_union_closure_left_eq`
`closure_union_congr_right` 📖	mathematical	`closure`	`Set` `Set.instUnion`	—	`closure_union_closure_right_eq`
`closure_univ` 📖	mathematical	—	`closure` `Set.univ` `E`	—	`closure_inter_ground` `Set.univ_inter` `closure_ground`
`coindep_iff_closure_compl_eq_ground` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`Coindep` `closure` `Set.instSDiff`	—	`coindep_iff_compl_spanning` `spanning_iff_closure_eq`
`coindep_iff_compl_spanning` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`Coindep` `Spanning` `Set.instSDiff`	—	`coindep_iff_exists` `spanning_iff_exists_isBase_subset`
`comap_closure_eq` 📖	mathematical	—	`closure` `comap` `Set.preimage` `Set.image`	—	`exists_isBasis'` `comap_isBasis'_iff` `IsBasis'.closure_eq_closure` `Indep.mem_closure_iff'` `IsBasis'.indep` `Set.insert_eq_of_mem` `Set.injOn_insert`
`emptyOn_closure_eq` 📖	mathematical	—	`closure` `emptyOn` `Set` `Set.instEmptyCollection`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `closure_subset_ground` `Set.empty_subset`
`empty_isBasis_iff` 📖	mathematical	—	`IsBasis` `Set` `Set.instEmptyCollection` `Set.instHasSubset` `closure`	—	`isBasis_iff_indep_closure` `empty_indep` `Set.empty_subset`
`exists_isBasis_inter_ground_isBasis_closure` 📖	mathematical	—	`IsBasis` `Set` `Set.instInter` `E` `closure`	—	`exists_isBasis` `IsBasis.isBasis_closure_right` `closure_inter_ground`
`exists_of_closure_ssubset` 📖	mathematical	`Set` `Set.instHasSSubset` `closure`	`Set.instMembership`	—	`HasSSubset.SSubset.not_subset` `Set.instIsNonstrictStrictOrderSubsetSSubset` `closure_subset_closure_of_subset_closure` `Mathlib.Tactic.Push.not_and_eq`
`ext_closure` 📖	—	`closure`	—	—	`ext_indep` `closure_univ`
`ext_spanning` 📖	—	`E` `Spanning`	—	—	`em` `Spanning.subset_ground` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Eq.subset` `Set.instReflSubset` `ext_iff_indep` `dual_ground` `coindep_def` `coindep_iff_compl_spanning`
`freeOn_closure_eq` 📖	mathematical	—	`closure` `freeOn` `Set` `Set.instInter`	—	`closure_inter_ground` `Indep.mem_closure_iff'` `freeOn_indep` `Set.inter_subset_right`
`ground_isFlat` 📖	mathematical	—	`IsFlat` `E`	—	`IsBasis.subset_ground` `Set.Subset.rfl`
`ground_spanning` 📖	mathematical	—	`Spanning` `E`	—	`closure_ground` `Eq.subset` `Set.instReflSubset`
`ground_subset_closure_iff` 📖	mathematical	—	`Set` `Set.instHasSubset` `E` `closure`	—	`Set.instReflSubset` `Set.instAntisymmSubset` `closure_subset_ground`
`indep_iff_forall_closure_diff_ne` 📖	mathematical	—	`Indep`	—	`indep_iff_forall_notMem_closure_diff'` `Eq.subset` `Set.instReflSubset` `mem_closure_of_mem` `by_contra` `closure_inter_ground` `Set.inter_comm` `Set.inter_diff_distrib_left` `Set.inter_singleton_eq_empty` `Set.diff_empty` `Set.insert_diff_self_of_mem` `closure_insert_closure_eq_closure_insert` `Set.insert_eq_of_mem` `closure_closure`
`indep_iff_forall_closure_ssubset_of_ssubset` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`Indep` `Set.instHasSSubset` `closure`	—	`Indep.closure_ssubset_closure` `indep_iff_forall_notMem_closure_diff` `HasSSubset.SSubset.ne` `Set.instIrreflSSubset` `Set.diff_singleton_ssubset` `Set.insert_diff_self_of_mem` `closure_insert_closure_eq_closure_insert` `Set.insert_eq_of_mem` `Set.insert_diff_singleton` `Set.insert_diff_of_mem` `closure_closure`
`indep_iff_forall_notMem_closure_diff` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`Indep` `Set.instMembership` `closure` `Set.instSDiff` `Set.instSingletonSet`	—	`Eq.subset` `Set.instReflSubset` `Indep.closure_inter_eq_self_of_subset` `Set.diff_subset` `exists_isBasis` `HasSubset.Subset.antisymm'` `Set.instAntisymmSubset` `IsBasis.subset` `by_contra` `Set.mem_of_mem_of_subset` `IsBasis.subset_closure` `closure_subset_closure` `Set.subset_diff_singleton` `IsBasis.indep`
`indep_iff_forall_notMem_closure_diff'` 📖	mathematical	—	`Indep` `Set` `Set.instHasSubset` `E` `Set.instMembership` `closure` `Set.instSDiff` `Set.instSingletonSet`	—	`Indep.subset_ground` `indep_iff_forall_notMem_closure_diff`
`insert_indep_iff` 📖	mathematical	—	`Indep` `Set` `Set.instInsert` `Set.instMembership` `Set.instSDiff` `E` `closure`	—	`Indep.insert_indep_iff` `Indep.subset` `Set.subset_insert`
`instNonemptyElemSetSetOfAndIsFlatSubsetInterE` 📖	mathematical	—	`Set.Elem` `Set` `setOf` `IsFlat` `Set.instHasSubset` `Set.instInter` `E`	—	`ground_isFlat` `Set.inter_subset_right`
`inter_ground_subset_closure` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.instInter` `E` `closure`	—	—
`isBase_iff_indep_closure_eq` 📖	mathematical	—	`IsBase` `Indep` `closure` `E`	—	`isBasis_ground_iff` `isBasis_iff_indep_subset_closure` `HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `closure_subset_ground` `LE.le.trans_eq` `subset_closure` `Indep.subset_ground` `Eq.subset` `Set.instReflSubset`
`isBase_iff_minimal_spanning` 📖	mathematical	—	`IsBase` `Minimal` `Set` `Set.instLE` `Spanning`	—	`minimal_subset_iff` `IsBase.spanning` `IsBase.eq_of_superset_spanning` `Spanning.exists_isBase_subset`
`isBasis'_iff_isBasis_closure` 📖	mathematical	—	`IsBasis'` `IsBasis` `closure` `Set` `Set.instHasSubset`	—	`closure_inter_ground` `isBasis'_iff_isBasis_inter_ground` `IsBasis.isBasis_closure_right` `HasSubset.Subset.trans` `Set.instIsTransSubset` `IsBasis.subset` `Set.inter_subset_left` `IsBasis.isBasis_subset` `Set.subset_inter` `Indep.subset_ground` `IsBasis.indep` `subset_closure`
`isBasis_iff_indep_closure` 📖	mathematical	—	`IsBasis` `Indep` `Set` `Set.instHasSubset` `closure`	—	`IsBasis.indep` `IsBasis.subset_closure` `IsBasis.subset` `IsBasis.isBasis_subset` `isBasis_union_iff_indep_closure` `Set.subset_union_right`
`isBasis_iff_indep_subset_closure` 📖	mathematical	—	`IsBasis` `Indep` `Set` `Set.instHasSubset` `closure`	—	`IsBasis.indep` `IsBasis.subset` `IsBasis.subset_closure` `Indep.isBasis_of_subset_of_subset_closure`
`isBasis_iff_isBasis_closure_of_subset` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`IsBasis` `closure`	—	`IsBasis.isBasis_closure_right` `IsBasis.isBasis_subset` `subset_closure`
`isBasis_iff_isBasis_closure_of_subset'` 📖	mathematical	`Set` `Set.instHasSubset`	`IsBasis` `closure` `E`	—	`IsBasis.isBasis_closure_right` `IsBasis.subset_ground` `IsBasis.isBasis_subset` `subset_closure`
`isBasis_union_iff_indep_closure` 📖	mathematical	—	`IsBasis` `Set` `Set.instUnion` `Indep` `Set.instHasSubset` `closure`	—	`IsBasis.indep` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.subset_union_right` `IsBasis.subset_closure` `IsBasis.isBasis_subset` `Indep.isBasis_closure` `Set.subset_union_left` `Set.union_subset` `subset_closure` `Indep.subset_ground`
`isClosed_iff_isFlat` 📖	mathematical	—	`ClosureOperator.IsClosed` `Set.Elem` `Set` `Set.Iic` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `E` `Subtype.preorder` `Set.instMembership` `subtypeClosure` `IsFlat`	—	—
`isFlat_closure` 📖	mathematical	—	`IsFlat` `closure`	—	`closure.eq_1` `Set.sInter_eq_iInter` `IsFlat.iInter` `instNonemptyElemSetSetOfAndIsFlatSubsetInterE`
`isFlat_iff` 📖	mathematical	—	`IsFlat` `Set` `Set.instHasSubset` `E`	—	—
`isFlat_iff_closure_eq` 📖	mathematical	—	`IsFlat` `closure`	—	`IsFlat.closure` `isFlat_closure`
`isFlat_iff_isClosed` 📖	mathematical	—	`IsFlat` `ClosureOperator.IsClosed` `Set.Elem` `Set` `Set.Iic` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `E` `Subtype.preorder` `Set.instMembership` `subtypeClosure`	—	`IsFlat.subset_ground`
`loopyOn_closure_eq` 📖	mathematical	—	`closure` `loopyOn`	—	`restrict_closure_eq'` `emptyOn_closure_eq` `Set.empty_inter` `Set.diff_empty` `Set.empty_union`
`loopyOn_spanning_iff` 📖	mathematical	—	`Spanning` `loopyOn` `Set` `Set.instHasSubset`	—	`spanning_iff` `loopyOn_closure_eq` `loopyOn_ground`
`map_closure_eq` 📖	mathematical	`Set.InjOn` `E`	`closure` `map` `Set.image` `Set.preimage`	—	`Set.ext` `Indep.mem_closure_iff'` `Indep.map` `Set.image_insert_eq` `Set.InjOn.eq_iff` `Indep.subset_ground` `map_image_indep_iff` `Set.insert_subset` `exists_isBasis` `closure_inter_ground` `map_ground` `IsBasis.closure_eq_closure` `IsBasis.indep` `Set.image_preimage_inter` `IsBasis.map`
`mem_closure_diff_singleton_iff_closure` 📖	mathematical	`Set` `Set.instMembership` `E`	`closure` `Set.instSDiff` `Set.instSingletonSet`	—	`subset_closure_diff_iff_closure_eq`
`mem_closure_iff_forall_mem_isFlat` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`Set.instMembership` `closure`	—	`closure_def'`
`mem_closure_insert` 📖	—	`Set` `Set.instMembership` `closure` `Set.instInsert`	—	—	`closure_inter_ground` `Set.insert_inter_of_notMem` `closure_subset_ground` `Set.insert_inter_of_mem` `exists_isBasis` `closure_insert_closure_eq_closure_insert` `IsBasis.closure_eq_closure` `Indep.mem_closure_iff` `Indep.notMem_closure_iff` `IsBasis.indep` `dep_iff` `Set.insert_comm` `Set.insert_subset` `Indep.subset_ground` `Set.mem_insert` `Set.mem_insert_iff` `Indep.not_dep` `Indep.subset` `Set.subset_insert`
`mem_closure_of_mem` 📖	mathematical	`Set` `Set.instMembership` `Set.instHasSubset` `E`	`closure`	—	`subset_closure`
`mem_closure_of_mem'` 📖	mathematical	`Set` `Set.instMembership` `E`	`closure`	—	`closure_inter_ground` `mem_closure_of_mem`
`mem_closure_self` 📖	mathematical	`Set` `Set.instMembership` `E`	`closure` `Set.instSingletonSet`	—	`mem_closure_of_mem'`
`mem_ground_of_mem_closure` 📖	mathematical	`Set` `Set.instMembership` `closure`	`E`	—	`closure_subset_ground`
`notMem_of_mem_diff_closure` 📖	—	`Set` `Set.instMembership` `Set.instSDiff` `E` `closure`	—	—	`mem_closure_of_mem'`
`not_spanning_iff_closure_ssubset` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`Spanning` `Set.instHasSSubset` `closure`	—	`spanning_iff_closure_eq` `ssubset_iff_subset_ne` `Set.instIsNonstrictStrictOrderSubsetSSubset` `Set.instAntisymmSubset` `closure_subset_ground`
`restrict_closure_eq` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`closure` `restrict` `Set.instInter`	—	`restrict_closure_eq'` `Set.diff_eq_empty` `Set.union_empty` `Set.inter_eq_self_of_subset_left`
`restrict_closure_eq'` 📖	mathematical	—	`closure` `restrict` `Set` `Set.instUnion` `Set.instInter` `Set.instSDiff` `E`	—	`exists_isBasis'` `isBasis'_restrict_iff` `Set.ext` `IsBasis'.closure_eq_closure` `Indep.mem_closure_iff'` `IsBasis'.indep` `Set.mem_union` `Set.mem_inter_iff` `restrict_ground_eq` `restrict_indep_iff` `Set.mem_diff` `Indep.subset_ground` `Set.mem_insert`
`restrict_spanning_iff` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`Spanning` `restrict` `closure`	—	`spanning_iff` `restrict_ground_eq` `restrict_closure_eq` `Set.inter_eq_right`
`restrict_spanning_iff'` 📖	mathematical	—	`Spanning` `restrict` `Set` `Set.instHasSubset` `Set.instInter` `E` `closure`	—	`spanning_iff` `restrict_closure_eq'` `restrict_ground_eq` `Set.diff_eq_compl_inter` `Set.union_inter_distrib_right` `Set.inter_eq_right` `Set.union_comm` `Set.diff_subset_iff` `Set.diff_compl` `Set.inter_eq_self_of_subset_left`
`spanning_iff` 📖	mathematical	—	`Spanning` `closure` `E` `Set` `Set.instHasSubset`	—	—
`spanning_iff_closure_eq` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`Spanning` `closure`	—	`spanning_iff`
`spanning_iff_compl_coindep` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`Spanning` `Coindep` `Set.instSDiff`	—	`coindep_iff_compl_spanning` `Set.diff_diff_cancel_left`
`spanning_iff_exists_isBase_subset` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`Spanning` `IsBase`	—	`spanning_iff_exists_isBase_subset'`
`spanning_iff_exists_isBase_subset'` 📖	mathematical	—	`Spanning` `IsBase` `Set` `Set.instHasSubset` `E`	—	`exists_isBasis` `Spanning.subset_ground` `IsBasis.isBasis_closure_right` `isBasis_ground_iff` `Spanning.closure_eq` `IsBasis.subset` `Spanning.superset` `IsBase.spanning`
`spanning_iff_ground_subset_closure` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`Spanning` `closure`	—	`spanning_iff_closure_eq` `subset_antisymm_iff` `Set.instReflSubset` `Set.instAntisymmSubset` `closure_subset_ground`
`subset_closure` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`closure`	—	`closure_def'`
`subset_closure_diff_iff_closure_eq` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`closure` `Set.instSDiff`	—	`closure_diff_eq_self` `HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure_of_subset'` `Eq.subset` `Set.instReflSubset`
`subset_closure_iff_forall_subset_isFlat` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`closure`	—	`closure_def'`
`subset_closure_of_subset` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`closure`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure`
`subset_closure_of_subset'` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`closure`	—	`closure_inter_ground` `subset_closure_of_subset` `Set.subset_inter`
`uniqueBaseOn_closure_eq` 📖	mathematical	—	`closure` `uniqueBaseOn` `Set` `Set.instUnion` `Set.instInter` `Set.instSDiff`	—	`uniqueBaseOn.eq_1` `restrict_closure_eq'` `freeOn_closure_eq` `Set.inter_right_comm` `Set.inter_assoc` `Set.inter_self` `freeOn_ground`

Matroid.Coindep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_compl` 📖	mathematical	`Matroid.Coindep`	`Matroid.closure` `Set` `Set.instSDiff` `Matroid.E`	—	`Matroid.coindep_iff_closure_compl_eq_ground` `subset_ground`
`compl_spanning` 📖	mathematical	`Matroid.Coindep`	`Matroid.Spanning` `Set` `Set.instSDiff` `Matroid.E`	—	`Matroid.coindep_iff_compl_spanning` `subset_ground`

Matroid.Indep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_diff_singleton_ssubset` 📖	mathematical	`Matroid.Indep` `Set` `Set.instMembership`	`Set.instHasSSubset` `Matroid.closure` `Set.instSDiff` `Set.instSingletonSet`	—	`closure_ssubset_closure`
`closure_diff_ssubset` 📖	mathematical	`Matroid.Indep` `Set.Nonempty` `Set` `Set.instInter`	`Set.instHasSSubset` `Matroid.closure` `Set.instSDiff`	—	`closure_ssubset_closure` `HasSubset.Subset.ssubset_of_ne` `Set.instIsNonstrictStrictOrderSubsetSSubset` `Set.instAntisymmSubset` `Set.diff_subset` `Set.disjoint_iff_inter_eq_empty` `sdiff_eq_left`
`closure_eq_setOf_isBasis_insert` 📖	mathematical	`Matroid.Indep`	`Matroid.closure` `setOf` `Matroid.IsBasis` `Set` `Set.instInsert`	—	`isBasis_setOf_insert_isBasis` `Matroid.IsBasis.isBasis_subset` `Matroid.IsBasis.isBasis_of_isBasis_of_subset_of_subset` `Matroid.IsBasis.isBasis_union` `Matroid.IsBasis.subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.subset_union_right` `Set.subset_insert` `Set.insert_subset` `Matroid.IsBasis.subset_ground` `subset_antisymm_iff` `Set.instReflSubset` `Set.instAntisymmSubset` `Matroid.closure_def` `Set.subset_sInter_iff` `Set.sInter_subset_of_mem` `Set.inter_subset_left` `subset_isBasis_of_subset` `Set.inter_eq_left` `Matroid.IsFlat.subset_ground` `Matroid.IsFlat.subset_of_isBasis_of_isBasis` `Matroid.IsBasis.isBasis_union_of_subset` `Matroid.IsBasis.indep` `Set.mem_insert`
`closure_iInter_eq_biInter_closure_of_forall_subset` 📖	mathematical	`Matroid.Indep` `Set` `Set.instHasSubset`	`Matroid.closure` `Set.iInter`	—	`Matroid.closure_iInter_eq_iInter_closure_of_iUnion_indep` `subset`
`closure_insert_diff_eq_of_mem_closure` 📖	—	`Matroid.Indep` `Set` `Set.instMembership` `Matroid.closure` `Set.instSDiff` `Set.instInsert` `Set.instSingletonSet`	—	—	`subset_antisymm` `Set.instAntisymmSubset` `Matroid.closure_subset_closure_of_subset_closure` `Matroid.subset_closure` `subset_ground` `eq_or_ne` `Matroid.mem_closure_of_mem'`
`closure_inter_eq_inter_closure` 📖	mathematical	`Matroid.Indep` `Set` `Set.instUnion`	`Matroid.closure` `Set.instInter`	—	`Set.inter_eq_iInter` `Matroid.closure_iInter_eq_iInter_closure_of_iUnion_indep` `Set.union_eq_iUnion` `Set.iInter_congr`
`closure_inter_eq_self_of_subset` 📖	mathematical	`Matroid.Indep` `Set` `Set.instHasSubset`	`Set.instInter` `Matroid.closure`	—	`subset` `subset_antisymm_iff` `Set.instReflSubset` `Set.instAntisymmSubset` `Set.subset_inter` `Matroid.subset_closure` `subset_ground` `Matroid.IsBasis.mem_of_insert_indep` `isBasis_closure` `Set.insert_subset`
`closure_sInter_eq_biInter_closure_of_forall_subset` 📖	mathematical	`Matroid.Indep` `Set.Nonempty` `Set` `Set.instHasSubset`	`Matroid.closure` `Set.sInter` `Set.iInter` `Set.instMembership`	—	`subset_antisymm_iff` `Set.instReflSubset` `Set.instAntisymmSubset` `Set.subset_iInter₂_iff` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.sInter_subset_of_mem` `Set.Nonempty.some_mem` `subset` `Matroid.closure_subset_closure` `by_contra` `Matroid.closure_subset_ground` `Set.mem_iInter₂` `Matroid.mem_closure_of_mem` `closure_inter_eq_self_of_subset` `subset_ground` `subset_isBasis_of_subset` `notMem_closure_iff_of_notMem` `Set.notMem_subset` `Set.insert_subset_insert` `Set.insert_subset` `insert_isBasis_iff_mem_closure` `Matroid.IsBasis.exchange` `Set.mem_insert` `Set.mem_insert_of_mem` `mem_closure_iff` `not_dep` `Matroid.IsBasis.indep` `Set.diff_singleton_eq_self` `Set.diff_subset_iff` `Set.singleton_union` `Set.diff_subset` `eq_of_isBasis` `Matroid.IsBasis.isBasis_subset` `Matroid.IsBasis.subset` `Set.subset_insert`
`closure_ssubset_closure` 📖	mathematical	`Matroid.Indep` `Set` `Set.instHasSSubset`	`Matroid.closure`	—	`Set.exists_of_ssubset` `HasSubset.Subset.ssubset_of_not_subset` `Set.instIsNonstrictStrictOrderSubsetSSubset` `Matroid.closure_subset_closure` `HasSSubset.SSubset.subset` `Eq.subset` `Set.instReflSubset` `closure_inter_eq_self_of_subset` `Matroid.mem_closure_of_mem` `subset_ground`
`eq_of_spanning_subset` 📖	—	`Matroid.Indep` `Matroid.Spanning` `Set` `Set.instHasSubset`	—	—	`Matroid.IsBase.eq_of_subset_indep` `isBase_of_spanning` `subset`
`exists_isBase_subset_spanning` 📖	mathematical	`Matroid.Indep` `Matroid.Spanning` `Set` `Set.instHasSubset`	`Matroid.IsBase`	—	`subset_isBasis_of_subset` `Matroid.Spanning.subset_ground` `Matroid.IsBasis.isBase_of_spanning` `Matroid.IsBasis.subset`
`indep_insert_diff_of_mem_closure` 📖	—	`Matroid.Indep` `Set` `Set.instMembership` `Matroid.closure` `Set.instSDiff` `Set.instInsert` `Set.instSingletonSet`	—	—	`subset` `Set.insert_diff_of_mem` `insert_diff_indep_iff` `Set.diff_subset` `Matroid.mem_ground_of_mem_closure` `notMem_closure_diff_of_mem` `Matroid.closure_subset_closure` `Matroid.closure_insert_eq_of_mem_closure`
`insert_dep_iff` 📖	mathematical	`Matroid.Indep`	`Matroid.Dep` `Set` `Set.instInsert` `Set.instMembership` `Set.instSDiff` `Matroid.closure`	—	`Set.mem_diff` `mem_closure_iff` `Set.insert_eq_of_mem` `not_dep`
`insert_diff_indep_iff` 📖	mathematical	`Matroid.Indep` `Set` `Set.instSDiff` `Set.instSingletonSet` `Set.instMembership`	`Set.instInsert` `Matroid.E` `Matroid.closure`	—	`eq_or_ne` `Set.insert_eq_of_mem` `Set.insert_diff_singleton_comm` `insert_indep_iff` `Set.mem_diff_singleton`
`insert_indep_iff` 📖	mathematical	`Matroid.Indep`	`Set` `Set.instInsert` `Set.instMembership` `Set.instSDiff` `Matroid.E` `Matroid.closure`	—	`em` `Set.insert_eq_of_mem` `insert_indep_iff_of_notMem`
`insert_indep_iff_of_notMem` 📖	mathematical	`Matroid.Indep` `Set` `Set.instMembership`	`Set.instInsert` `Set.instSDiff` `Matroid.E` `Matroid.closure`	—	`Set.mem_diff` `mem_closure_iff_of_notMem` `Matroid.dep_iff` `not_imp_not` `Set.insert_subset_iff` `subset_ground` `Set.mem_insert`
`insert_isBasis_iff_mem_closure` 📖	mathematical	`Matroid.Indep`	`Matroid.IsBasis` `Set` `Set.instInsert` `Set.instMembership` `Matroid.closure`	—	`closure_eq_setOf_isBasis_insert` `Set.mem_setOf`
`inter_isBasis_biInter` 📖	mathematical	`Matroid.Indep` `Set.Nonempty` `Matroid.IsBasis` `Set` `Set.instInter`	`Set.iInter` `Set.instMembership`	—	`isBasis_of_subset_of_subset_closure` `inter_left` `Set.inter_subset_left` `Set.biInter_inter` `Matroid.closure_biInter_eq_biInter_closure_of_biUnion_indep` `subset` `Set.iUnion_congr_Prop` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.biInter_subset_of_mem` `Matroid.IsBasis.subset_closure`
`inter_isBasis_closure_iff_subset_closure_inter` 📖	mathematical	`Matroid.Indep`	`Matroid.IsBasis` `Set` `Set.instInter` `Set.instHasSubset` `Matroid.closure`	—	`Matroid.IsBasis.subset_closure` `isBasis_of_subset_of_subset_closure` `inter_left` `Set.inter_subset_left`
`inter_isBasis_iInter` 📖	mathematical	`Matroid.Indep` `Matroid.IsBasis` `Set` `Set.instInter`	`Set.iInter`	—	`Set.iInter_congr_Prop` `Set.iInter_true` `Set.iInter_plift_down` `inter_isBasis_biInter` `Set.univ_nonempty` `PLift.instNonempty_mathlib`
`inter_isBasis_sInter` 📖	mathematical	`Matroid.Indep` `Set.Nonempty` `Set` `Matroid.IsBasis` `Set.instInter`	`Set.sInter`	—	`Set.sInter_eq_biInter` `inter_isBasis_biInter`
`isBase_iff_ground_subset_closure` 📖	mathematical	`Matroid.Indep`	`Matroid.IsBase` `Set` `Set.instHasSubset` `Matroid.E` `Matroid.closure`	—	`Eq.subset` `Set.instReflSubset` `Matroid.IsBase.closure_eq` `isBase_of_ground_subset_closure`
`isBase_of_ground_subset_closure` 📖	mathematical	`Matroid.Indep` `Set` `Set.instHasSubset` `Matroid.E` `Matroid.closure`	`Matroid.IsBase`	—	`Matroid.isBasis_ground_iff` `isBasis_of_subset_of_subset_closure` `subset_ground`
`isBase_of_spanning` 📖	mathematical	`Matroid.Indep` `Matroid.Spanning`	`Matroid.IsBase`	—	`Matroid.Spanning.exists_isBase_subset` `Matroid.IsBase.eq_of_subset_indep`
`isBasis_closure` 📖	mathematical	`Matroid.Indep`	`Matroid.IsBasis` `Matroid.closure`	—	`closure_eq_setOf_isBasis_insert` `isBasis_setOf_insert_isBasis`
`isBasis_of_subset_of_subset_closure` 📖	mathematical	`Matroid.Indep` `Set` `Set.instHasSubset` `Matroid.closure`	`Matroid.IsBasis`	—	`Matroid.IsBasis.isBasis_subset` `isBasis_closure`
`mem_closure_iff` 📖	mathematical	`Matroid.Indep`	`Set` `Set.instMembership` `Matroid.closure` `Matroid.Dep` `Set.instInsert`	—	`closure_eq_setOf_isBasis_insert` `Set.mem_setOf` `isBasis_insert_iff`
`mem_closure_iff'` 📖	mathematical	`Matroid.Indep`	`Set` `Set.instMembership` `Matroid.closure` `Matroid.E`	—	`mem_closure_iff` `Matroid.dep_iff` `Set.insert_subset_iff` `subset_ground` `imp_iff_not_or` `Set.insert_eq_of_mem`
`mem_closure_iff_of_notMem` 📖	mathematical	`Matroid.Indep` `Set` `Set.instMembership`	`Matroid.closure` `Matroid.Dep` `Set.instInsert`	—	`insert_dep_iff` `Set.mem_diff`
`notMem_closure_diff_of_mem` 📖	mathematical	`Matroid.Indep` `Set` `Set.instMembership`	`Matroid.closure` `Set.instSDiff` `Set.instSingletonSet`	—	`Matroid.indep_iff_forall_notMem_closure_diff'`
`notMem_closure_iff` 📖	mathematical	`Matroid.Indep` `Set` `Set.instMembership` `Matroid.E`	`Matroid.closure` `Set.instInsert`	—	`mem_closure_iff` `Matroid.dep_iff` `Set.insert_subset_iff` `subset_ground`
`notMem_closure_iff_of_notMem` 📖	mathematical	`Matroid.Indep` `Set` `Set.instMembership` `Matroid.E`	`Matroid.closure` `Set.instInsert`	—	`notMem_closure_iff`
`union_indep_iff_forall_notMem_closure_left` 📖	mathematical	`Matroid.Indep`	`Set` `Set.instUnion` `Set.instMembership` `Matroid.closure` `Set.instSDiff` `Set.instSingletonSet`	—	`Set.union_comm` `union_indep_iff_forall_notMem_closure_right`
`union_indep_iff_forall_notMem_closure_right` 📖	mathematical	`Matroid.Indep`	`Set` `Set.instUnion` `Set.instMembership` `Matroid.closure` `Set.instSDiff` `Set.instSingletonSet`	—	`notMem_closure_diff_of_mem` `Set.union_diff_distrib` `Set.diff_singleton_eq_self` `subset_isBasis_of_subset` `Set.subset_union_left` `subset_ground` `HasSubset.Subset.eq_or_ssubset` `Set.instIsNonstrictStrictOrderSubsetSSubset` `Set.instAntisymmSubset` `Matroid.IsBasis.subset` `Matroid.IsBasis.indep` `Set.exists_of_ssubset` `Set.union_diff_right` `Set.union_comm` `Set.notMem_subset` `Matroid.closure_subset_closure` `Set.subset_diff_singleton` `Matroid.IsBasis.subset_closure`

Matroid.IsBase

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_eq` 📖	mathematical	`Matroid.IsBase`	`Matroid.closure` `Matroid.E`	—	`Matroid.IsBasis.closure_eq_closure` `Matroid.isBasis_ground_iff` `Matroid.closure_ground`
`closure_of_superset` 📖	mathematical	`Matroid.IsBase` `Set` `Set.instHasSubset`	`Matroid.closure` `Matroid.E`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Matroid.closure_subset_ground` `Matroid.closure_subset_closure` `closure_eq`
`eq_of_superset_spanning` 📖	—	`Matroid.IsBase` `Matroid.Spanning` `Set` `Set.instHasSubset`	—	—	`Matroid.Spanning.exists_isBase_subset` `subset_antisymm` `Set.instAntisymmSubset` `eq_of_subset_isBase` `HasSubset.Subset.trans` `Set.instIsTransSubset`
`exchange_base_of_notMem_closure` 📖	mathematical	`Matroid.IsBase` `Set` `Set.instMembership` `Matroid.closure` `Set.instSDiff` `Set.instSingletonSet` `Matroid.E`	`Set.instInsert`	—	`eq_or_ne` `Set.insert_diff_self_of_mem` `Matroid.Indep.notMem_closure_iff` `Matroid.Indep.diff` `indep` `exchange_isBase_of_indep`
`isBase_insert_diff_of_mem_closure` 📖	—	`Matroid.IsBase` `Set` `Set.instMembership` `Matroid.closure` `Set.instSDiff` `Set.instInsert` `Set.instSingletonSet`	—	—	`Matroid.isBasis_ground_iff` `Matroid.IsBasis.isBasis_insert_diff_of_mem_closure` `Set.insert_diff_of_mem` `Set.diff_singleton_eq_self` `Matroid.Indep.notMem_closure_diff_of_mem` `Matroid.IsBasis.indep` `Matroid.closure_subset_closure` `Matroid.closure_inter_ground`
`spanning` 📖	mathematical	`Matroid.IsBase`	`Matroid.Spanning`	—	`closure_eq` `subset_ground`
`spanning_of_superset` 📖	mathematical	`Matroid.IsBase` `Set` `Set.instHasSubset` `Matroid.E`	`Matroid.Spanning`	—	`Matroid.Spanning.superset` `spanning`

Matroid.IsBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_eq_closure` 📖	mathematical	`Matroid.IsBasis`	`Matroid.closure`	—	`subset_antisymm` `Set.instAntisymmSubset` `Matroid.closure_subset_closure` `subset` `Matroid.closure_closure` `Matroid.Indep.closure_eq_setOf_isBasis_insert` `indep` `isBasis_subset` `Set.subset_insert` `Set.insert_subset`
`closure_eq_right` 📖	—	`Matroid.IsBasis` `Matroid.closure`	—	—	`closure_eq_closure` `Matroid.closure_closure`
`closure_inter_isBasis_closure` 📖	mathematical	`Matroid.IsBasis` `Set` `Set.instInter` `Matroid.Indep`	`Matroid.closure`	—	`Matroid.Indep.inter_isBasis_closure_iff_subset_closure_inter` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Matroid.closure_subset_closure_of_subset_closure` `Matroid.closure_subset_closure` `Set.inter_subset_inter_left` `Set.inter_subset_left`
`eq_of_closure_subset` 📖	—	`Matroid.IsBasis` `Set` `Set.instHasSubset` `Matroid.closure`	—	—	`Matroid.Indep.closure_inter_eq_self_of_subset` `indep` `Set.inter_eq_self_of_subset_right` `HasSubset.Subset.trans` `Set.instIsTransSubset` `subset`
`insert_isBasis_insert_of_notMem_closure` 📖	mathematical	`Matroid.IsBasis` `Set` `Set.instMembership` `Matroid.closure` `Matroid.E`	`Set.instInsert`	—	`insert_isBasis_insert` `Matroid.Indep.insert_indep_iff` `indep`
`isBase_of_spanning` 📖	mathematical	`Matroid.IsBasis` `Matroid.Spanning`	`Matroid.IsBase`	—	`Matroid.Indep.isBase_of_spanning` `indep` `spanning_iff_spanning`
`isBasis_closure_right` 📖	mathematical	`Matroid.IsBasis`	`Matroid.closure`	—	`Matroid.IsBasis'.isBasis_closure_right` `isBasis'`
`isBasis_insert_diff_of_mem_closure` 📖	—	`Matroid.IsBasis` `Set` `Set.instMembership` `Matroid.closure` `Set.instSDiff` `Set.instInsert` `Set.instSingletonSet`	—	—	`Matroid.isBasis_iff_indep_closure` `Matroid.Indep.indep_insert_diff_of_mem_closure` `LE.le.trans_eq` `Matroid.Indep.closure_insert_diff_eq_of_mem_closure` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.diff_subset` `Set.insert_subset`
`isBasis_of_closure_eq_closure` 📖	—	`Matroid.IsBasis` `Set` `Set.instHasSubset` `Matroid.closure` `Matroid.E`	—	—	`Matroid.Indep.isBasis_of_subset_of_subset_closure` `indep` `closure_eq_closure` `Matroid.subset_closure`
`spanning_iff_spanning` 📖	mathematical	`Matroid.IsBasis`	`Matroid.Spanning`	—	`Matroid.spanning_iff_closure_eq` `left_subset_ground` `subset_ground` `closure_eq_closure`
`subset_closure` 📖	mathematical	`Matroid.IsBasis`	`Set` `Set.instHasSubset` `Matroid.closure`	—	`Matroid.closure_subset_closure_iff_subset_closure` `subset_ground` `closure_eq_closure` `subset_refl` `Set.instReflSubset`

Matroid.IsBasis'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_eq_closure` 📖	mathematical	`Matroid.IsBasis'`	`Matroid.closure`	—	`Matroid.closure_inter_ground` `Matroid.IsBasis.closure_eq_closure` `isBasis_inter_ground`
`isBasis_closure_right` 📖	mathematical	`Matroid.IsBasis'`	`Matroid.IsBasis` `Matroid.closure`	—	`closure_eq_closure` `Matroid.Indep.isBasis_closure` `indep`

Matroid.IsFlat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure` 📖	mathematical	`Matroid.IsFlat`	`Matroid.closure`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Set.sInter_subset_of_mem` `Matroid.subset_closure` `subset_ground`
`iInter` 📖	mathematical	`Matroid.IsFlat`	`Set.iInter`	—	`Set.subset_iInter` `Matroid.Indep.subset_isBasis_of_subset` `Matroid.IsBasis.indep` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Matroid.IsBasis.subset` `Set.iInter_subset` `subset_ground` `Set.subset_union_right` `subset_of_isBasis_of_isBasis` `Set.union_assoc` `Set.union_eq_self_of_subset_right` `Matroid.IsBasis.isBasis_union` `Matroid.IsBasis.isBasis_union_of_subset`
`subset_ground` 📖	mathematical	`Matroid.IsFlat`	`Set` `Set.instHasSubset` `Matroid.E`	—	—
`subset_of_isBasis_of_isBasis` 📖	mathematical	`Matroid.IsFlat` `Matroid.IsBasis`	`Set` `Set.instHasSubset`	—	—

Matroid.Restriction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBase_iff_of_spanning` 📖	mathematical	`Matroid.IsRestriction` `Matroid.Spanning` `Matroid.E`	`Matroid.IsBase` `Set` `Set.instHasSubset`	—	`Matroid.Spanning.isBase_restrict_iff` `Matroid.restrict_ground_eq`

Matroid.Spanning

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_eq` 📖	mathematical	`Matroid.Spanning`	`Matroid.closure` `Matroid.E`	—	—
`closure_eq_of_superset` 📖	mathematical	`Matroid.Spanning` `Set` `Set.instHasSubset`	`Matroid.closure` `Matroid.E`	—	`Matroid.closure_inter_ground` `Matroid.spanning_iff_closure_eq` `superset` `Set.subset_inter` `subset_ground`
`compl_coindep` 📖	mathematical	`Matroid.Spanning`	`Matroid.Coindep` `Set` `Set.instSDiff` `Matroid.E`	—	`Matroid.spanning_iff_compl_coindep` `subset_ground`
`exists_isBase_subset` 📖	mathematical	`Matroid.Spanning`	`Matroid.IsBase` `Set` `Set.instHasSubset`	—	`Matroid.spanning_iff_exists_isBase_subset` `subset_ground`
`isBase_of_indep` 📖	mathematical	`Matroid.Spanning` `Matroid.Indep`	`Matroid.IsBase`	—	`Matroid.Indep.isBase_of_spanning`
`isBase_of_minimal` 📖	mathematical	`Matroid.Spanning`	`Matroid.IsBase`	—	`Matroid.isBase_iff_minimal_spanning` `minimal_subset_iff`
`isBase_restrict_iff` 📖	mathematical	`Matroid.Spanning`	`Matroid.IsBase` `Matroid.restrict` `Set` `Set.instHasSubset`	—	`Matroid.isBase_restrict_iff'` `Matroid.isBasis'_iff_isBasis` `subset_ground` `Matroid.Indep.isBase_of_spanning` `Matroid.IsBasis.indep` `Matroid.IsBasis.spanning_iff_spanning` `Matroid.IsBasis.subset` `Matroid.Indep.isBasis_of_subset_of_subset_closure` `Matroid.IsBase.indep` `Matroid.IsBase.closure_eq`
`subset_ground` 📖	mathematical	`Matroid.Spanning`	`Set` `Set.instHasSubset` `Matroid.E`	—	—
`superset` 📖	—	`Matroid.Spanning` `Set` `Set.instHasSubset` `Matroid.E`	—	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Matroid.closure_subset_ground` `closure_eq` `Matroid.closure_subset_closure`
`union_left` 📖	mathematical	`Matroid.Spanning` `Set` `Set.instHasSubset` `Matroid.E`	`Set.instUnion`	—	`superset` `Set.subset_union_left` `subset_ground`
`union_right` 📖	mathematical	`Matroid.Spanning` `Set` `Set.instHasSubset` `Matroid.E`	`Set.instUnion`	—	`superset` `Set.subset_union_right` `subset_ground`

---

← Back to Index