Contract

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

Statistics

Metric	Count
Definitions contract, «term_／_»	2
Theorems coindep_contract_of_disjoint, of_contract, contract_dep_iff, contract_indep_iff, contract_isBase_iff, diff_indep_contract_of_subset, of_contract, union_indep_iff_contract_indep, union_isBasis_union_of_contract_isBasis, contract_dep_iff, contract_eq_contract_delete, contract_indep_diff_iff, contract_indep_iff, contract_isBasis', contract_isBasis'_diff_diff_of_subset, contract_isBasis'_diff_of_subset, contract_isBasis_of_indep, contract_isBasis_union_union, contract_dep_iff, contract_diff_isBasis_diff, contract_eq_contract_delete, contract_indep_diff_iff, contract_indep_iff, contract_indep_iff_of_disjoint, contract_isBasis, contract_isBasis_diff_diff_of_subset, contract_isBasis_of_disjoint, contract_isBasis_of_disjoint_indep, contract_isBasis_of_indep, contract_isBasis_of_isBasis', contract_isBasis_union_union, diff_subset_loops_contract, contractElem_isCircuit, contract_dep, contract_dep_of_not_subset, contract_diff_isCircuit, contract_isCircuit, exists_subset_isCircuit_of_contract, delete_diff_isCocircuit, delete_isCocircuit, of_contract, contractElem_indep_iff, of_contract, contract, contract_eq_loopyOn, coindep_contract_iff, contractElem_eq_self, contract_closure_eq, contract_closure_eq_contract_delete, contract_coloops_eq, contract_comm, contract_contract, contract_contract_eq_contract_diff, contract_delete_comm, contract_delete_comm', contract_delete_contract, contract_delete_contract', contract_delete_contract_delete, contract_delete_contract_delete', contract_delete_diff, contract_empty, contract_eq_contract_iff, contract_eq_delete_of_subset_coloops, contract_eq_delete_of_subset_loops, contract_eq_self_iff, contract_finitary, contract_finite, contract_ground, contract_ground_subset_ground, contract_inter_ground_eq, contract_isCocircuit_iff, contract_isColoop_iff, contract_isLoop_iff_mem_closure, contract_isNonloop_iff, contract_loops_eq, contract_rankFinite, contract_restrict_eq_restrict_contract, contract_spanning_iff, contract_spanning_iff', delete_contract_comm', delete_contract_delete, delete_contract_delete', delete_contract_eq_diff, dual_contract, dual_contract_delete, dual_contract_dual, dual_delete, dual_delete_contract, dual_delete_dual, restrict_contract_eq_contract_restrict	90
Total	92

Matroid

Definitions

