Order

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

Statistics

Metric	Count
Definitions IsMinor, IsStrictMinor, instPartialOrder, «term_, «term_≤m_»	5
Theorems of_isMinor, of_isMinor, of_isMinor, antisymm, eq_of_ground_subset, exists_eq_contract_delete_disjoint, le, refl, subset, trans, trans_isStrictMinor, of_isMinor, isMinor, lt, ne, not_isMinor, ssubset, trans, trans_isMinor, contract_delete_isMinor, isStrictMinor_iff_isMinor_ne, isStrictMinor_iff_isMinor_ssubset, isStrictMinor_irrefl, le_eq_isMinor, lt_eq_isStrictMinor	25
Total	30

Matroid

Definitions

Name	Category	Theorems
IsMinor 📖	MathDef	7 math math: IsStrictMinor.isMinor, IsMinor.refl, IsStrictMinor.not_isMinor, contract_delete_isMinor, isStrictMinor_iff_isMinor_ssubset, le_eq_isMinor, isStrictMinor_iff_isMinor_ne
IsStrictMinor 📖	MathDef	4 math math: lt_eq_isStrictMinor, isStrictMinor_irrefl, isStrictMinor_iff_isMinor_ssubset, isStrictMinor_iff_isMinor_ne
instPartialOrder 📖	CompOp	4 math math: lt_eq_isStrictMinor, IsStrictMinor.lt, IsMinor.le, le_eq_isMinor
«term_ 📖	CompOp	—
«term_≤m_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contract_delete_isMinor 📖	mathematical	—	IsMinor delete contract	—	—
isStrictMinor_iff_isMinor_ne 📖	mathematical	—	IsStrictMinor IsMinor	—	lt_iff_le_and_ne
isStrictMinor_iff_isMinor_ssubset 📖	mathematical	—	IsStrictMinor IsMinor Set Set.instHasSSubset E	—	IsStrictMinor.isMinor IsStrictMinor.ssubset HasSSubset.SSubset.ne Set.instIrreflSSubset IsMinor.antisymm
isStrictMinor_irrefl 📖	mathematical	—	IsStrictMinor	—	lt_irrefl
le_eq_isMinor 📖	mathematical	—	Matroid Preorder.toLE PartialOrder.toPreorder instPartialOrder IsMinor	—	—
lt_eq_isStrictMinor 📖	mathematical	—	Matroid Preorder.toLT PartialOrder.toPreorder instPartialOrder IsStrictMinor	—	—

Matroid.Dep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isMinor 📖	—	Matroid.Dep Set Set.instHasSubset Matroid.E Matroid.IsMinor	—	—	not_indep Matroid.Indep.of_isMinor

Matroid.Indep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isMinor 📖	—	Matroid.Indep Matroid.IsMinor	—	—	of_contract of_delete

Matroid.IsLoop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isMinor 📖	—	Matroid.IsLoop Set Set.instMembership Matroid.E Matroid.IsMinor	—	—	Matroid.singleton_dep Matroid.Dep.of_isMinor

Matroid.IsMinor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antisymm 📖	—	Matroid.IsMinor	—	—	eq_of_ground_subset subset
eq_of_ground_subset 📖	—	Matroid.IsMinor Set Set.instHasSubset Matroid.E	—	—	Matroid.contract_inter_ground_eq Disjoint.inter_eq Disjoint.symm Set.subset_diff Matroid.contract_ground Matroid.delete_ground Matroid.contract_empty Matroid.delete_inter_ground_eq Matroid.delete_empty
exists_eq_contract_delete_disjoint 📖	mathematical	Matroid.IsMinor	Set Set.instHasSubset Matroid.E Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Matroid.delete Matroid.contract	—	Set.inter_subset_right HasSubset.Subset.trans Set.instIsTransSubset Set.diff_subset Disjoint.mono_left Set.inter_subset_left Set.disjoint_sdiff_right Matroid.contract_inter_ground_eq Set.inter_diff_assoc Set.inter_assoc Set.inter_self
le 📖	mathematical	Matroid.IsMinor	Matroid Preorder.toLE PartialOrder.toPreorder Matroid.instPartialOrder	—	—
refl 📖	mathematical	—	Matroid.IsMinor	—	Matroid.contract_empty Matroid.delete_empty
subset 📖	mathematical	Matroid.IsMinor	Set Set.instHasSubset Matroid.E	—	HasSubset.Subset.trans Set.instIsTransSubset Set.diff_subset
trans 📖	—	Matroid.IsMinor	—	—	Matroid.contract_delete_contract_delete'
trans_isStrictMinor 📖	—	Matroid.IsMinor Matroid.IsStrictMinor	—	—	LE.le.trans_lt le

Matroid.IsNonloop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isMinor 📖	—	Matroid.IsNonloop Matroid.IsMinor	—	—	of_contract of_delete

Matroid.IsStrictMinor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isMinor 📖	mathematical	Matroid.IsStrictMinor	Matroid.IsMinor	—	LT.lt.le lt
lt 📖	mathematical	Matroid.IsStrictMinor	Matroid Preorder.toLT PartialOrder.toPreorder Matroid.instPartialOrder	—	—
ne 📖	—	Matroid.IsStrictMinor	—	—	LT.lt.ne lt
not_isMinor 📖	mathematical	Matroid.IsStrictMinor	Matroid.IsMinor	—	LT.lt.not_ge lt
ssubset 📖	mathematical	Matroid.IsStrictMinor	Set Set.instHasSSubset Matroid.E	—	HasSubset.Subset.ssubset_of_ne Set.instIsNonstrictStrictOrderSubsetSSubset Set.instAntisymmSubset Matroid.IsMinor.subset isMinor ne Matroid.IsMinor.eq_of_ground_subset Eq.subset Set.instReflSubset
trans 📖	—	Matroid.IsStrictMinor	—	—	LT.lt.trans lt
trans_isMinor 📖	—	Matroid.IsStrictMinor Matroid.IsMinor	—	—	LT.lt.trans_le lt

---

← Back to Index