IndepAxioms

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

Statistics

Metric	Count
Definitions `IndepMatroid`, `E`, `matroid`, `ofBdd`, `ofBddAugment`, `ofFinitary`, `ofFinitaryCardAugment`, `ofFinite`, `ofFinset`, `ofBase`, `ofExistsFiniteIsBase`, `ofExistsMatroid`, `ofIsBaseOfFinite`	13
Theorems `indep_aug`, `indep_empty`, `indep_maximal`, `indep_subset`, `instRankFiniteMatroidOfBdd`, `matroid_E`, `matroid_Indep`, `matroid_IsBase`, `matroid_indep_iff`, `ofBddAugment_E`, `ofBddAugment_indep`, `ofBddAugment_rankFinite`, `ofBdd_E`, `ofBdd_indep`, `ofFinitaryCardAugment_E`, `ofFinitaryCardAugment_finitary`, `ofFinitaryCardAugment_indep`, `ofFinitary_E`, `ofFinitary_finitary`, `ofFinitary_indep`, `ofFinite_E`, `ofFinite_finite`, `ofFinite_indep`, `ofFinset_E`, `ofFinset_indep`, `ofFinset_indep'`, `subset_ground`, `existsMaximalSubsetProperty_of_bdd`, `ofBaseOfFinite_finite`, `ofBase_E`, `ofExistsFiniteIsBase_E`, `ofExistsFiniteIsBase_isBase`, `ofExistsFiniteIsBase_rankFinite`, `ofExistsMatroid_E`, `ofIsBaseOfFinite_E`, `ofIsBaseOfFinite_isBase`	36
Total	49

IndepMatroid

Definitions