Name	Category	Theorems
contract 📖	CompOp	84 math math: IsBasis'.contract_isBasis_of_indep, IsBasis'.contract_eq_contract_delete, IsNonloop.contractElem_indep_iff, IsBasis'.contract_isBasis', IsBasis.contract_isBasis_of_indep, IsBasis.contract_dep_iff, contract_isCocircuit_iff, IsBasis.contract_indep_iff, contract_contract_eq_contract_diff, IsBasis.contract_isBasis, IsMinor.exists_eq_contract_delete_disjoint, contract_eq_self_iff, Coindep.coindep_contract_of_disjoint, IsCircuit.contract_dep, contract_delete_isMinor, Spanning.contract_eq_loopyOn, contract_isNonloop_iff, dual_contract_delete, contract_eq_delete_of_subset_loops, dual_contract, Indep.contract_dep_iff, IsCircuit.contract_isCircuit, contract_eq_delete_of_subset_coloops, contract_ground, IsBasis.contract_isBasis_diff_diff_of_subset, Indep.diff_indep_contract_of_subset, contract_delete_comm', contract_closure_eq, IsCircuit.contract_diff_isCircuit, delete_contract_delete, Indep.union_indep_iff_contract_indep, delete_contract_eq_diff, IsBasis.contract_indep_iff_of_disjoint, contract_spanning_iff, dual_delete_contract, contract_delete_contract, contract_empty, IsBasis.contract_isBasis_union_union, IsBasis'.contract_isBasis_union_union, IsBasis.contract_diff_isBasis_diff, contract_loops_eq, dual_delete_dual, contract_delete_diff, contract_coloops_eq, contract_isColoop_iff, contract_delete_contract', IsBasis.contract_isBasis_of_isBasis', coindep_contract_iff, contract_finitary, IsBasis.contract_isBasis_of_disjoint_indep, IsBasis.contract_indep_diff_iff, contract_delete_contract_delete, IsCircuit.contract_dep_of_not_subset, contractElem_eq_self, contract_spanning_iff', Indep.contract_indep_iff, contract_inter_ground_eq, contract_eq_contract_iff, contract_closure_eq_contract_delete, dual_contract_dual, IsCircuit.contractElem_isCircuit, contract_finite, delete_contract_comm', restrict_contract_eq_contract_restrict, contract_comm, contract_delete_comm, IsBasis.contract_eq_contract_delete, contract_contract, delete_contract_delete', contract_restrict_eq_restrict_contract, IsBasis'.contract_isBasis'_diff_diff_of_subset, Indep.contract_isBase_iff, IsBasis.diff_subset_loops_contract, contract_ground_subset_ground, contract_delete_contract_delete', IsBasis'.contract_dep_iff, Spanning.contract, IsBasis'.contract_isBasis'_diff_of_subset, IsBasis'.contract_indep_diff_iff, IsBasis'.contract_indep_iff, contract_isLoop_iff_mem_closure, dual_delete, IsBasis.contract_isBasis_of_disjoint, contract_rankFinite
«term_／_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coindep_contract_iff 📖	mathematical	—	Coindep contract Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	coindep_def dual_contract delete_indep_iff
contractElem_eq_self 📖	mathematical	Set Set.instMembership E	contract Set Set.instSingletonSet	—	dual_delete_dual deleteElem_eq_self dual_dual
contract_closure_eq 📖	mathematical	—	closure contract Set Set.instSDiff Set.instUnion	—	Set.diff_union_inter Set.diff_diff Set.union_comm contract_loops_eq contract_contract subset_antisymm_iff Set.instReflSubset Set.instAntisymmSubset Set.union_subset_iff Set.diff_subset Set.diff_subset_iff sdiff_sdiff_right_self mem_closure_of_mem' mem_ground_of_mem_closure closure_subset_ground
contract_closure_eq_contract_delete 📖	mathematical	—	contract closure delete Set Set.instSDiff	—	exists_isBasis IsBasis.contract_eq_contract_delete IsBasis.isBasis_closure_right delete_delete Set.union_comm Set.diff_union_diff_cancel subset_closure IsBasis.subset contract_inter_ground_eq closure_inter_ground Set.inter_subset_right Set.diff_inter Set.diff_eq_empty closure_subset_ground Set.union_empty
contract_coloops_eq 📖	mathematical	—	coloops contract Set Set.instSDiff	—	dual_delete_dual dual_coloops delete_loops_eq dual_loops
contract_comm 📖	mathematical	—	contract	—	contract_contract Set.union_comm
contract_contract 📖	mathematical	—	contract Set Set.instUnion	—	dual_contract delete_delete
contract_contract_eq_contract_diff 📖	mathematical	—	contract Set Set.instSDiff	—	contract_contract Set.union_diff_self
contract_delete_comm 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	delete contract	—	delete_eq_restrict contract_ground Set.diff_diff_comm restrict_contract_eq_contract_restrict contract_inter_ground_eq Disjoint.mono_left Set.inter_subset_left Set.inter_subset_right contract_eq_contract_iff Set.inter_assoc delete_ground Set.inter_eq_self_of_subset_right Set.diff_subset
contract_delete_comm' 📖	mathematical	—	delete contract Set Set.instSDiff	—	contract_delete_diff contract_delete_comm Set.disjoint_sdiff_right
contract_delete_contract 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	contract delete Set Set.instUnion	—	contract_delete_contract' sdiff_eq_left
contract_delete_contract' 📖	mathematical	—	contract delete Set Set.instUnion Set.instSDiff	—	delete_contract_eq_diff contract_delete_comm Set.disjoint_sdiff_left contract_contract
contract_delete_contract_delete 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	delete contract Set Set.instUnion	—	contract_delete_contract_delete' sdiff_eq_left
contract_delete_contract_delete' 📖	mathematical	—	delete contract Set Set.instUnion Set.instSDiff	—	contract_delete_contract' delete_delete
contract_delete_diff 📖	mathematical	—	delete contract Set Set.instSDiff	—	delete_eq_delete_iff contract_ground Set.diff_eq Set.inter_inter_distrib_right Set.inter_assoc
contract_empty 📖	mathematical	—	contract Set Set.instEmptyCollection	—	dual_delete_dual delete_empty dual_dual
contract_eq_contract_iff 📖	mathematical	—	contract Set Set.instInter E	—	dual_delete_dual delete_eq_delete_iff dual_ground
contract_eq_delete_of_subset_coloops 📖	mathematical	Set Set.instHasSubset coloops	contract delete	—	dual_delete contract_eq_delete_of_subset_loops dual_contract
contract_eq_delete_of_subset_loops 📖	mathematical	Set Set.instHasSubset loops	contract delete	—	IsBasis.contract_eq_contract_delete empty_isBasis_iff contract_empty Set.diff_empty
contract_eq_self_iff 📖	mathematical	—	contract Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice E	—	dual_delete_dual dual_dual delete_eq_self_iff dual_ground
contract_finitary 📖	mathematical	—	Finitary contract	—	exists_isBasis' Indep.contract_indep_iff IsBasis'.indep Set.disjoint_left Indep.subset_ground indep_of_forall_finite_subset_indep Indep.subset Set.inter_subset_right Set.Finite.inter_of_left IsBasis'.contract_eq_contract_delete delete_finitary
contract_finite 📖	mathematical	—	Finite contract	—	dual_delete_dual dual_finite delete_finite
contract_ground 📖	mathematical	—	E contract Set Set.instSDiff	—	—
contract_ground_subset_ground 📖	mathematical	—	Set Set.instHasSubset E contract	—	Eq.trans_subset contract_ground Set.diff_subset
contract_inter_ground_eq 📖	mathematical	—	contract Set Set.instInter E	—	dual_delete_dual dual_ground delete_inter_ground_eq
contract_isCocircuit_iff 📖	mathematical	—	IsCocircuit contract Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	isCocircuit_def dual_contract delete_isCircuit_iff
contract_isColoop_iff 📖	mathematical	—	IsColoop contract Set Set.instMembership	—	contract_coloops_eq
contract_isLoop_iff_mem_closure 📖	mathematical	—	IsLoop contract Set Set.instMembership closure	—	exists_isBasis' IsBasis'.contract_eq_contract_delete delete_isLoop_iff singleton_dep Indep.contract_dep_iff IsBasis'.indep Set.singleton_union Indep.insert_dep_iff IsBasis'.closure_eq_closure IsBasis'.subset
contract_isNonloop_iff 📖	mathematical	—	IsNonloop contract Set Set.instMembership Set.instSDiff E closure	—	isNonloop_iff_mem_compl_loops contract_ground contract_loops_eq closure_inter_ground subset_closure
contract_loops_eq 📖	mathematical	—	loops contract Set Set.instSDiff closure	—	—
contract_rankFinite 📖	mathematical	—	RankFinite contract	—	exists_isBase Indep.finite Indep.of_contract IsBase.indep
contract_restrict_eq_restrict_contract 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	restrict contract Set Set.instUnion	—	ext_indep Set.union_diff_right Disjoint.sdiff_eq_right exists_isBasis' Set.inter_eq_self_of_subset_left Set.subset_union_right isBasis'_restrict_iff restrict_indep_iff IsBasis'.contract_indep_iff IsBasis'.subset
contract_spanning_iff 📖	mathematical	Set Set.instHasSubset E	Spanning contract Set Set.instUnion Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	spanning_iff contract_closure_eq contract_ground Set.union_subset_iff Set.subset_diff Set.union_diff_cancel subset_closure_of_subset' Set.subset_union_right
contract_spanning_iff' 📖	mathematical	—	Spanning contract Set Set.instUnion Set.instInter E Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	contract_inter_ground_eq contract_spanning_iff Set.diff_union_inter Set.disjoint_union_right Disjoint.mono_left HasSubset.Subset.trans Set.instIsTransSubset Set.subset_union_left Spanning.subset_ground Set.disjoint_sdiff_right Disjoint.mono_right Set.inter_subset_left
delete_contract_comm' 📖	mathematical	—	contract delete Set Set.instSDiff	—	delete_contract_eq_diff contract_delete_comm Set.disjoint_sdiff_left
delete_contract_delete 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	delete contract Set Set.instUnion	—	delete_contract_delete' sdiff_eq_left
delete_contract_delete' 📖	mathematical	—	delete contract Set Set.instSDiff Set.instUnion	—	delete_contract_comm' delete_delete
delete_contract_eq_diff 📖	mathematical	—	contract delete Set Set.instSDiff	—	contract_eq_contract_iff delete_ground Set.diff_inter_distrib_right Set.diff_eq Set.inter_assoc
dual_contract 📖	mathematical	—	dual contract delete	—	dual_delete_dual dual_dual
dual_contract_delete 📖	mathematical	—	dual delete contract	—	dual_delete dual_contract
dual_contract_dual 📖	mathematical	—	dual contract delete	—	dual_contract dual_dual
dual_delete 📖	mathematical	—	dual delete contract	—	dual_dual dual_delete_dual
dual_delete_contract 📖	mathematical	—	dual contract delete	—	dual_contract dual_delete
dual_delete_dual 📖	mathematical	—	dual delete contract	—	—
restrict_contract_eq_contract_restrict 📖	mathematical	Set Set.instHasSubset	contract restrict Set Set.instSDiff	—	contract_restrict_eq_restrict_contract Set.disjoint_sdiff_right Set.diff_union_self Set.union_eq_self_of_subset_right

