Constructions

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

Statistics

Metric	Count
Definitions `emptyOn`, `freeOn`, `loopyOn`, `uniqueBaseOn`	4
Theorems `loopyOn_finite`, `restrict_eq_freeOn`, `emptyOn_dual_eq`, `emptyOn_ground`, `emptyOn_indep_iff`, `emptyOn_isBase_iff`, `empty_isBase_iff`, `eq_emptyOn`, `eq_emptyOn_or_nonempty`, `eq_freeOn_iff`, `eq_loopyOn_iff`, `eq_loopyOn_or_rankPos`, `finite_emptyOn`, `freeOn_dual_eq`, `freeOn_empty`, `freeOn_finitary`, `freeOn_ground`, `freeOn_indep`, `freeOn_indep_iff`, `freeOn_isBase_iff`, `freeOn_isBasis'_iff`, `freeOn_isBasis_iff`, `freeOn_rankPos`, `freeOn_restrict`, `ground_eq_empty_iff`, `ground_indep_iff_eq_freeOn`, `loopyOn_dual_eq`, `loopyOn_empty`, `loopyOn_ground`, `loopyOn_indep_iff`, `loopyOn_isBase_iff`, `loopyOn_isBasis_iff`, `loopyOn_rankFinite`, `loopyOn_restrict`, `not_rankPos_iff`, `restrict_empty`, `restrict_eq_freeOn_iff`, `uniqueBaseOn_dual_eq`, `uniqueBaseOn_empty`, `uniqueBaseOn_finitary`, `uniqueBaseOn_ground`, `uniqueBaseOn_indep_iff`, `uniqueBaseOn_indep_iff'`, `uniqueBaseOn_inter_ground_eq`, `uniqueBaseOn_inter_isBasis`, `uniqueBaseOn_isBase_iff`, `uniqueBaseOn_isBasis_iff`, `uniqueBaseOn_rankFinite`, `uniqueBaseOn_rankPos`, `uniqueBaseOn_restrict`, `uniqueBaseOn_restrict'`, `uniqueBaseOn_self`	52
Total	56

Matroid

Definitions

