Restrict

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

Statistics

Metric	Count
Definitions `IsRestriction`, `IsStrictRestriction`, `Matroidᵣ`, `toMatroid`, `instCoeOutMatroidᵣ`, `instPartialOrderMatroidᵣ`, `restrict`, `restrictIndepMatroid`, `«term_, «term_↾_», «term_≤r_»`	11
Theorems `dep_isRestriction`, `of_isRestriction`, `augment`, `augment_finset`, `exists_insert_of_not_isBasis`, `exists_isBasis_subset_union_isBasis`, `indep_isRestriction`, `indep_restrict_of_subset`, `of_isRestriction`, `of_restrict`, `isBasis_of_isRestriction`, `encard_eq_encard`, `isBase_restrict`, `encard_eq_encard`, `eq_exchange_of_diff_eq_singleton`, `exchange`, `isBase_of_isBase_subset`, `isBase_restrict`, `isBasis_isRestriction`, `isBasis_of_isBasis_of_subset_of_subset`, `isBasis_restrict_of_subset`, `of_isRestriction`, `restrict_isBase`, `transfer`, `antisymm`, `base_iff`, `dep_iff`, `eq_or_isStrictRestriction`, `eq_restrict`, `exists_eq_restrict`, `finitary`, `finite`, `indep_iff`, `isBasis_iff`, `isStrictRestriction_of_ground_ne`, `isStrictRestriction_of_ne`, `of_subset`, `rankFinite`, `refl`, `subset`, `trans`, `eq_restrict`, `exists_eq_restrict`, `irrefl`, `isRestriction`, `ne`, `of_ssubset`, `ssubset`, `coe_inj`, `ext`, `ext_iff`, `le_iff`, `lt_iff`, `finite_setOf_isRestriction`, `isBase_restrict_iff`, `isBase_restrict_iff'`, `isBasis'_iff_isBasis_restrict_univ`, `isBasis'_restrict_iff`, `isBasis_restrict_iff`, `isBasis_restrict_iff'`, `isRestriction_iff_exists`, `ofMatroid_le_iff`, `ofMatroid_lt_iff`, `restrictIndepMatroid_E`, `restrictIndepMatroid_Indep`, `restrict_dep_iff`, `restrict_eq_restrict_iff`, `restrict_eq_self_iff`, `restrict_finitary`, `restrict_finite`, `restrict_ground_eq`, `restrict_ground_eq_self`, `restrict_idem`, `restrict_indep_iff`, `restrict_isRestriction`, `restrict_isStrictRestriction`, `restrict_rankFinite`, `restrict_restrict_eq`	78
Total	89

Matroid

Definitions