Matroid.Coindep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coindep_contract_of_disjoint 📖	mathematical	Matroid.Coindep Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Matroid.Coindep Matroid.contract	—	Matroid.coindep_contract_iff

Matroid.Dep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_contract 📖	mathematical	Matroid.Dep Matroid.contract Set Set.instHasSubset Matroid.E	Matroid.Dep Set Set.instUnion	—	eq_1 Set.union_subset HasSubset.Subset.trans Set.instIsTransSubset subset_ground Set.diff_subset Set.union_comm Matroid.Indep.contract_indep_iff Matroid.Indep.subset Set.subset_union_left Set.subset_diff

Matroid.Indep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contract_dep_iff 📖	mathematical	Matroid.Indep	Matroid.Dep Matroid.contract Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.instUnion	—	Matroid.dep_iff contract_indep_iff Matroid.contract_ground Set.subset_diff disjoint_comm Set.union_subset_iff subset_ground
contract_indep_iff 📖	mathematical	Matroid.Indep	Matroid.Indep Matroid.contract Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.instUnion	—	contract_isBase_iff Set.disjoint_of_subset_left HasSubset.Subset.trans Set.instIsTransSubset Set.subset_union_left Set.subset_union_right Set.diff_union_self Set.union_eq_self_of_subset_right Set.disjoint_sdiff_left Set.subset_diff
contract_isBase_iff 📖	mathematical	Matroid.Indep	Matroid.IsBase Matroid.contract Set Set.instUnion Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	Matroid.dual_delete_dual Matroid.dual_isBase_iff' Matroid.delete_ground Matroid.dual_ground Matroid.delete_isBase_iff Set.subset_diff Matroid.dual_dual Set.union_comm Set.union_subset_iff subset_ground Matroid.isBase_restrict_iff Set.diff_diff Matroid.Spanning.isBase_restrict_iff Matroid.coindep_iff_compl_spanning Matroid.dual_coindep_iff Set.diff_subset_diff_right Set.subset_union_left sdiff_sdiff_right_self
diff_indep_contract_of_subset 📖	mathematical	Matroid.Indep Set Set.instHasSubset	Matroid.Indep Matroid.contract Set Set.instSDiff	—	union_indep_iff_contract_indep subset Set.union_eq_self_of_subset_left
of_contract 📖	mathematical	Matroid.Indep Matroid.contract	Matroid.Indep	—	subset Matroid.exists_isBasis' Matroid.IsBasis'.contract_indep_iff Set.subset_union_left
union_indep_iff_contract_indep 📖	mathematical	Matroid.Indep	Matroid.Indep Set Set.instUnion Matroid.contract Set.instSDiff	—	contract_indep_iff Set.disjoint_sdiff_left Set.diff_union_self Set.union_comm
union_isBasis_union_of_contract_isBasis 📖	mathematical	Matroid.Indep Matroid.IsBasis Matroid.contract	Matroid.IsBasis Set Set.instUnion	—	isBasis_of_maximal_subset contract_indep_iff Set.union_subset_union_left Set.disjoint_sdiff_left Set.diff_union_of_subset Set.union_subset_iff Set.diff_subset_iff Set.union_comm Set.subset_diff subset_refl Set.instReflSubset subset_ground

