Dual

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

Statistics

Metric	Count
Definitions `Coindep`, `dual`, `dualIndepMatroid`, `«term_✶»`	4
Theorems `exists_isBase_subset_compl`, `exists_subset_compl_isBase`, `indep`, `subset_ground`, `coindep`, `ssubset_ground`, `compl_inter_isBasis_of_inter_isBasis`, `compl_isBase_dual`, `compl_isBase_of_dual`, `inter_isBasis_iff_compl_inter_isBasis_dual`, `ssubset_ground`, `base_iff_dual_isBase_compl`, `coindep_def`, `coindep_iff_exists`, `coindep_iff_exists'`, `coindep_iff_subset_compl_isBase`, `dualIndepMatroid_E`, `dualIndepMatroid_Indep`, `dual_coindep_iff`, `dual_dep_iff_forall`, `dual_dual`, `dual_finite`, `dual_ground`, `dual_indep_iff_exists`, `dual_indep_iff_exists'`, `dual_inj`, `dual_injective`, `dual_involutive`, `dual_isBase_iff`, `dual_isBase_iff'`, `dual_nonempty`, `eq_dual_comm`, `eq_dual_iff_dual_eq`, `ground_not_isBase`, `setOf_dual_isBase_eq`	35
Total	39

Matroid

Definitions

Name	Category	Theorems
`Coindep` 📖	MathDef	12 math math: `spanning_iff_compl_coindep`, `coindep_iff_closure_compl_eq_ground`, `coindep_iff_exists`, `coindep_iff_forall_subset_not_isCocircuit`, `dual_coindep_iff`, `Spanning.compl_coindep`, `coindep_contract_iff`, `coindep_iff_subset_compl_isBase`, `coindep_iff_exists'`, `coindep_iff_compl_spanning`, `Indep.coindep`, `coindep_def`
`dual` 📖	CompOp	53 math math: `base_iff_dual_isBase_compl`, `dual_isBase_iff'`, `IsCircuit.isCocircuit`, `IsLoop.dual_isColoop`, `uniqueBaseOn_dual_eq`, `restrictSubtype_dual'`, `dual_coindep_iff`, `eRk_dual_add_eRank'`, `dual_contract_delete`, `dual_dep_iff_forall`, `dual_contract`, `dual_injective`, `dual_loops`, `dual_rankPos_iff_exists_isCircuit`, `IsCircuit.dual_rankPos`, `eRk_dual_add_eRank`, `dual_isLoop_iff_isColoop`, `dual_indep_iff_exists'`, `freeOn_dual_eq`, `dual_finite`, `dual_isBase_iff`, `isCocircuit_def`, `IsColoop.dual_isLoop`, `dual_delete_contract`, `map_dual`, `IsBase.compl_isBase_dual`, `IsBase.compl_inter_isBasis_of_inter_isBasis`, `dual_dual`, `dual_delete_dual`, `Coindep.indep`, `dual_involutive`, `eq_dual_iff_dual_eq`, `dual_isColoop_iff_isLoop`, `dual_isCocircuit_iff`, `dual_indep_iff_exists`, `eRank_add_eRank_dual`, `dual_coloops`, `dual_contract_dual`, `loopyOn_dual_eq`, `restrictSubtype_dual`, `dual_ground`, `comapOn_dual_eq_of_bijOn`, `IsCocircuit.isCircuit`, `IsBase.inter_isBasis_iff_compl_inter_isBasis_dual`, `eq_dual_comm`, `dual_nonempty`, `dual_inj`, `IsBase.encard_compl_eq`, `Indep.coindep`, `emptyOn_dual_eq`, `coindep_def`, `setOf_dual_isBase_eq`, `dual_delete`
`dualIndepMatroid` 📖	CompOp	2 math math: `dualIndepMatroid_E`, `dualIndepMatroid_Indep`
`«term_✶»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`base_iff_dual_isBase_compl` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`IsBase` `dual` `Set.instSDiff`	—	`dual_isBase_iff` `Set.diff_diff_cancel_left`
`coindep_def` 📖	mathematical	—	`Coindep` `Indep` `dual`	—	—
`coindep_iff_exists` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`Coindep` `IsBase` `Set.instSDiff`	—	`coindep_iff_exists'`
`coindep_iff_exists'` 📖	mathematical	—	`Coindep` `IsBase` `Set` `Set.instHasSubset` `Set.instSDiff` `E`	—	`IsBase.subset_ground` `Disjoint.symm`
`coindep_iff_subset_compl_isBase` 📖	mathematical	—	`Coindep` `IsBase` `Set` `Set.instHasSubset` `Set.instSDiff` `E`	—	`Disjoint.symm` `IsBase.subset_ground`
`dualIndepMatroid_E` 📖	mathematical	—	`IndepMatroid.E` `dualIndepMatroid` `E`	—	—
`dualIndepMatroid_Indep` 📖	mathematical	—	`IndepMatroid.Indep` `dualIndepMatroid` `Set` `Set.instHasSubset` `E` `IsBase` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	—
`dual_coindep_iff` 📖	mathematical	—	`Coindep` `dual` `Indep`	—	`Coindep.eq_1` `dual_dual`
`dual_dep_iff_forall` 📖	mathematical	—	`Dep` `dual` `Set.Nonempty` `Set` `Set.instInter` `Set.instHasSubset` `E`	—	—
`dual_dual` 📖	mathematical	—	`dual`	—	`ext_isBase` `dual_isBase_iff` `dual_ground` `Set.diff_diff_cancel_left`
`dual_finite` 📖	mathematical	—	`Finite` `dual`	—	`ground_finite`
`dual_ground` 📖	mathematical	—	`E` `dual`	—	—
`dual_indep_iff_exists` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`Indep` `dual` `IsBase` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`dual_indep_iff_exists'`
`dual_indep_iff_exists'` 📖	mathematical	—	`Indep` `dual` `Set` `Set.instHasSubset` `E` `IsBase` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	—
`dual_inj` 📖	mathematical	—	`dual`	—	`dual_injective`
`dual_injective` 📖	mathematical	—	`Matroid` `dual`	—	`Function.Involutive.injective` `dual_involutive`
`dual_involutive` 📖	mathematical	—	`Function.Involutive` `Matroid` `dual`	—	`dual_dual`
`dual_isBase_iff` 📖	mathematical	`Set` `Set.instHasSubset` `E`	`IsBase` `dual` `Set.instSDiff`	—	`isBase_compl_iff_maximal_disjoint_isBase` `isBase_iff_maximal_indep` `maximal_subset_iff`
`dual_isBase_iff'` 📖	mathematical	—	`IsBase` `dual` `Set` `Set.instSDiff` `E` `Set.instHasSubset`	—	`em` `dual_isBase_iff` `IsBase.subset_ground`
`dual_nonempty` 📖	mathematical	—	`Nonempty` `dual`	—	`ground_nonempty`
`eq_dual_comm` 📖	mathematical	—	`dual`	—	`dual_dual`
`eq_dual_iff_dual_eq` 📖	mathematical	—	`dual`	—	`Function.Involutive.eq_iff` `dual_involutive`
`ground_not_isBase` 📖	mathematical	—	`IsBase` `E`	—	`Set.diff_empty` `dual_isBase_iff` `rankPos_iff`
`setOf_dual_isBase_eq` 📖	mathematical	—	`setOf` `Set` `IsBase` `dual` `Set.image` `Set.instSDiff` `E`	—	`Set.ext` `Set.diff_diff_cancel_left` `IsBase.subset_ground` `Eq.trans_subset` `Set.diff_subset`