Name	Category	Theorems
`emptyOn` 📖	CompOp	15 math math: `comap_emptyOn`, `freeOn_empty`, `eRank_emptyOn`, `eq_emptyOn`, `emptyOn_ground`, `loopyOn_empty`, `eq_emptyOn_or_nonempty`, `emptyOn_closure_eq`, `restrict_empty`, `emptyOn_indep_iff`, `finite_emptyOn`, `emptyOn_isBase_iff`, `ground_eq_empty_iff`, `emptyOn_dual_eq`, `map_emptyOn`
`freeOn` 📖	CompOp	22 math math: `uniqueBaseOn_self`, `freeOn_not_isLoop`, `freeOn_isBasis_iff`, `eRank_freeOn`, `freeOn_empty`, `Indep.restrict_eq_freeOn`, `freeOn_finitary`, `freeOn_isBasis'_iff`, `freeOn_dual_eq`, `freeOn_indep`, `freeOn_restrict`, `freeOn_isNonloop_iff`, `freeOn_ground`, `restrict_eq_freeOn_iff`, `freeOn_closure_eq`, `ground_indep_iff_eq_freeOn`, `freeOn_rankPos`, `eRk_freeOn`, `loopyOn_dual_eq`, `freeOn_isBase_iff`, `eq_freeOn_iff`, `freeOn_indep_iff`
`loopyOn` 📖	CompOp	30 math math: `eRank_loopyOn`, `loopyOn_spanning_iff`, `comap_loopyOn`, `exists_of_eRank_eq_zero`, `loopyOn_restrict`, `loopyOn_indep_iff`, `loopyOn_isLoop_iff`, `Spanning.contract_eq_loopyOn`, `loopyOn_empty`, `freeOn_dual_eq`, `loopyOn_isBasis_iff`, `loopyOn_isLoopless_iff`, `uniqueBaseOn_empty`, `eRk_loopyOn`, `Finite.loopyOn_finite`, `loopyOn_isBase_iff`, `eRank_eq_zero_iff`, `loopyOn_rankFinite`, `loopyOn_closure_eq`, `loopyOn_dual_eq`, `closure_empty_eq_ground_iff`, `not_rankPos_iff`, `eq_loopyOn_or_rankPos`, `restrict_subset_loops_eq`, `eq_loopyOn_iff`, `eq_loopyOn_iff_eRank`, `eq_loopyOn_iff_loops_eq`, `empty_isBase_iff`, `eq_loopyOn_iff_loops`, `loopyOn_ground`
`uniqueBaseOn` 📖	CompOp	18 math math: `uniqueBaseOn_self`, `uniqueBaseOn_isLoop_iff`, `uniqueBaseOn_inter_ground_eq`, `uniqueBaseOn_indep_iff'`, `uniqueBaseOn_dual_eq`, `uniqueBaseOn_restrict'`, `uniqueBaseOn_ground`, `uniqueBaseOn_rankPos`, `uniqueBaseOn_empty`, `uniqueBaseOn_finitary`, `uniqueBaseOn_inter_isBasis`, `uniqueBaseOn_isNonloop_iff`, `uniqueBaseOn_isBasis_iff`, `uniqueBaseOn_indep_iff`, `uniqueBaseOn_restrict`, `uniqueBaseOn_rankFinite`, `uniqueBaseOn_closure_eq`, `uniqueBaseOn_isBase_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`emptyOn_dual_eq` 📖	mathematical	—	`dual` `emptyOn`	—	`ground_eq_empty_iff`
`emptyOn_ground` 📖	mathematical	—	`E` `emptyOn` `Set` `Set.instEmptyCollection`	—	—
`emptyOn_indep_iff` 📖	mathematical	—	`Indep` `emptyOn` `Set` `Set.instEmptyCollection`	—	—
`emptyOn_isBase_iff` 📖	mathematical	—	`IsBase` `emptyOn` `Set` `Set.instEmptyCollection`	—	—
`empty_isBase_iff` 📖	mathematical	—	`IsBase` `Set` `Set.instEmptyCollection` `loopyOn` `E`	—	`Indep.subset_ground`
`eq_emptyOn` 📖	mathematical	—	`emptyOn`	—	`ground_eq_empty_iff` `Set.eq_empty_of_isEmpty` `instIsEmptySubtype`
`eq_emptyOn_or_nonempty` 📖	mathematical	—	`emptyOn` `Nonempty`	—	`ground_eq_empty_iff` `Set.eq_empty_or_nonempty`
`eq_freeOn_iff` 📖	mathematical	—	`freeOn` `E` `Indep`	—	`Set.instReflSubset` `Indep.subset`
`eq_loopyOn_iff` 📖	mathematical	—	`loopyOn` `E` `Set` `Set.instEmptyCollection`	—	—
`eq_loopyOn_or_rankPos` 📖	mathematical	—	`loopyOn` `E` `RankPos`	—	`empty_isBase_iff` `rankPos_iff` `em`
`finite_emptyOn` 📖	mathematical	—	`Finite` `emptyOn`	—	`Set.finite_empty`
`freeOn_dual_eq` 📖	mathematical	—	`dual` `freeOn` `loopyOn`	—	`freeOn.eq_1` `dual_dual`
`freeOn_empty` 📖	mathematical	—	`freeOn` `Set` `Set.instEmptyCollection` `emptyOn`	—	`loopyOn_empty` `emptyOn_dual_eq`
`freeOn_finitary` 📖	mathematical	—	`Finitary` `freeOn`	—	—
`freeOn_ground` 📖	mathematical	—	`E` `freeOn`	—	—
`freeOn_indep` 📖	mathematical	`Set` `Set.instHasSubset`	`Indep` `freeOn`	—	`freeOn_indep_iff`
`freeOn_indep_iff` 📖	mathematical	—	`Indep` `freeOn` `Set` `Set.instHasSubset`	—	—
`freeOn_isBase_iff` 📖	mathematical	—	`IsBase` `freeOn`	—	`Set.instReflSubset` `Set.instAntisymmSubset`
`freeOn_isBasis'_iff` 📖	mathematical	—	`IsBasis'` `freeOn` `Set` `Set.instInter`	—	`isBasis'_iff_isBasis_inter_ground` `freeOn_isBasis_iff` `freeOn_ground` `Set.inter_subset_right`
`freeOn_isBasis_iff` 📖	mathematical	—	`IsBasis` `freeOn` `Set` `Set.instHasSubset`	—	`Indep.eq_of_isBasis` `freeOn_indep` `IsBasis.subset_ground` `Indep.isBasis_self`
`freeOn_rankPos` 📖	mathematical	`Set.Nonempty`	`RankPos` `freeOn`	—	`Set.Nonempty.ne_empty`
`freeOn_restrict` 📖	mathematical	`Set` `Set.instHasSubset`	`restrict` `freeOn`	—	`Set.instReflSubset`
`ground_eq_empty_iff` 📖	mathematical	—	`E` `Set` `Set.instEmptyCollection` `emptyOn`	—	—
`ground_indep_iff_eq_freeOn` 📖	mathematical	—	`Indep` `E` `freeOn`	—	—
`loopyOn_dual_eq` 📖	mathematical	—	`dual` `loopyOn` `freeOn`	—	—
`loopyOn_empty` 📖	mathematical	—	`loopyOn` `Set` `Set.instEmptyCollection` `emptyOn`	—	`ground_eq_empty_iff` `loopyOn_ground`
`loopyOn_ground` 📖	mathematical	—	`E` `loopyOn`	—	—
`loopyOn_indep_iff` 📖	mathematical	—	`Indep` `loopyOn` `Set` `Set.instEmptyCollection`	—	`Set.empty_subset`
`loopyOn_isBase_iff` 📖	mathematical	—	`IsBase` `loopyOn` `Set` `Set.instEmptyCollection`	—	—
`loopyOn_isBasis_iff` 📖	mathematical	—	`IsBasis` `loopyOn` `Set` `Set.instEmptyCollection` `Set.instHasSubset`	—	`loopyOn_indep_iff` `IsBasis.indep` `IsBasis.subset_ground` `isBasis_iff`
`loopyOn_rankFinite` 📖	mathematical	—	`RankFinite` `loopyOn`	—	—
`loopyOn_restrict` 📖	mathematical	—	`restrict` `loopyOn`	—	`ext_indep`
`not_rankPos_iff` 📖	mathematical	—	`RankPos` `loopyOn` `E`	—	`rankPos_iff` `not_iff_comm` `empty_isBase_iff`
`restrict_empty` 📖	mathematical	—	`restrict` `Set` `Set.instEmptyCollection` `emptyOn`	—	—
`restrict_eq_freeOn_iff` 📖	mathematical	—	`restrict` `freeOn` `Indep`	—	`eq_freeOn_iff` `restrict_ground_eq` `restrict_indep_iff` `Set.Subset.rfl`
`uniqueBaseOn_dual_eq` 📖	mathematical	—	`dual` `uniqueBaseOn` `Set` `Set.instSDiff`	—	`uniqueBaseOn_inter_ground_eq` `ext_isBase` `dual_isBase_iff` `uniqueBaseOn_isBase_iff` `Set.inter_subset_right` `Set.diff_subset` `uniqueBaseOn_ground` `Set.diff_diff_cancel_left` `Set.diff_inter_self_eq_diff` `Set.inter_comm` `sdiff_sdiff_right_self`
`uniqueBaseOn_empty` 📖	mathematical	—	`uniqueBaseOn` `Set` `Set.instEmptyCollection` `loopyOn`	—	`uniqueBaseOn_dual_eq` `Set.diff_empty` `uniqueBaseOn_self` `loopyOn_dual_eq`
`uniqueBaseOn_finitary` 📖	mathematical	—	`Finitary` `uniqueBaseOn`	—	`Set.singleton_subset_iff`
`uniqueBaseOn_ground` 📖	mathematical	—	`E` `uniqueBaseOn`	—	—
`uniqueBaseOn_indep_iff` 📖	mathematical	`Set` `Set.instHasSubset`	`Indep` `uniqueBaseOn`	—	`uniqueBaseOn.eq_1` `restrict_indep_iff` `freeOn_indep_iff` `HasSubset.Subset.trans` `Set.instIsTransSubset`
`uniqueBaseOn_indep_iff'` 📖	mathematical	—	`Indep` `uniqueBaseOn` `Set` `Set.instHasSubset` `Set.instInter`	—	`uniqueBaseOn.eq_1` `restrict_indep_iff` `freeOn_indep_iff` `Set.subset_inter_iff`
`uniqueBaseOn_inter_ground_eq` 📖	mathematical	—	`uniqueBaseOn` `Set` `Set.instInter`	—	—
`uniqueBaseOn_inter_isBasis` 📖	mathematical	`Set` `Set.instHasSubset`	`IsBasis` `uniqueBaseOn` `Set.instInter`	—	`uniqueBaseOn_isBasis_iff`
`uniqueBaseOn_isBase_iff` 📖	mathematical	`Set` `Set.instHasSubset`	`IsBase` `uniqueBaseOn`	—	`uniqueBaseOn.eq_1` `isBase_restrict_iff'` `freeOn_isBasis'_iff` `Set.inter_eq_self_of_subset_right`
`uniqueBaseOn_isBasis_iff` 📖	mathematical	`Set` `Set.instHasSubset`	`IsBasis` `uniqueBaseOn` `Set.instInter`	—	`isBasis_iff_maximal` `maximal_iff_eq` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.inter_subset_left`
`uniqueBaseOn_rankFinite` 📖	mathematical	—	`RankFinite` `uniqueBaseOn`	—	`uniqueBaseOn_inter_ground_eq` `uniqueBaseOn_isBase_iff` `Set.inter_subset_right` `Set.Finite.subset` `Set.inter_subset_left`
`uniqueBaseOn_rankPos` 📖	mathematical	`Set` `Set.instHasSubset` `Set.Nonempty`	`RankPos` `uniqueBaseOn`	—	`uniqueBaseOn_isBase_iff` `Set.Nonempty.ne_empty`
`uniqueBaseOn_restrict` 📖	mathematical	`Set` `Set.instHasSubset`	`restrict` `uniqueBaseOn` `Set.instInter`	—	`uniqueBaseOn_restrict'` `Set.inter_right_comm` `Set.inter_eq_self_of_subset_left`
`uniqueBaseOn_restrict'` 📖	mathematical	—	`restrict` `uniqueBaseOn` `Set` `Set.instInter`	—	—
`uniqueBaseOn_self` 📖	mathematical	—	`uniqueBaseOn` `freeOn`	—	`uniqueBaseOn.eq_1` `freeOn_restrict` `Eq.subset` `Set.instReflSubset`

Matroid.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`loopyOn_finite` 📖	mathematical	—	`Matroid.Finite` `Matroid.loopyOn`	—	—

Matroid.Indep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrict_eq_freeOn` 📖	mathematical	`Matroid.Indep`	`Matroid.restrict` `Matroid.freeOn`	—	`Matroid.restrict_eq_freeOn_iff`

---

← Back to Index