Matroid.IsBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contract_dep_iff 📖	mathematical	Matroid.IsBasis	Matroid.Dep Matroid.contract Set Set.instUnion Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	Matroid.IsBasis'.contract_dep_iff isBasis'
contract_diff_isBasis_diff 📖	mathematical	Matroid.IsBasis Set Set.instHasSubset	Matroid.IsBasis Matroid.contract Set Set.instSDiff	—	isBasis_subset contract_isBasis_diff_diff_of_subset Set.subset_diff HasSubset.Subset.trans Set.instIsTransSubset Set.diff_subset subset eq_of_subset_indep Matroid.Indep.inter_right indep Set.subset_inter Set.inter_subset_right Set.diff_self_inter Set.disjoint_sdiff_left Set.diff_subset_diff_right
contract_eq_contract_delete 📖	mathematical	Matroid.IsBasis	Matroid.contract Matroid.delete Set Set.instSDiff	—	Set.diff_union_of_subset subset Matroid.dual_contract_delete Matroid.dual_contract Set.union_comm Matroid.delete_delete Matroid.ext_iff_indep Matroid.dual_coloops Matroid.IsLoop.eq_1 Matroid.singleton_dep Matroid.Indep.contract_dep_iff indep Set.singleton_union Matroid.Indep.insert_dep_iff closure_eq_closure Set.diff_subset_diff_left Matroid.subset_closure subset_ground Matroid.Indep.contract_indep_iff Matroid.Indep.subset Matroid.coloops_indep Matroid.delete_indep_iff Matroid.union_indep_iff_indep_of_subset_coloops
contract_indep_diff_iff 📖	mathematical	Matroid.IsBasis	Matroid.Indep Matroid.contract Set Set.instSDiff Set.instUnion	—	contract_indep_iff Set.disjoint_sdiff_right
contract_indep_iff 📖	mathematical	Matroid.IsBasis	Matroid.Indep Matroid.contract Set Set.instUnion Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	Matroid.IsBasis'.contract_indep_iff isBasis'
contract_indep_iff_of_disjoint 📖	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.Indep Matroid.contract Set Set.instUnion	—	contract_indep_iff
contract_isBasis 📖	mathematical	Matroid.IsBasis Matroid.Indep Set Set.instUnion Set.instSDiff	Matroid.IsBasis Matroid.contract Set Set.instSDiff	—	contract_isBasis_of_isBasis' isBasis'
contract_isBasis_diff_diff_of_subset 📖	mathematical	Matroid.IsBasis Set Set.instHasSubset	Matroid.IsBasis Matroid.contract Set Set.instSDiff	—	Matroid.IsBasis'.isBasis_inter_ground Matroid.IsBasis'.contract_isBasis'_diff_of_subset isBasis' Set.inter_eq_self_of_subset_left subset_ground Set.inter_diff_assoc Matroid.contract_ground
contract_isBasis_of_disjoint 📖	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.Indep Set.instUnion	Matroid.IsBasis Matroid.contract	—	contract_isBasis Disjoint.sdiff_eq_right Disjoint.mono_right subset
contract_isBasis_of_disjoint_indep 📖	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.Indep Set.instUnion	Matroid.IsBasis Matroid.contract	—	Disjoint.sdiff_eq_right Disjoint.mono_right subset contract_isBasis_of_indep
contract_isBasis_of_indep 📖	mathematical	Matroid.IsBasis Matroid.Indep Set Set.instUnion	Matroid.IsBasis Matroid.contract Set Set.instSDiff	—	contract_isBasis Matroid.Indep.isBasis_self Matroid.Indep.subset Set.subset_union_right Set.diff_union_self
contract_isBasis_of_isBasis' 📖	mathematical	Matroid.IsBasis Matroid.IsBasis' Matroid.Indep Set Set.instUnion Set.instSDiff	Matroid.IsBasis Matroid.contract Set Set.instSDiff	—	subset Matroid.IsBasis'.subset Matroid.IsBasis'.contract_eq_contract_delete Matroid.delete_isBasis_iff contract_isBasis_union_union Matroid.Indep.isBasis_of_subset_of_subset_closure Matroid.closure_union_congr_right Matroid.IsBasis'.closure_eq_closure Set.diff_union_self Matroid.closure_union_congr_left closure_eq_closure Matroid.subset_closure_of_subset' Set.union_subset HasSubset.Subset.trans Set.instIsTransSubset Set.diff_subset subset_ground Matroid.Indep.subset_ground Matroid.IsBasis'.indep
contract_isBasis_union_union 📖	mathematical	Matroid.IsBasis Set Set.instUnion Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Matroid.IsBasis Matroid.contract	—	Matroid.isBasis'_iff_isBasis Matroid.contract_ground Set.subset_diff HasSubset.Subset.trans Set.instIsTransSubset Set.subset_union_left subset_ground Matroid.IsBasis'.contract_isBasis_union_union isBasis'
diff_subset_loops_contract 📖	mathematical	Matroid.IsBasis	Set Set.instHasSubset Set.instSDiff Matroid.loops Matroid.contract	—	Set.diff_subset_iff Matroid.contract_loops_eq Set.union_diff_self Set.union_eq_self_of_subset_left Matroid.subset_closure left_subset_ground subset_closure