Name	Category	Theorems
`IsRestriction` 📖	MathDef	11 math math: `IsRestriction.of_subset`, `IsRestriction.refl`, `Matroidᵣ.le_iff`, `IsStrictRestriction.isRestriction`, `restrict_isRestriction`, `removeLoops_isRestriction`, `ofMatroid_le_iff`, `finite_setOf_isRestriction`, `delete_isRestriction`, `isRestriction_iff_exists`, `isRestriction_iff_exists_eq_delete`
`IsStrictRestriction` 📖	MathDef	8 math math: `IsRestriction.isStrictRestriction_of_ground_ne`, `restrict_isStrictRestriction`, `IsRestriction.eq_or_isStrictRestriction`, `IsStrictRestriction.irrefl`, `ofMatroid_lt_iff`, `IsStrictRestriction.of_ssubset`, `IsRestriction.isStrictRestriction_of_ne`, `Matroidᵣ.lt_iff`
`Matroidᵣ` 📖	CompData	4 math math: `Matroidᵣ.le_iff`, `ofMatroid_le_iff`, `ofMatroid_lt_iff`, `Matroidᵣ.lt_iff`
`instCoeOutMatroidᵣ` 📖	CompOp	—
`instPartialOrderMatroidᵣ` 📖	CompOp	4 math math: `Matroidᵣ.le_iff`, `ofMatroid_le_iff`, `ofMatroid_lt_iff`, `Matroidᵣ.lt_iff`
`restrict` 📖	CompOp	73 math math: `IsBasis.isBase_restrict`, `isBase_restrict_iff'`, `fundCircuit_restrict`, `Spanning.eRank_restrict`, `restrict_eq_self_iff`, `IsRestriction.of_subset`, `cRk_restrict_subset`, `restrict_loops_eq`, `restrict_loops_eq'`, `IsRestriction.exists_eq_restrict`, `isBasis_restrict_iff`, `loopyOn_restrict`, `isBasis'_restrict_iff`, `isNonloop_iff_restrict_of_mem`, `delete_compl`, `removeLoops_restrict_eq_restrict`, `restrict_spanning_iff`, `restrict_rankFinite`, `Indep.restrict_eq_freeOn`, `IsBasis'.isBase_restrict`, `restrict_eq_restrict_iff`, `restrict_closure_eq`, `restrict_dep_iff`, `restrict_ground_eq`, `uniqueBaseOn_restrict'`, `restrict_spanning_iff'`, `restrict_isRestriction`, `restrict_isCircuit_iff`, `restrict_isColoop_iff`, `freeOn_restrict`, `restrict_empty`, `eRank_restrict`, `IsRkFinite.rankFinite`, `delete_eq_restrict`, `removeLoops_eq_restrict`, `restrict_isNonloop_iff`, `map_val_restrictSubtype_eq`, `restrict_eq_freeOn_iff`, `restrict_ground_eq_self`, `fundCircuit_restrict_univ`, `cRank_restrict`, `eq_restrict_removeLoops`, `restrict_eRk_eq'`, `IsBasis.isBasis_restrict_of_subset`, `isBasis_restrict_iff'`, `isRestriction_iff_exists`, `Indep.indep_restrict_of_subset`, `restrict_isStrictRestriction`, `restrict_eRk_eq`, `restrict_finite`, `Spanning.isBase_restrict_iff`, `IsStrictRestriction.eq_restrict`, `restrict_finitary`, `restrict_closure_eq'`, `restrict_contract_eq_contract_restrict`, `IsCircuit.isCircuit_restrict_of_subset`, `restrict_indep_iff`, `restrict_subset_loops_eq`, `restrict_restrict_eq`, `isBase_restrict_iff`, `restrict_compl`, `contract_restrict_eq_restrict_contract`, `isBasis'_iff_isBasis_restrict_univ`, `uniqueBaseOn_restrict`, `IsBasis.restrict_isBase`, `invariantCardinalRank_restrict`, `IsRestriction.eq_restrict`, `restrict_isLoop_iff`, `IsStrictRestriction.of_ssubset`, `restrict_univ_removeLoops_eq`, `restrict_idem`, `IsStrictRestriction.exists_eq_restrict`, `cRk_restrict`
`restrictIndepMatroid` 📖	CompOp	2 math math: `restrictIndepMatroid_Indep`, `restrictIndepMatroid_E`
`«term_` `📖`	CompOp	—
`«term_↾_»` 📖	CompOp	—
`«term_≤r_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_setOf_isRestriction` 📖	mathematical	—	`Set.Finite` `Matroid` `setOf` `IsRestriction`	—	`Set.Finite.subset` `Set.Finite.image` `Set.Finite.finite_subsets` `ground_finite`
`isBase_restrict_iff` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`IsBase` `restrict` `IsBasis`	—	—
`isBase_restrict_iff'` 📖	mathematical	—	`IsBase` `restrict` `IsBasis'`	—	—
`isBasis'_iff_isBasis_restrict_univ` 📖	mathematical	—	`IsBasis'` `IsBasis` `restrict` `Set.univ`	—	`isBasis_restrict_iff'` `isBasis'_iff_isBasis_inter_ground` `Set.subset_univ`
`isBasis'_restrict_iff` 📖	mathematical	—	`IsBasis'` `restrict` `Set` `Set.instInter` `Set.instHasSubset`	—	—
`isBasis_restrict_iff` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`IsBasis` `restrict`	—	`isBasis_restrict_iff'` `isBasis'_iff_isBasis_inter_ground` `isBasis'_iff_isBasis`
`isBasis_restrict_iff'` 📖	mathematical	—	`IsBasis` `restrict` `Set` `Set.instInter` `E` `Set.instHasSubset`	—	`isBasis_iff_isBasis'_subset_ground` `isBasis'_restrict_iff` `restrict_ground_eq` `isBasis'_iff_isBasis_inter_ground` `Set.inter_eq_self_of_subset_left` `HasSubset.Subset.trans` `Set.instIsTransSubset` `IsBasis'.subset`
`isRestriction_iff_exists` 📖	mathematical	—	`IsRestriction` `Set` `Set.instHasSubset` `E` `restrict`	—	`IsRestriction.exists_eq_restrict` `restrict_isRestriction`
`ofMatroid_le_iff` 📖	mathematical	—	`Matroidᵣ` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderMatroidᵣ` `Matroidᵣ.ofMatroid` `IsRestriction`	—	—
`ofMatroid_lt_iff` 📖	mathematical	—	`Matroidᵣ` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderMatroidᵣ` `Matroidᵣ.ofMatroid` `IsStrictRestriction`	—	—
`restrictIndepMatroid_E` 📖	mathematical	—	`IndepMatroid.E` `restrictIndepMatroid`	—	—
`restrictIndepMatroid_Indep` 📖	mathematical	—	`IndepMatroid.Indep` `restrictIndepMatroid` `Indep` `Set` `Set.instHasSubset`	—	—
`restrict_dep_iff` 📖	mathematical	—	`Dep` `restrict` `Indep` `Set` `Set.instHasSubset`	—	`Dep.eq_1` `restrict_indep_iff` `restrict_ground_eq`
`restrict_eq_restrict_iff` 📖	mathematical	—	`restrict` `Indep`	—	`restrict_indep_iff` `ext_indep`
`restrict_eq_self_iff` 📖	mathematical	—	`restrict` `E`	—	`restrict_ground_eq_self`
`restrict_finitary` 📖	mathematical	—	`Finitary` `restrict`	—	`indep_iff_forall_finite_subset_indep` `Set.singleton_subset_iff` `Set.toFinite` `Finite.of_fintype`
`restrict_finite` 📖	mathematical	—	`Finite` `restrict`	—	—
`restrict_ground_eq` 📖	mathematical	—	`E` `restrict`	—	—
`restrict_ground_eq_self` 📖	mathematical	—	`restrict` `E`	—	`ext_indep`
`restrict_idem` 📖	mathematical	—	`restrict`	—	`restrict_restrict_eq` `Set.Subset.rfl`
`restrict_indep_iff` 📖	mathematical	—	`Indep` `restrict` `Set` `Set.instHasSubset`	—	—
`restrict_isRestriction` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`IsRestriction` `restrict`	—	—
`restrict_isStrictRestriction` 📖	mathematical	`Set` `Set.instHasSSubset` `E`	`IsStrictRestriction` `restrict`	—	`IsRestriction.isStrictRestriction_of_ne` `restrict_isRestriction` `HasSSubset.SSubset.subset` `Set.instIsNonstrictStrictOrderSubsetSSubset` `HasSSubset.SSubset.ne` `Set.instIrreflSSubset` `restrict_ground_eq`
`restrict_rankFinite` 📖	mathematical	—	`RankFinite` `restrict`	—	`exists_isBase` `IsBase.rankFinite_of_finite` `Indep.finite` `Indep.of_restrict` `IsBase.indep`
`restrict_restrict_eq` 📖	mathematical	`Set` `Set.instHasSubset`	`restrict`	—	`ext_indep` `HasSubset.Subset.trans` `Set.instIsTransSubset`

