Delete

📁 Source: Mathlib/Combinatorics/Matroid/Minor/Delete.lean

Statistics

Metric	Count
Definitions delete, «term_＼_»	2
Theorems delete_isBase_iff, delete_rankPos, delete_spanning_iff, indep_delete_of_disjoint, of_delete, delete, of_delete, of_delete, of_delete, exists_eq_delete, isRestriction_deleteElem, restrict_delete_of_disjoint, circuit_iff_delete_of_disjoint, deleteElem_eq_self, deleteElem_indep_iff, delete_closure_eq, delete_closure_eq_of_disjoint, delete_comm, delete_compl, delete_delete, delete_delete_eq_delete_diff, delete_dep_iff, delete_empty, delete_eq_delete_iff, delete_eq_restrict, delete_eq_self, delete_eq_self_iff, delete_finitary, delete_finite, delete_ground, delete_indep_iff, delete_inter_ground_eq, delete_isBase_iff, delete_isBasis'_iff, delete_isBasis_iff, delete_isCircuit_iff, delete_isColoop_iff, delete_isLoop_iff, delete_isNonloop_iff, delete_isRestriction, delete_loops_eq, delete_loops_eq_removeLoops, delete_rankFinite, delete_subset_ground, indep_iff_delete_of_disjoint, isNonloop_iff_delete_of_notMem, isRestriction_iff_exists_eq_delete, restrict_compl	48
Total	50

Matroid

Definitions

Name	Category	Theorems
delete 📖	CompOp	70 math math: IsBasis'.contract_eq_contract_delete, isNonloop_iff_delete_of_notMem, delete_comm, IsCocircuit.delete_isCocircuit, indep_iff_delete_of_disjoint, IsRestriction.exists_eq_delete, delete_inter_ground_eq, IsMinor.exists_eq_contract_delete_disjoint, delete_eq_self_iff, delete_isBasis'_iff, delete_empty, Coindep.delete_spanning_iff, contract_delete_isMinor, delete_compl, dual_contract_delete, deleteElem_indep_iff, contract_eq_delete_of_subset_loops, dual_contract, delete_closure_eq, contract_eq_delete_of_subset_coloops, circuit_iff_delete_of_disjoint, contract_delete_comm', deleteElem_eq_self, delete_isNonloop_iff, delete_contract_delete, delete_contract_eq_diff, IsBasis.delete, dual_delete_contract, delete_closure_eq_of_disjoint, delete_eq_restrict, delete_isRestriction, contract_delete_contract, delete_finitary, delete_isLoop_iff, delete_ground, dual_delete_dual, contract_delete_diff, contract_delete_contract', delete_loops_eq_removeLoops, delete_loops_eq, delete_finite, contract_delete_contract_delete, delete_isColoop_iff, delete_dep_iff, isRestriction_iff_exists_eq_delete, IsRestriction.isRestriction_deleteElem, contract_closure_eq_contract_delete, dual_contract_dual, delete_contract_comm', delete_rankFinite, Indep.indep_delete_of_disjoint, delete_isBasis_iff, contract_delete_comm, IsRestriction.restrict_delete_of_disjoint, IsBasis.contract_eq_contract_delete, delete_contract_delete', restrict_compl, delete_subset_ground, delete_delete, delete_eq_delete_iff, delete_eq_self, Coindep.delete_isBase_iff, contract_delete_contract_delete', delete_indep_iff, delete_isCircuit_iff, Coindep.delete_rankPos, delete_isBase_iff, delete_delete_eq_delete_diff, dual_delete, IsCocircuit.delete_diff_isCocircuit
«term_＼_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
circuit_iff_delete_of_disjoint 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	IsCircuit delete	—	delete_isCircuit_iff IsCircuit.of_delete
deleteElem_eq_self 📖	mathematical	Set Set.instMembership E	delete Set.instSingletonSet	—	—
deleteElem_indep_iff 📖	mathematical	—	Indep delete Set Set.instSingletonSet Set.instMembership	—	—
delete_closure_eq 📖	mathematical	—	closure delete Set Set.instSDiff	—	restrict_compl restrict_closure_eq' sdiff_sdiff_self Set.bot_eq_empty Set.union_empty Set.diff_eq Set.inter_comm Set.inter_assoc closure_inter_ground Set.inter_eq_left HasSubset.Subset.trans Set.instIsTransSubset Set.diff_subset closure_subset_ground
delete_closure_eq_of_disjoint 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	closure delete Set.instSDiff	—	delete_closure_eq Disjoint.sdiff_eq_left
delete_comm 📖	mathematical	—	delete	—	delete_delete Set.union_comm
delete_compl 📖	mathematical	Set Set.instHasSubset E	delete Set.instSDiff restrict	—	restrict_compl Set.diff_diff_cancel_left
delete_delete 📖	mathematical	—	delete Set Set.instUnion	—	restrict_compl restrict_restrict_eq restrict_ground_eq Set.diff_diff
delete_delete_eq_delete_diff 📖	mathematical	—	delete Set Set.instSDiff	—	delete_delete Set.union_diff_self
delete_dep_iff 📖	mathematical	—	Dep delete Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	dep_iff delete_indep_iff delete_ground Set.subset_diff
delete_empty 📖	mathematical	—	delete Set Set.instEmptyCollection	—	delete_eq_self_iff Set.empty_disjoint
delete_eq_delete_iff 📖	mathematical	—	delete Set Set.instInter E	—	delete_inter_ground_eq Set.diff_diff_cancel_left Set.inter_subset_right
delete_eq_restrict 📖	mathematical	—	delete restrict Set Set.instSDiff E	—	—
delete_eq_self 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice E	delete	—	delete_eq_self_iff
delete_eq_self_iff 📖	mathematical	—	delete Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice E	—	restrict_compl restrict_eq_self_iff sdiff_eq_left disjoint_comm
delete_finitary 📖	mathematical	—	Finitary delete	—	restrict_finitary
delete_finite 📖	mathematical	—	Finite delete	—	Set.Finite.diff ground_finite
delete_ground 📖	mathematical	—	E delete Set Set.instSDiff	—	—
delete_indep_iff 📖	mathematical	—	Indep delete Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	restrict_compl restrict_indep_iff Set.subset_diff Indep.subset_ground
delete_inter_ground_eq 📖	mathematical	—	delete Set Set.instInter E	—	restrict_compl Set.diff_inter_self_eq_diff
delete_isBase_iff 📖	mathematical	—	IsBase delete IsBasis Set Set.instSDiff E	—	restrict_compl isBase_restrict_iff
delete_isBasis'_iff 📖	mathematical	—	IsBasis' delete Set Set.instSDiff	—	isBasis'_iff_isBasis_inter_ground delete_isBasis_iff delete_ground Set.diff_eq Set.inter_comm Set.inter_assoc Set.inter_diff_assoc Set.disjoint_sdiff_left
delete_isBasis_iff 📖	mathematical	—	IsBasis delete Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	restrict_compl isBasis_restrict_iff Set.subset_diff IsBasis.subset_ground
delete_isCircuit_iff 📖	mathematical	—	IsCircuit delete Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	delete_eq_restrict restrict_isCircuit_iff Set.subset_diff IsCircuit.subset_ground
delete_isColoop_iff 📖	mathematical	—	IsColoop delete Set Set.instMembership closure Set.instSDiff E Set.instSingletonSet	—	delete_eq_restrict restrict_isColoop_iff Set.diff_subset Set.mem_diff
delete_isLoop_iff 📖	mathematical	—	IsLoop delete Set Set.instMembership	—	singleton_dep delete_dep_iff Set.disjoint_singleton_left
delete_isNonloop_iff 📖	mathematical	—	IsNonloop delete Set Set.instMembership	—	indep_singleton delete_indep_iff Set.disjoint_singleton_left
delete_isRestriction 📖	mathematical	—	IsRestriction delete	—	restrict_isRestriction Set.diff_subset
delete_loops_eq 📖	mathematical	—	loops delete Set Set.instSDiff	—	delete_closure_eq Set.empty_diff
delete_loops_eq_removeLoops 📖	mathematical	—	delete loops removeLoops	—	removeLoops.eq_1 delete_eq_restrict compl_loops_eq
delete_rankFinite 📖	mathematical	—	RankFinite delete	—	restrict_rankFinite
delete_subset_ground 📖	mathematical	—	Set Set.instHasSubset E delete	—	Set.diff_subset
indep_iff_delete_of_disjoint 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Indep delete	—	Indep.indep_delete_of_disjoint Indep.of_delete
isNonloop_iff_delete_of_notMem 📖	mathematical	Set Set.instMembership	IsNonloop delete	—	delete_isNonloop_iff IsNonloop.of_delete
isRestriction_iff_exists_eq_delete 📖	mathematical	—	IsRestriction Set Set.instHasSubset E delete	—	IsRestriction.exists_eq_delete delete_isRestriction
restrict_compl 📖	mathematical	—	restrict Set Set.instSDiff E delete	—	—