Matroid.IsBasis'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contract_dep_iff 📖	mathematical	Matroid.IsBasis'	Matroid.Dep Matroid.contract Set Set.instUnion Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	contract_eq_contract_delete Matroid.delete_dep_iff Matroid.Indep.contract_dep_iff indep Set.disjoint_union_right Set.diff_union_of_subset subset disjoint_comm
contract_eq_contract_delete 📖	mathematical	Matroid.IsBasis'	Matroid.contract Matroid.delete Set Set.instSDiff	—	Matroid.contract_inter_ground_eq Matroid.IsBasis.contract_eq_contract_delete isBasis_inter_ground Matroid.delete_inter_ground_eq Matroid.contract_ground Set.diff_eq Set.inter_inter_distrib_right
contract_indep_diff_iff 📖	mathematical	Matroid.IsBasis'	Matroid.Indep Matroid.contract Set Set.instSDiff Set.instUnion	—	contract_indep_iff Set.disjoint_sdiff_right
contract_indep_iff 📖	mathematical	Matroid.IsBasis'	Matroid.Indep Matroid.contract Set Set.instUnion Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	contract_eq_contract_delete Matroid.delete_indep_iff Matroid.Indep.contract_indep_iff indep Set.disjoint_union_right Set.diff_union_self Set.union_eq_self_of_subset_right subset disjoint_comm
contract_isBasis' 📖	mathematical	Matroid.IsBasis' Matroid.Indep Set Set.instUnion Set.instSDiff	Matroid.IsBasis' Matroid.contract Set Set.instSDiff	—	Matroid.isBasis'_iff_isBasis_inter_ground Matroid.contract_ground Set.diff_inter_distrib_right Matroid.IsBasis.contract_isBasis_of_isBasis' isBasis_inter_ground
contract_isBasis'_diff_diff_of_subset 📖	mathematical	Matroid.IsBasis' Set Set.instHasSubset	Matroid.IsBasis' Matroid.contract Set Set.instSDiff	—	eq_of_subset_indep Set.union_subset HasSubset.Subset.trans Set.instIsTransSubset subset Matroid.Indep.contract_indep_iff Matroid.Indep.subset indep Set.diff_union_self Set.union_eq_self_of_subset_right Set.diff_subset Set.union_comm Set.instReflSubset Set.instAntisymmSubset
contract_isBasis'_diff_of_subset 📖	mathematical	Matroid.IsBasis' Set Set.instHasSubset	Matroid.IsBasis' Matroid.contract Set Set.instSDiff	—	Set.inter_diff_assoc isBasis_inter_ground contract_isBasis'_diff_diff_of_subset
contract_isBasis_of_indep 📖	mathematical	Matroid.IsBasis' Matroid.Indep Set Set.instUnion	Matroid.IsBasis' Matroid.contract Set Set.instSDiff	—	contract_isBasis' Matroid.IsBasis.isBasis' Matroid.Indep.isBasis_self Matroid.Indep.subset Set.subset_union_right Set.diff_union_self
contract_isBasis_union_union 📖	mathematical	Matroid.IsBasis' Set Set.instUnion Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Matroid.IsBasis' Matroid.contract	—	Set.union_diff_right Disjoint.sdiff_eq_left contract_isBasis'_diff_diff_of_subset Set.subset_union_right