Name	Category	Theorems
`E` 📖	CompOp	10 math math: `subset_ground`, `Matroid.dualIndepMatroid_E`, `ofFinset_E`, `ofFinitaryCardAugment_E`, `matroid_E`, `ofBdd_E`, `ofBddAugment_E`, `Matroid.restrictIndepMatroid_E`, `ofFinitary_E`, `ofFinite_E`
`matroid` 📖	CompOp	9 math math: `matroid_IsBase`, `ofBddAugment_rankFinite`, `ofFinite_finite`, `ofFinitary_finitary`, `matroid_E`, `matroid_Indep`, `ofFinitaryCardAugment_finitary`, `matroid_indep_iff`, `instRankFiniteMatroidOfBdd`
`ofBdd` 📖	CompOp	3 math math: `ofBdd_indep`, `ofBdd_E`, `instRankFiniteMatroidOfBdd`
`ofBddAugment` 📖	CompOp	3 math math: `ofBddAugment_rankFinite`, `ofBddAugment_indep`, `ofBddAugment_E`
`ofFinitary` 📖	CompOp	3 math math: `ofFinitary_indep`, `ofFinitary_finitary`, `ofFinitary_E`
`ofFinitaryCardAugment` 📖	CompOp	3 math math: `ofFinitaryCardAugment_E`, `ofFinitaryCardAugment_indep`, `ofFinitaryCardAugment_finitary`
`ofFinite` 📖	CompOp	3 math math: `ofFinite_indep`, `ofFinite_finite`, `ofFinite_E`
`ofFinset` 📖	CompOp	3 math math: `ofFinset_indep`, `ofFinset_E`, `ofFinset_indep'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`indep_aug` 📖	mathematical	`Indep` `Maximal` `Set` `Set.instLE`	`Set.instMembership` `Set.instSDiff` `Set.instInsert`	—	—
`indep_empty` 📖	mathematical	—	`Indep` `Set` `Set.instEmptyCollection`	—	—
`indep_maximal` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`Matroid.ExistsMaximalSubsetProperty` `Indep`	—	—
`indep_subset` 📖	—	`Indep` `Set` `Set.instHasSubset`	—	—	—
`instRankFiniteMatroidOfBdd` 📖	mathematical	`Set` `Set.instEmptyCollection` `Set.instMembership` `Set.instSDiff` `Set.instInsert` `Set.instHasSubset` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `Set.encard` `ENat.instNatCast`	`Matroid.RankFinite` `matroid` `ofBdd`	—	`Matroid.exists_isBase` `Matroid.IsBase.rankFinite_of_finite` `Set.finite_of_encard_le_coe` `Matroid.IsBase.indep`
`matroid_E` 📖	mathematical	—	`Matroid.E` `matroid` `E`	—	—
`matroid_Indep` 📖	mathematical	—	`Matroid.Indep` `matroid` `Indep`	—	—
`matroid_IsBase` 📖	mathematical	—	`Matroid.IsBase` `matroid` `Maximal` `Set` `Set.instLE` `Indep`	—	—
`matroid_indep_iff` 📖	mathematical	—	`Matroid.Indep` `matroid` `Indep`	—	—
`ofBddAugment_E` 📖	mathematical	`Set` `Set.instEmptyCollection` `Set.instMembership` `Set.instInsert` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `Set.encard` `ENat.instNatCast` `Set.instHasSubset`	`E` `ofBddAugment`	—	—
`ofBddAugment_indep` 📖	mathematical	`Set` `Set.instEmptyCollection` `Set.instMembership` `Set.instInsert` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `Set.encard` `ENat.instNatCast` `Set.instHasSubset`	`Indep` `ofBddAugment`	—	—
`ofBddAugment_rankFinite` 📖	mathematical	`Set` `Set.instEmptyCollection` `Set.instMembership` `Set.instInsert` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `Set.encard` `ENat.instNatCast` `Set.instHasSubset`	`Matroid.RankFinite` `matroid` `ofBddAugment`	—	`ofBddAugment.eq_1` `instRankFiniteMatroidOfBdd`
`ofBdd_E` 📖	mathematical	`Set` `Set.instEmptyCollection` `Set.instMembership` `Set.instSDiff` `Set.instInsert` `Set.instHasSubset` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `Set.encard` `ENat.instNatCast`	`E` `ofBdd`	—	—
`ofBdd_indep` 📖	mathematical	`Set` `Set.instEmptyCollection` `Set.instMembership` `Set.instSDiff` `Set.instInsert` `Set.instHasSubset` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `Set.encard` `ENat.instNatCast`	`Indep` `ofBdd`	—	—
`ofFinitaryCardAugment_E` 📖	mathematical	`Set` `Set.instEmptyCollection` `Set.instMembership` `Set.instInsert` `Set.instHasSubset`	`E` `ofFinitaryCardAugment`	—	—
`ofFinitaryCardAugment_finitary` 📖	mathematical	`Set` `Set.instEmptyCollection` `Set.instMembership` `Set.instInsert` `Set.instHasSubset`	`Matroid.Finitary` `matroid` `ofFinitaryCardAugment`	—	—
`ofFinitaryCardAugment_indep` 📖	mathematical	`Set` `Set.instEmptyCollection` `Set.instMembership` `Set.instInsert` `Set.instHasSubset`	`Indep` `ofFinitaryCardAugment`	—	—
`ofFinitary_E` 📖	mathematical	`Set` `Set.instEmptyCollection` `Set.instMembership` `Set.instSDiff` `Set.instInsert` `Set.instHasSubset`	`E` `ofFinitary`	—	—
`ofFinitary_finitary` 📖	mathematical	`Set` `Set.instEmptyCollection` `Set.instMembership` `Set.instSDiff` `Set.instInsert` `Set.instHasSubset`	`Matroid.Finitary` `matroid` `ofFinitary`	—	—
`ofFinitary_indep` 📖	mathematical	`Set` `Set.instEmptyCollection` `Set.instMembership` `Set.instSDiff` `Set.instInsert` `Set.instHasSubset`	`Indep` `ofFinitary`	—	—
`ofFinite_E` 📖	mathematical	`Set` `Set.instEmptyCollection` `Set.instMembership` `Set.instInsert` `Set.instHasSubset`	`E` `ofFinite`	—	—
`ofFinite_finite` 📖	mathematical	`Set` `Set.instEmptyCollection` `Set.instMembership` `Set.instInsert` `Set.instHasSubset`	`Matroid.Finite` `matroid` `ofFinite`	—	—
`ofFinite_indep` 📖	mathematical	`Set` `Set.instEmptyCollection` `Set.instMembership` `Set.instInsert` `Set.instHasSubset`	`Indep` `ofFinite`	—	—
`ofFinset_E` 📖	mathematical	`Finset` `Finset.instEmptyCollection` `Finset.instMembership` `Finset.instInsert` `Set` `Set.instHasSubset` `SetLike.coe` `Finset.instSetLike`	`E` `ofFinset`	—	—
`ofFinset_indep` 📖	mathematical	`Finset` `Finset.instEmptyCollection` `Finset.instMembership` `Finset.instInsert` `Set` `Set.instHasSubset` `SetLike.coe` `Finset.instSetLike`	`Indep` `ofFinset`	—	`Set.Subset.rfl`
`ofFinset_indep'` 📖	mathematical	`Finset` `Finset.instEmptyCollection` `Finset.instMembership` `Finset.instInsert` `Set` `Set.instHasSubset` `SetLike.coe` `Finset.instSetLike`	`Indep` `ofFinset`	—	—
`subset_ground` 📖	mathematical	`Indep`	`Set` `Set.instHasSubset` `E`	—	—