Matroid.Dep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dep_isRestriction` 📖	—	`Matroid.Dep` `Matroid.IsRestriction` `Set` `Set.instHasSubset` `Matroid.E`	—	—	`not_indep`
`of_isRestriction` 📖	—	`Matroid.Dep` `Matroid.IsRestriction`	—	—	`Matroid.restrict_dep_iff` `HasSubset.Subset.trans` `Set.instIsTransSubset`

Matroid.Indep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`augment` 📖	mathematical	`Matroid.Indep` `ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `Set.encard`	`Set` `Set.instMembership` `Set.instSDiff` `Set.instInsert`	—	`isBasis_iff_forall_insert_dep` `Set.subset_union_left` `Set.union_diff_left` `subset_ground` `Mathlib.Tactic.Push.not_and_eq` `subset_isBasis_of_subset` `Set.subset_union_right` `LT.lt.not_ge` `Matroid.IsBasis.encard_eq_encard` `Set.encard_mono`
`augment_finset` 📖	mathematical	`Matroid.Indep` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.card`	`Finset.instMembership` `Set` `Set.instInsert`	—	`augment` `Set.encard_eq_coe_toFinset_card` `Finset.toFinset_coe` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass`
`exists_insert_of_not_isBasis` 📖	mathematical	`Matroid.Indep` `Set` `Set.instHasSubset` `Matroid.IsBasis`	`Set.instMembership` `Set.instSDiff` `Set.instInsert`	—	`exists_insert_of_not_isBase` `indep_restrict_of_subset` `Matroid.isBase_restrict_iff` `Matroid.IsBasis.subset_ground` `Matroid.restrict_indep_iff`
`exists_isBasis_subset_union_isBasis` 📖	mathematical	`Matroid.Indep` `Set` `Set.instHasSubset` `Matroid.IsBasis`	`Set.instUnion`	—	`exists_isBase_subset_union_isBase` `indep_restrict_of_subset` `Matroid.IsBasis.isBase_restrict` `Matroid.isBase_restrict_iff` `Matroid.IsBasis.subset_ground`
`indep_isRestriction` 📖	—	`Matroid.Indep` `Matroid.IsRestriction` `Set` `Set.instHasSubset` `Matroid.E`	—	—	—
`indep_restrict_of_subset` 📖	mathematical	`Matroid.Indep` `Set` `Set.instHasSubset`	`Matroid.restrict`	—	`Matroid.restrict_indep_iff`
`of_isRestriction` 📖	—	`Matroid.Indep` `Matroid.IsRestriction`	—	—	`of_restrict`
`of_restrict` 📖	—	`Matroid.Indep` `Matroid.restrict`	—	—	`Matroid.restrict_indep_iff`