Matroid.Coindep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isBase_subset_compl` 📖	mathematical	`Matroid.Coindep`	`Matroid.IsBase` `Set` `Set.instHasSubset` `Set.instSDiff` `Matroid.E`	—	`Matroid.coindep_iff_exists` `subset_ground`
`exists_subset_compl_isBase` 📖	mathematical	`Matroid.Coindep`	`Matroid.IsBase` `Set` `Set.instHasSubset` `Set.instSDiff` `Matroid.E`	—	`Matroid.coindep_iff_subset_compl_isBase`
`indep` 📖	mathematical	`Matroid.Coindep`	`Matroid.Indep` `Matroid.dual`	—	—
`subset_ground` 📖	mathematical	`Matroid.Coindep`	`Set` `Set.instHasSubset` `Matroid.E`	—	`Matroid.Indep.subset_ground` `indep`

Matroid.Indep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coindep` 📖	mathematical	`Matroid.Indep`	`Matroid.Coindep` `Matroid.dual`	—	`Matroid.dual_coindep_iff`
`ssubset_ground` 📖	mathematical	`Matroid.Indep`	`Set` `Set.instHasSSubset` `Matroid.E`	—	`exists_isBase_superset` `HasSubset.Subset.trans_ssubset` `Set.instIsNonstrictStrictOrderSubsetSSubset` `Set.instIsTransSubset` `Matroid.IsBase.ssubset_ground`

Matroid.IsBase

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compl_inter_isBasis_of_inter_isBasis` 📖	mathematical	`Matroid.IsBase` `Matroid.IsBasis` `Set` `Set.instInter`	`Matroid.dual` `Set.instSDiff` `Matroid.E`	—	`Matroid.Indep.isBasis_of_forall_insert` `Matroid.dual_indep_iff_exists` `Set.disjoint_of_subset_left` `Set.inter_subset_left` `Set.disjoint_sdiff_left` `Set.inter_subset_right` `Set.diff_inter_self_eq_diff` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.diff_subset` `by_contra` `exchange` `Set.diff_eq_empty` `Set.diff_eq` `Set.inter_eq_self_of_subset_right` `subset_ground` `Set.inter_right_comm` `Set.singleton_inter_eq_empty` `Set.union_empty_iff` `Set.union_inter_distrib_right` `Set.diff_inter_diff` `Set.union_singleton` `not_ne_iff` `Set.nonempty_iff_ne_empty` `Matroid.Indep.subset` `indep` `Set.insert_subset_insert` `Matroid.IsBasis.mem_of_insert_indep`
`compl_isBase_dual` 📖	mathematical	`Matroid.IsBase`	`Matroid.dual` `Set` `Set.instSDiff` `Matroid.E`	—	`Matroid.dual_isBase_iff` `Set.diff_diff_cancel_left` `subset_ground`
`compl_isBase_of_dual` 📖	mathematical	`Matroid.IsBase` `Matroid.dual`	`Set` `Set.instSDiff` `Matroid.E`	—	`Matroid.dual_isBase_iff'`
`inter_isBasis_iff_compl_inter_isBasis_dual` 📖	mathematical	`Matroid.IsBase` `Set` `Set.instHasSubset` `Matroid.E`	`Matroid.IsBasis` `Set.instInter` `Matroid.dual` `Set.instSDiff`	—	`compl_inter_isBasis_of_inter_isBasis` `Matroid.dual_dual` `sdiff_sdiff_right_self` `Set.inter_eq_self_of_subset_right` `subset_ground` `compl_isBase_dual`
`ssubset_ground` 📖	mathematical	`Matroid.IsBase`	`Set` `Set.instHasSSubset` `Matroid.E`	—	`HasSubset.Subset.ssubset_of_ne` `Set.instIsNonstrictStrictOrderSubsetSSubset` `Set.instAntisymmSubset` `subset_ground` `Matroid.ground_not_isBase`

---

← Back to Index