Matroid

Definitions

Name	Category	Theorems
`ofBase` 📖	CompOp	1 math math: `ofBase_E`
`ofExistsFiniteIsBase` 📖	CompOp	3 math math: `ofExistsFiniteIsBase_rankFinite`, `ofExistsFiniteIsBase_E`, `ofExistsFiniteIsBase_isBase`
`ofExistsMatroid` 📖	CompOp	1 math math: `ofExistsMatroid_E`
`ofIsBaseOfFinite` 📖	CompOp	3 math math: `ofIsBaseOfFinite_isBase`, `ofIsBaseOfFinite_E`, `ofBaseOfFinite_finite`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`existsMaximalSubsetProperty_of_bdd` 📖	mathematical	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `Set.encard` `ENat.instNatCast`	`ExistsMaximalSubsetProperty`	—	`Set.finite_iff_bddAbove` `bddAbove_def` `Set.ncard_def` `ENat.toNat_coe` `Set.Finite.exists_maximalFor'` `instIsTransLe` `Eq.subset` `Set.instReflSubset` `Set.finite_of_encard_le_coe` `Set.eq_of_subset_of_ncard_le` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.ncard_le_ncard`
`ofBaseOfFinite_finite` 📖	mathematical	`ExchangeProperty` `Set` `Set.instHasSubset`	`Finite` `ofIsBaseOfFinite`	—	—
`ofBase_E` 📖	mathematical	`ExchangeProperty` `ExistsMaximalSubsetProperty` `Set` `Set.instHasSubset`	`E` `ofBase`	—	—
`ofExistsFiniteIsBase_E` 📖	mathematical	`Set.Finite` `ExchangeProperty` `Set` `Set.instHasSubset`	`E` `ofExistsFiniteIsBase`	—	—
`ofExistsFiniteIsBase_isBase` 📖	mathematical	`Set.Finite` `ExchangeProperty` `Set` `Set.instHasSubset`	`IsBase` `ofExistsFiniteIsBase`	—	—
`ofExistsFiniteIsBase_rankFinite` 📖	mathematical	`Set.Finite` `ExchangeProperty` `Set` `Set.instHasSubset`	`RankFinite` `ofExistsFiniteIsBase`	—	`IsBase.rankFinite_of_finite`
`ofExistsMatroid_E` 📖	mathematical	`E` `Indep`	`ofExistsMatroid`	—	—
`ofIsBaseOfFinite_E` 📖	mathematical	`ExchangeProperty` `Set` `Set.instHasSubset`	`E` `ofIsBaseOfFinite`	—	—
`ofIsBaseOfFinite_isBase` 📖	mathematical	`ExchangeProperty` `Set` `Set.instHasSubset`	`IsBase` `ofIsBaseOfFinite`	—	—

(root)

Definitions

Name	Category	Theorems
`IndepMatroid` 📖	CompData	—

---

← Back to Index