Matroid.Coindep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
delete_isBase_iff 📖	mathematical	Matroid.Coindep	Matroid.IsBase Matroid.delete Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	Matroid.delete_isBase_iff Matroid.IsBasis.subset Matroid.IsBasis.isBasis_closure_right Matroid.isBasis_ground_iff closure_compl Set.subset_diff Matroid.IsBasis.isBasis_subset Matroid.IsBase.isBasis_ground Matroid.IsBase.subset_ground Set.diff_subset
delete_rankPos 📖	mathematical	Matroid.Coindep	Matroid.RankPos Matroid.delete	—	Matroid.rankPos_iff delete_isBase_iff Matroid.empty_not_isBase
delete_spanning_iff 📖	mathematical	Matroid.Coindep	Matroid.Spanning Matroid.delete Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	delete_isBase_iff Disjoint.mono_left

Matroid.Indep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
indep_delete_of_disjoint 📖	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.delete	—	Matroid.delete_indep_iff
of_delete 📖	—	Matroid.Indep Matroid.delete	—	—	Matroid.delete_indep_iff

Matroid.IsBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
delete 📖	mathematical	Matroid.IsBasis Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Matroid.delete	—	Matroid.delete_isBasis_iff
of_delete 📖	—	Matroid.IsBasis Matroid.delete	—	—	Matroid.delete_isBasis_iff

Matroid.IsCircuit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_delete 📖	—	Matroid.IsCircuit Matroid.delete	—	—	Matroid.delete_isCircuit_iff

Matroid.IsNonloop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_delete 📖	—	Matroid.IsNonloop Matroid.delete	—	—	Matroid.delete_isNonloop_iff

Matroid.IsRestriction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_eq_delete 📖	mathematical	Matroid.IsRestriction	Set Set.instHasSubset Matroid.E Matroid.delete	—	Set.diff_subset Matroid.delete_compl Matroid.restrict_ground_eq
isRestriction_deleteElem 📖	mathematical	Matroid.IsRestriction Set Set.instMembership Matroid.E	Matroid.delete Set.instSingletonSet	—	restrict_delete_of_disjoint
restrict_delete_of_disjoint 📖	mathematical	Matroid.IsRestriction Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Matroid.E	Matroid.delete	—	Matroid.isRestriction_iff_exists_eq_delete Set.diff_subset_diff_left Matroid.delete_delete Set.union_diff_self Set.union_comm Matroid.delete_eq_self_iff

---

← Back to Index