Matroid.IsCircuit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contractElem_isCircuit 📖	mathematical	Matroid.IsCircuit Set.Nontrivial Set Set.instMembership	Matroid.IsCircuit Matroid.contract Set Set.instSingletonSet Set.instSDiff	—	contract_isCircuit ssubset_of_ne_of_subset Set.instIsNonstrictStrictOrderSubsetSSubset Set.instAntisymmSubset Set.Nontrivial.ne_singleton
contract_dep 📖	mathematical	Matroid.IsCircuit Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Matroid.Dep Matroid.contract	—	Matroid.exists_isBasis Matroid.contract_inter_ground_eq Matroid.Dep.eq_1 Matroid.IsBasis.contract_indep_iff Disjoint.mono_left Set.inter_subset_left Matroid.contract_ground Set.subset_diff Disjoint.mono_right Disjoint.symm subset_ground Matroid.Dep.not_indep dep Matroid.Indep.subset Set.subset_union_left
contract_dep_of_not_subset 📖	mathematical	Matroid.IsCircuit Set Set.instHasSubset	Matroid.Dep Matroid.contract Set Set.instSDiff	—	contract_isCircuit HasSubset.Subset.ssubset_of_ne Set.instIsNonstrictStrictOrderSubsetSSubset Set.instAntisymmSubset Set.inter_subset_right contract_dep Set.diff_inter_self_eq_diff disjoint_sdiff_sdiff Set.inter_union_diff Matroid.contract_contract
contract_diff_isCircuit 📖	mathematical	Matroid.IsCircuit Set.Nonempty Set Set.instHasSubset	Matroid.IsCircuit Matroid.contract Set Set.instSDiff	—	sdiff_sdiff_right_self Set.inter_eq_self_of_subset_right contract_isCircuit Set.diff_ssubset_left_iff
contract_isCircuit 📖	mathematical	Matroid.IsCircuit Set Set.instHasSSubset	Matroid.IsCircuit Matroid.contract Set Set.instSDiff	—	Matroid.Indep.subset diff_singleton_indep Set.instReflSubset Set.subset_diff_singleton HasSSubset.SSubset.subset Set.instIsNonstrictStrictOrderSubsetSSubset Matroid.Indep.contract_indep_iff ssubset_indep Set.diff_union_of_subset not_indep Set.diff_subset_diff_left subset_ground Set.diff_diff_comm Set.diff_union_self
exists_subset_isCircuit_of_contract 📖	mathematical	Matroid.IsCircuit Matroid.contract	Set Matroid.IsCircuit Set.instHasSubset Set.instUnion	—	Set.subset_diff subset_ground Matroid.Dep.exists_isCircuit_subset Matroid.Indep.contract_dep_iff dep Set.disjoint_sdiff_left Matroid.Dep.superset Set.diff_union_self Matroid.Indep.subset_ground eq_of_dep_subset Set.diff_subset_iff Set.union_comm Set.diff_subset Matroid.exists_isBasis' Matroid.delete_isCircuit_iff Matroid.IsBasis'.contract_eq_contract_delete Matroid.IsBasis'.indep HasSubset.Subset.trans Set.instIsTransSubset Set.union_subset_union_right Matroid.IsBasis'.subset