Matroid.IsBase

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBasis_of_isRestriction` 📖	mathematical	`Matroid.IsBase` `Matroid.IsRestriction`	`Matroid.IsBasis` `Matroid.E`	—	`Matroid.isBase_restrict_iff`

Matroid.IsBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`encard_eq_encard` 📖	mathematical	`Matroid.IsBasis`	`Set.encard`	—	`Matroid.IsBasis'.encard_eq_encard` `isBasis'`
`eq_exchange_of_diff_eq_singleton` 📖	mathematical	`Matroid.IsBasis` `Set` `Set.instSDiff` `Set.instSingletonSet`	`Set.instMembership` `Set.instInsert`	—	`Matroid.IsBase.eq_exchange_of_diff_eq_singleton` `Matroid.isBase_restrict_iff` `subset_ground`
`exchange` 📖	mathematical	`Matroid.IsBasis` `Set` `Set.instMembership` `Set.instSDiff`	`Set.instInsert` `Set.instSingletonSet`	—	`Matroid.IsBase.exchange` `restrict_isBase` `Matroid.isBase_restrict_iff` `subset_ground`
`isBase_of_isBase_subset` 📖	—	`Matroid.IsBasis` `Matroid.IsBase` `Set` `Set.instHasSubset`	—	—	`Matroid.IsBase.isBase_of_isBasis_superset`
`isBase_restrict` 📖	mathematical	`Matroid.IsBasis`	`Matroid.IsBase` `Matroid.restrict`	—	`Matroid.isBase_restrict_iff` `subset_ground`
`isBasis_isRestriction` 📖	—	`Matroid.IsBasis` `Matroid.IsRestriction` `Set` `Set.instHasSubset` `Matroid.E`	—	—	`Matroid.isBasis_restrict_iff`
`isBasis_of_isBasis_of_subset_of_subset` 📖	—	`Matroid.IsBasis` `Set` `Set.instHasSubset`	—	—	`isBasis_subset` `Set.subset_inter` `subset` `Set.inter_subset_left` `Set.inter_subset_right` `transfer`
`isBasis_restrict_of_subset` 📖	mathematical	`Matroid.IsBasis` `Set` `Set.instHasSubset`	`Matroid.restrict`	—	`Matroid.isBase_restrict_iff` `Matroid.restrict_restrict_eq` `subset_ground`
`of_isRestriction` 📖	—	`Matroid.IsBasis` `Matroid.IsRestriction`	—	—	`Matroid.isBasis_restrict_iff`
`restrict_isBase` 📖	mathematical	`Matroid.IsBasis`	`Matroid.IsBase` `Matroid.restrict`	—	`Matroid.isBase_restrict_iff` `subset_ground`
`transfer` 📖	—	`Matroid.IsBasis` `Set` `Set.instHasSubset`	—	—	`Matroid.isBase_restrict_iff` `subset_ground` `Matroid.IsBase.isBase_of_isBasis_superset` `subset` `isBasis_restrict_of_subset`

Matroid.IsBasis'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`encard_eq_encard` 📖	mathematical	`Matroid.IsBasis'`	`Set.encard`	—	`Matroid.IsBase.encard_eq_encard_of_isBase` `Matroid.isBase_restrict_iff'`
`isBase_restrict` 📖	mathematical	`Matroid.IsBasis'`	`Matroid.IsBase` `Matroid.restrict`	—	`Matroid.isBase_restrict_iff'`

Matroid.IsRestriction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antisymm` 📖	—	`Matroid.IsRestriction`	—	—	`LE.le.antisymm` `Matroid.ofMatroid_le_iff`
`base_iff` 📖	mathematical	`Matroid.IsRestriction`	`Matroid.IsBase` `Matroid.IsBasis` `Matroid.E`	—	`Matroid.IsBase.isBasis_of_isRestriction` `eq_restrict` `Matroid.IsBasis.restrict_isBase`
`dep_iff` 📖	mathematical	`Matroid.IsRestriction`	`Matroid.Dep` `Set` `Set.instHasSubset` `Matroid.E`	—	`Matroid.Dep.of_isRestriction` `Matroid.Dep.subset_ground` `Matroid.Dep.dep_isRestriction`
`eq_or_isStrictRestriction` 📖	mathematical	`Matroid.IsRestriction`	`Matroid.IsStrictRestriction`	—	`eq_or_lt_of_le` `Matroid.ofMatroid_le_iff`
`eq_restrict` 📖	mathematical	`Matroid.IsRestriction`	`Matroid.restrict` `Matroid.E`	—	`Matroid.restrict_ground_eq`
`exists_eq_restrict` 📖	mathematical	`Matroid.IsRestriction`	`Set` `Set.instHasSubset` `Matroid.E` `Matroid.restrict`	—	—
`finitary` 📖	mathematical	`Matroid.IsRestriction`	`Matroid.Finitary`	—	`Matroid.restrict_finitary`
`finite` 📖	mathematical	`Matroid.IsRestriction`	`Matroid.Finite`	—	`Matroid.restrict_finite` `Set.Finite.subset` `Matroid.ground_finite`
`indep_iff` 📖	mathematical	`Matroid.IsRestriction`	`Matroid.Indep` `Set` `Set.instHasSubset` `Matroid.E`	—	`Matroid.Indep.of_isRestriction` `Matroid.Indep.subset_ground` `Matroid.Indep.indep_isRestriction`
`isBasis_iff` 📖	mathematical	`Matroid.IsRestriction`	`Matroid.IsBasis` `Set` `Set.instHasSubset` `Matroid.E`	—	`Matroid.IsBasis.of_isRestriction` `Matroid.IsBasis.subset_ground` `Matroid.IsBasis.isBasis_isRestriction`
`isStrictRestriction_of_ground_ne` 📖	mathematical	`Matroid.IsRestriction`	`Matroid.IsStrictRestriction`	—	`eq_restrict` `Matroid.restrict_isStrictRestriction` `HasSubset.Subset.ssubset_of_ne` `Set.instIsNonstrictStrictOrderSubsetSSubset` `Set.instAntisymmSubset` `subset`
`isStrictRestriction_of_ne` 📖	mathematical	`Matroid.IsRestriction`	`Matroid.IsStrictRestriction`	—	`antisymm`
`of_subset` 📖	mathematical	`Set` `Set.instHasSubset`	`Matroid.IsRestriction` `Matroid.restrict`	—	`Matroid.restrict_restrict_eq` `Matroid.restrict_isRestriction`
`rankFinite` 📖	mathematical	`Matroid.IsRestriction`	`Matroid.RankFinite`	—	`Matroid.restrict_rankFinite`
`refl` 📖	mathematical	—	`Matroid.IsRestriction`	—	`le_refl`
`subset` 📖	mathematical	`Matroid.IsRestriction`	`Set` `Set.instHasSubset` `Matroid.E`	—	—
`trans` 📖	—	`Matroid.IsRestriction`	—	—	`le_trans`

Matroid.IsStrictRestriction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_restrict` 📖	mathematical	`Matroid.IsStrictRestriction`	`Matroid.restrict` `Matroid.E`	—	`Matroid.IsRestriction.eq_restrict` `isRestriction`
`exists_eq_restrict` 📖	mathematical	`Matroid.IsStrictRestriction`	`Set` `Set.instHasSSubset` `Matroid.E` `Matroid.restrict`	—	`ssubset` `eq_restrict`
`irrefl` 📖	mathematical	—	`Matroid.IsStrictRestriction`	—	`ne`
`isRestriction` 📖	mathematical	`Matroid.IsStrictRestriction`	`Matroid.IsRestriction`	—	—
`ne` 📖	—	`Matroid.IsStrictRestriction`	—	—	`Matroid.ofMatroid_lt_iff`
`of_ssubset` 📖	mathematical	`Set` `Set.instHasSSubset`	`Matroid.IsStrictRestriction` `Matroid.restrict`	—	`Matroid.IsRestriction.isStrictRestriction_of_ground_ne` `Matroid.IsRestriction.of_subset` `HasSSubset.SSubset.subset` `Set.instIsNonstrictStrictOrderSubsetSSubset` `HasSSubset.SSubset.ne` `Set.instIrreflSSubset`
`ssubset` 📖	mathematical	`Matroid.IsStrictRestriction`	`Set` `Set.instHasSSubset` `Matroid.E`	—	`HasSubset.Subset.ssubset_of_ne` `Set.instIsNonstrictStrictOrderSubsetSSubset` `Set.instAntisymmSubset` `Matroid.IsRestriction.subset` `isRestriction` `Set.Subset.rfl` `Matroid.restrict_idem` `Matroid.restrict_ground_eq_self`

Matroid.Matroidᵣ

Definitions

Name	Category	Theorems
`toMatroid` 📖	CompOp	4 math math: `le_iff`, `ext_iff`, `coe_inj`, `lt_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_inj` 📖	mathematical	—	`toMatroid`	—	`ext_iff`
`ext` 📖	—	`toMatroid`	—	—	—
`ext_iff` 📖	mathematical	—	`toMatroid`	—	`ext`
`le_iff` 📖	mathematical	—	`Matroid.Matroidᵣ` `Preorder.toLE` `PartialOrder.toPreorder` `Matroid.instPartialOrderMatroidᵣ` `Matroid.IsRestriction` `toMatroid`	—	—
`lt_iff` 📖	mathematical	—	`Matroid.Matroidᵣ` `Preorder.toLT` `PartialOrder.toPreorder` `Matroid.instPartialOrderMatroidᵣ` `Matroid.IsStrictRestriction` `toMatroid`	—	—

---

← Back to Index