Matroid.IsCocircuit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
delete_diff_isCocircuit 📖	mathematical	Matroid.IsCocircuit Set Set.instHasSubset Set.Nonempty	Matroid.IsCocircuit Matroid.delete Set Set.instSDiff	—	Matroid.isCocircuit_def Matroid.dual_delete Matroid.IsCircuit.contract_diff_isCircuit isCircuit
delete_isCocircuit 📖	mathematical	Matroid.IsCocircuit Set Set.instHasSSubset	Matroid.IsCocircuit Matroid.delete Set Set.instSDiff	—	Matroid.isCocircuit_def Matroid.dual_delete Matroid.IsCircuit.contract_isCircuit isCircuit
of_contract 📖	mathematical	Matroid.IsCocircuit Matroid.contract	Matroid.IsCocircuit	—	Matroid.IsCircuit.of_delete Matroid.dual_contract Matroid.isCocircuit_def

Matroid.IsNonloop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contractElem_indep_iff 📖	mathematical	Matroid.IsNonloop	Matroid.Indep Matroid.contract Set Set.instSingletonSet Set.instMembership Set.instInsert	—	Matroid.Indep.contract_indep_iff indep Set.union_singleton
of_contract 📖	mathematical	Matroid.IsNonloop Matroid.contract	Matroid.IsNonloop	—	Matroid.indep_singleton Matroid.Indep.of_contract

Matroid.Spanning

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contract 📖	mathematical	Matroid.Spanning	Matroid.Spanning Matroid.contract Set Set.instSDiff	—	subset_ground Matroid.contract_spanning_iff' Set.disjoint_sdiff_left superset
contract_eq_loopyOn 📖	mathematical	Matroid.Spanning	Matroid.contract Matroid.loopyOn Set Set.instSDiff Matroid.E	—	Matroid.eq_loopyOn_iff_loops_eq Matroid.contract_loops_eq closure_eq

---

← Back to Index