| Metric | Count |
|---|
DefinitionsMatroid, Dep, E, ExchangeProperty, ExistsMaximalSubsetProperty, Finitary, IsBase, IsBasis, IsBasis', RankFinite, RankInfinite, RankPos, aesop_mat, copy, copyBase, copyIndep | 16 |
Theoremsnonempty, not_indep, subset_ground, superset, antichain, encard_diff_eq, encard_diff_le_aux, encard_isBase_eq, indep_of_forall_finite, ground_finite, diff, eq_of_isBasis, exists_insert_of_not_isBase, exists_insert_of_not_maximal, exists_isBase_subset_union_isBase, exists_isBase_superset, finite, inter_left, inter_right, isBase_of_forall_insert, isBase_of_maximal, isBasis_iff_forall_insert_dep, isBasis_insert_iff, isBasis_of_forall_insert, isBasis_of_maximal_subset, isBasis_self, isBasis_setOf_insert_isBasis, not_dep, rankPos_of_nonempty, subset, subset_ground, subset_isBasis'_of_subset, subset_isBasis_of_subset, dep_of_insert, dep_of_ssubset, diff_finite_comm, diff_infinite_comm, encard_diff_comm, encard_eq_encard_of_isBase, eq_exchange_of_diff_eq_singleton, eq_of_subset_indep, eq_of_subset_isBase, exchange, exchange_isBase_of_indep, exchange_isBase_of_indep', exchange_mem, exists_insert_of_ssubset, finite, finite_of_finite, indep, infinite, infinite_of_infinite, insert_dep, insert_not_isBase, isBase_of_isBasis_superset, isBasis_ground, isBasis_of_subset, mem_of_insert_indep, ncard_diff_comm, ncard_eq_ncard_of_isBase, nonempty, not_isBase_of_ssubset, rankFinite_of_finite, rankInfinite_of_infinite, rankPos_of_nonempty, subset_ground, eq_of_subset_indep, indep, insert_not_indep, inter_eq_of_subset_indep, isBasis, isBasis_inter_ground, mem_of_insert_indep, subset, dep_of_ssubset, eq_of_subset_indep, exists_isBase, exists_isBasis_inter_eq_of_superset, iUnion_isBasis_iUnion, indep, insert_dep, insert_isBasis_insert, inter_eq_of_subset_indep, isBasis', isBasis_iUnion, isBasis_inter_ground, isBasis_sUnion, isBasis_subset, isBasis_union, isBasis_union_of_subset, left_subset_ground, mem_of_insert_indep, not_isBasis_of_ssubset, subset, subset_ground, union_isBasis_union, ground_nonempty, exists_finite_isBase, exists_infinite_isBase, empty_not_isBase, copyBase_E, copyBase_Indep, copyBase_IsBase, copyIndep_E, copyIndep_Indep, copyIndep_IsBase, copy_E, copy_Indep, copy_IsBase, dep_iff, dep_of_not_indep, empty_indep, empty_not_isBase, existsMaximalSubsetProperty_indep, exists_isBase, exists_isBasis, exists_isBasis', exists_isBasis_disjoint_isBasis_of_subset, exists_isBasis_subset_isBasis, exists_isBasis_union_inter_isBasis, ext, ext_iff, ext_iff_indep, ext_iff_isBase, ext_indep, ext_indep_iff, ext_isBase, ext_isBase_indep, finitary_iff, finitary_of_rankFinite, finite_iff, finite_of_finite, finite_setOf_matroid, finite_setOf_matroid', ground_finite, ground_indep_iff_isBase, ground_nonempty, ground_nonempty_iff, indep_iff, indep_iff', indep_iff_forall_finite_subset_indep, indep_iff_not_dep, indep_of_forall_finite_subset_indep, indep_of_not_dep, indep_or_dep, insert_isBase_of_insert_indep, instNonemptySubtypeSetIsBase, isBase_compl_iff_maximal_disjoint_isBase, isBase_exchange, isBase_iff_maximal_indep, isBasis'_iff_isBasis, isBasis'_iff_isBasis_inter_ground, isBasis_empty_iff, isBasis_ground_iff, isBasis_iff, isBasis_iff', isBasis_iff_isBasis'_subset_ground, isBasis_iff_maximal, isBasis_self_iff_indep, maximality, nonempty_type, not_dep_iff, not_indep_iff, not_rankFinite, not_rankFinite_iff, not_rankInfinite, not_rankInfinite_iff, rankFinite_iff, rankFinite_of_finite, rankFinite_or_rankInfinite, rankInfinite_iff, rankPos_iff, rankPos_nonempty, setOf_dep_eq, setOf_indep_eq, set_finite, subset_ground | 177 |
| Total | 193 |
| Name | Category | Theorems |
|---|
Dep 📖 | MathDef | 44 mathmath: Indep.mem_closure_iff, IsBase.dep_of_insert, eRk_lt_encard_iff_dep, IsCircuit.minimal, IsBasis.contract_dep_iff, Indep.isBasis_insert_iff, isLoop_tfae, map_dep_iff, eRk_lt_encard_iff_dep_of_finite, IsCircuit.contract_dep, dual_dep_iff_forall, restrict_dep_iff, IsBase.dep_of_ssubset, Indep.contract_dep_iff, dep_iff_superset_isCircuit', indep_iff_not_dep, mapEquiv_dep_iff, Indep.insert_dep_iff, comap_dep_iff, IsBase.insert_dep, isCircuit_iff_dep_forall_diff_singleton_indep, IsLoop.dep, isCircuit_def, IsRestriction.dep_iff, IsCircuit.contract_dep_of_not_subset, Indep.mem_closure_iff_of_notMem, delete_dep_iff, indep_or_dep, isCircuit_iff_forall_ssubset, Indep.isBasis_iff_forall_insert_dep, singleton_dep, not_dep_iff, dep_of_not_indep, IsBasis.dep_of_ssubset, not_indep_iff, IsBasis.insert_dep, IsLoop.dep_of_mem, IsCircuit.dep, Indep.not_dep, dep_iff_superset_isCircuit, IsBasis'.contract_dep_iff, isCircuit_iff, dep_iff, setOf_dep_eq
|
E 📖 | CompOp | 226 mathmath: exists_isBasis_inter_ground_isBasis_closure, instNonemptyElemSetSetOfAndIsFlatSubsetInterE, isColoop_iff_forall_mem_compl_isCircuit, IsNonloop.mem_ground, isCocircuit_iff_minimal_compl_nonspanning, isRkFinite_ground, ext_indep_iff, Indep.mem_closure_iff', IsStrictMinor.ssubset, Coindep.compl_spanning, restrict_eq_self_iff, ofBase_E, IsRestriction.exists_eq_delete, subset_ground, dual_isBase_iff', Coindep.exists_subset_compl_isBase, eRank_le_encard_add_eRk_compl, inter_ground_subset_closure, delete_inter_ground_eq, ext_iff_isBase, cRk_inter_ground, Dep.subset_ground, finite_setOf_matroid', IsBase.compl_isBase_of_dual, IsBasis.subset_ground, Indep.exists_eq_image_of_mapSetEmbedding, restrict_loops_eq', insert_indep_iff, closure_univ, IsRestriction.exists_eq_restrict, isColoop_iff_diff_not_spanning, isColoop_iff_forall_mem_closure_iff_mem', closure_subset_ground, IsMinor.exists_eq_contract_delete_disjoint, isBasis_iff_isBasis'_subset_ground, coindep_iff_forall_subset_not_isCocircuit, delete_eq_self_iff, contract_eq_self_iff, cRk_ground, IsColoop.mem_ground, restrictSubtype_ground, isBasis_ground_iff, isClosed_iff_isFlat, eRk_dual_add_eRank', eRk_compl_union_of_disjoint, Spanning.contract_eq_loopyOn, IsBase.isBasis_ground, contract_isNonloop_iff, removeLoops_ground_eq, dual_dep_iff_forall, comapOn_ground_eq, ext_iff, eRk_compl_insert_union_add_eRk_compl_insert_inter_le, contract_ground, comap_map, fundCocircuit_subset_insert_compl, Coindep.exists_isBase_subset_compl, closure_eq_subtypeClosure, spanning_iff_eRk_le', emptyOn_ground, restrict_ground_eq, dualIndepMatroid_E, eRk_union_ground, dep_iff_superset_isCircuit', sigma_ground_eq, Spanning.closure_eq, mapEmbedding_ground_eq, restrict_spanning_iff', dual_indep_iff_exists', instFiniteElemERestrictSubtype, IsStrictRestriction.ssubset, indep_iff_not_dep, sum'_ground_eq, ground_not_isBase, mapSetEmbedding_indep_iff', Indep.insert_indep_iff, eRank_le_encard_ground, coloops_subset_ground, spanning_iff, isBasis'_iff_isBasis_inter_ground, isBasis_iff', ground_isFlat, IsBasis.isBasis_inter_ground, eRank_def, IsBase.compl_closure_diff_singleton_isCocircuit, ofIsBaseOfFinite_E, eRk_inter_ground, uniqueBaseOn_ground, mapSetEquiv.ground, IsBase.subset_ground, IsBase.closure_eq, setOf_isNonloop_eq, freeOn_ground, closure_ground, delete_eq_restrict, IsRestriction.base_iff, ground_nonempty, mapEquiv_ground_eq, IsBase.compl_isBase_dual, IsBasis'.isBasis_inter_ground, IndepMatroid.matroid_E, eRk_ground_inter, Spanning.compl_coindep, isRkFinite_ground_iff_rankFinite, IsBase.compl_inter_isBasis_of_inter_isBasis, eRk_ground, map_id, delete_ground, closure_def, sum_ground, map_val_restrictSubtype_eq, ofExistsFiniteIsBase_E, mapSetEmbedding_indep_iff, restrict_ground_eq_self, finite_setOf_matroid, eRank_eq_zero_iff, Indep.subset_ground, indep_iff_forall_notMem_closure_diff', eRk_ground_union, eq_restrict_removeLoops, isBasis_restrict_iff', isRestriction_iff_exists, ground_indep_iff_eq_freeOn, ground_subset_closure_iff, eRk_eq_zero_iff', instRankPosElemERestrictSubtype, closure_inter_ground, finite_iff, spanning_iff_exists_isBase_subset', isLoop_iff_forall_mem_compl_isBase, comap_ground_eq, eRank_add_eRank_dual, isNonloop_iff_mem_compl_loops, IsCircuit.subset_ground, Spanning.closure_eq_of_superset, IsBasis.left_subset_ground, IsRestriction.dep_iff, delete_isColoop_iff, Spanning.subset_ground, isColoop_tfae, isRestriction_iff_exists_eq_delete, IsRestriction.subset, contract_spanning_iff', Nonempty.ground_nonempty, IsRkFinite.inter_ground, restrictSubtype_ground_isBasis_iff, restrictSubtype_ground_isBase_iff, contract_inter_ground_eq, isBase_iff_indep_closure_eq, contract_eq_contract_iff, Indep.isBase_iff_ground_subset_closure, IsStrictRestriction.eq_restrict, ground_indep_iff_isBase, AlgebraicIndependent.matroid_e, Coindep.subset_ground, restrict_closure_eq', ground_finite, closure_empty_eq_ground_iff, not_rankPos_iff, Coindep.closure_compl, restrictSubtype_dual, dual_ground, eq_loopyOn_or_rankPos, IsCocircuit.subset_ground, IsBase.closure_of_superset, eq_freeOn_iff, isBasis_iff_isBasis_closure_of_subset', coindep_iff_subset_compl_isBase, isFlat_iff_isClosed, Indep.insert_diff_indep_iff, ground_spanning, isCocircuit_iff_minimal_compl_nonspanning', restrict_compl, isNonloop_iff, eRk_compl_union_add_eRk_compl_inter_le, coindep_iff_exists', map_val_restrictSubtype_ground_eq, ground_nonempty_iff, delete_subset_ground, eq_loopyOn_iff, comap_isBase_iff, Finite.ground_finite, isRkFinite_inter_ground_iff, IsMinor.subset, delete_eq_delete_iff, IsRestriction.isLoop_iff, contract_ground_subset_ground, eq_loopyOn_iff_eRank, dualIndepMatroid_Indep, loops_subset_ground, ext_iff_indep, mapSetEmbedding_ground, IsBase.isBasis_of_isRestriction, eq_loopyOn_iff_loops_eq, Loopless.ground_eq, empty_isBase_iff, IsRestriction.indep_iff, mapEquiv_eq_map, mapSetEquiv_indep_iff, IsBase.ssubset_ground, IsRestriction.eq_restrict, isLoop_iff_closure_eq_loops_and_mem_ground, eq_loopyOn_iff_loops, IsLoop.mem_ground, IsBase.encard_compl_eq, ground_eq_empty_iff, ext_iff_isCircuit, restrict_isLoop_iff, isStrictMinor_iff_isMinor_ssubset, delete_isBase_iff, instNonemptyElemERestrictSubtype, loopyOn_ground, IsRestriction.isBasis_iff, IsFlat.subset_ground, dep_iff, compl_loops_eq, indep_iff_forall_subset_not_isCircuit', IsColoop.diff_not_spanning, setOf_dual_isBase_eq, IsStrictRestriction.exists_eq_restrict, mem_ground_of_mem_closure, Indep.ssubset_ground, comapOn_preimage_eq, isFlat_iff, setOf_dep_eq, Indep.insert_indep_iff_of_notMem
|
ExchangeProperty 📖 | MathDef | 1 mathmath: isBase_exchange
|
ExistsMaximalSubsetProperty 📖 | MathDef | 4 mathmath: existsMaximalSubsetProperty_of_bdd, maximality, IndepMatroid.indep_maximal, existsMaximalSubsetProperty_indep
|
Finitary 📖 | CompData | 18 mathmath: AlgebraicIndependent.instFinitaryMatroid, comap_finitary, IsRestriction.finitary, finitary_iff, instFinitaryMapEmbedding, finitary_of_rankFinite, finitary_iff_forall_isCircuit_finite, instFinitaryElemRestrictSubtype, freeOn_finitary, IndepMatroid.ofFinitary_finitary, delete_finitary, uniqueBaseOn_finitary, contract_finitary, instFinitaryMapEquiv, restrict_finitary, instFinitaryMap, IndepMatroid.ofFinitaryCardAugment_finitary, comapOn_finitary
|
IsBase 📖 | MathDef | 91 mathmath: base_iff_dual_isBase_compl, Indep.isBase_of_forall_insert, rankPos_iff, ofIsBaseOfFinite_isBase, IsBasis.isBase_restrict, comapOn_isBase_iff_of_surjOn, isBase_restrict_iff', isBase_compl_iff_maximal_disjoint_isBase, IndepMatroid.matroid_IsBase, dual_isBase_iff', Coindep.exists_subset_compl_isBase, RankInfinite.exists_infinite_isBase, ext_iff_isBase, Spanning.isBase_of_indep, spanning_iff_exists_isBase_subset, coindep_iff_exists, Indep.isBase_of_maximal, isBasis_ground_iff, instNonemptySubtypeSetIsBase, IsBasis'.isBase_restrict, mapEmbedding_isBase_iff, ext_iff, Indep.isBase_of_spanning, Indep.isBase_of_eRk_ge, IsBasis.isBase_of_spanning, Coindep.exists_isBase_subset_compl, map_image_isBase_iff, indep_iff, dual_indep_iff_exists', comapOn_isBase_iff, ground_not_isBase, sum_isBase_iff, dual_isBase_iff, comapOn_isBase_iff_of_bijOn, Spanning.exists_isBase_subset, IsRestriction.base_iff, loopyOn_isBase_iff, RankPos.empty_not_isBase, AlgebraicIndependent.matroid_isBase_iff, Spanning.isBase_of_minimal, Indep.isBase_of_cRank_le, disjointSum_isBase_iff, Indep.isBase_of_cRank_le_of_finite, setOf_indep_eq, Indep.exists_isBase_superset, rankFinite_iff, sigma_isBase_iff, Restriction.isBase_iff_of_spanning, IsNonloop.exists_mem_isBase, copyIndep_IsBase, spanning_iff_exists_isBase_subset', dual_indep_iff_exists, exists_isBase, emptyOn_isBase_iff, restrictSubtype_ground_isBase_iff, isBase_iff_indep_closure_eq, Spanning.isBase_restrict_iff, Indep.isBase_iff_ground_subset_closure, ground_indep_iff_isBase, RankFinite.exists_finite_isBase, ofExistsFiniteIsBase_isBase, freeOn_isBase_iff, empty_not_isBase, isBase_iff_minimal_spanning, coindep_iff_subset_compl_isBase, isBase_restrict_iff, rankInfinite_iff, Spanning.isBase_of_le_cRank, sum'_isBase_iff, coindep_iff_exists', isBase_iff_maximal_indep, IsBasis.restrict_isBase, comap_isBase_iff, Indep.contract_isBase_iff, restrictSubtype_isBase_iff, Coindep.delete_isBase_iff, dualIndepMatroid_Indep, disjointSigma_isBase_iff, IsBasis.exists_isBase, map_isBase_iff, isBase_exchange, empty_isBase_iff, delete_isBase_iff, Spanning.isBase_of_le_cRank_of_finite, indep_iff', mapEquiv_isBase_iff, uniqueBaseOn_isBase_iff, Indep.isBase_of_ground_subset_closure, Indep.exists_isBase_subset_spanning, setOf_dual_isBase_eq, removeLoops_isBase_eq
|
IsBasis 📖 | MathDef | 78 mathmath: exists_isBasis_inter_ground_isBasis_closure, exists_isBasis_disjoint_isBasis_of_subset, Indep.isBasis_of_forall_insert, isBasis_iff, freeOn_isBasis_iff, isBasis_iff_isBasis_closure_of_subset, isBasis_iff_indep_encard_eq_of_finite, sigma_isBasis_iff, exists_isBasis_union_inter_isBasis, restrictSubtype_isBasis_iff, Indep.isBasis_insert_iff, AlgebraicIndependent.matroid_isBasis_iff, Indep.isBasis_of_maximal_subset, isBasis_restrict_iff, Indep.isBasis_of_eRk_ge, isBasis_iff_isBasis'_subset_ground, Indep.subset_finite_isBasis_of_subset_of_isRkFinite, Indep.isBasis_closure, isBasis_ground_iff, IsBase.isBasis_ground, isBasis_iff_indep_subset_closure, isBasis_self_iff_indep, IsCircuit.diff_singleton_isBasis, loopyOn_isBasis_iff, IsBasis'.isBasis, isBasis'_iff_isBasis_inter_ground, isBasis_iff', isRkFinite_iff, Indep.closure_eq_setOf_isBasis_insert, Indep.insert_isBasis_iff_mem_closure, IsRestriction.base_iff, comap_isBasis_iff, IsBasis'.isBasis_inter_ground, isBasis_iff_empty_of_subset_loops, sum_isBasis_iff, uniqueBaseOn_inter_isBasis, disjointSum_isBasis_iff, sum'_isBasis_iff, disjointSigma_isBasis_iff, isBasis_restrict_iff', map_isBasis_iff, IsRkFinite.isBasis_of_subset_closure_of_subset_of_encard_le, isBasis_loops_iff, IsCircuit.isBasis_iff_eq_diff_singleton, isBasis'_iff_isBasis, isBasis_iff_maximal, uniqueBaseOn_isBasis_iff, restrictSubtype_ground_isBasis_iff, Indep.isBasis_setOf_insert_isBasis, Indep.isBasis_iff_forall_insert_dep, Indep.inter_isBasis_closure_iff_subset_closure_inter, delete_isBasis_iff, isBasis_iff_isBasis_closure_of_subset', exists_isBasis_subset_isBasis, empty_isBasis_iff, isBase_restrict_iff, isBasis_union_iff_indep_closure, exists_isBasis, eq_eRk_iff, IsBase.inter_isBasis_iff_compl_inter_isBasis_dual, mapEmbedding_isBasis_iff, IsBase.isBasis_of_subset, isBasis'_iff_isBasis_restrict_univ, mapEquiv_isBasis_iff, comap_isBase_iff, isBasis'_iff_isBasis_closure, IsBase.isBasis_of_isRestriction, map_isBasis_iff', Indep.subset_isBasis_of_subset, isBasis_iff_indep_closure, Indep.isBasis_of_subset_of_subset_closure, AlgebraicIndependent.matroid_isBasis_iff_of_subsingleton, delete_isBase_iff, IsRestriction.isBasis_iff, IsCircuit.isBasis_iff_insert_eq, IsBasis'.isBasis_closure_right, isBasis_empty_iff, Indep.isBasis_self
|
IsBasis' 📖 | MathDef | 23 mathmath: removeLoops_isBasis'_eq, comap_isBasis'_iff, isBase_restrict_iff', restrictSubtype_isBasis_iff, isBasis_iff_isBasis'_subset_ground, Indep.subset_finite_isBasis'_of_subset_of_isRkFinite, IsBasis.isBasis', isBasis'_restrict_iff, delete_isBasis'_iff, isRkFinite_iff_exists_isBasis', Indep.isBasis'_of_eRk_ge, freeOn_isBasis'_iff, comapOn_isBase_iff, isBasis'_iff_isBasis_inter_ground, IsRkFinite.exists_finite_isBasis', Indep.subset_isBasis'_of_subset, isBasis'_iff_isBasis, isBasis'_iff_indep_encard_eq_of_finite, isBasis'_iff_isBasis_restrict_univ, restrictSubtype_isBase_iff, isBasis'_iff_isBasis_closure, exists_isBasis', IsRkFinite.exists_finset_isBasis'
|
RankFinite 📖 | CompData | 27 mathmath: IndepMatroid.ofBddAugment_rankFinite, instRankFiniteElemRestrictSubtype, ofExistsFiniteIsBase_rankFinite, restrict_rankFinite, IsBase.rankFinite_of_finite, comap_rankFinite, eRank_lt_top_iff, rankFinite_of_finite, IsRkFinite.rankFinite, comapOn_rankFinite, instRankFiniteMapEquiv, isRkFinite_ground_iff_rankFinite, not_rankFinite, rankFinite_iff, loopyOn_rankFinite, rankFinite_iff_cRank_lt_aleph0, not_rankFinite_iff, delete_rankFinite, not_rankInfinite_iff, rankFinite_or_rankInfinite, uniqueBaseOn_rankFinite, IsRestriction.rankFinite, instRankFiniteMap, eRank_ne_top_iff, instRankFiniteMapEmbedding, IndepMatroid.instRankFiniteMatroidOfBdd, contract_rankFinite
|
RankInfinite 📖 | CompData | 8 mathmath: eRank_eq_top_iff, IsBase.rankInfinite_of_infinite, rankInfinite_iff_aleph0_le_cRank, not_rankFinite_iff, not_rankInfinite, rankInfinite_iff, not_rankInfinite_iff, rankFinite_or_rankInfinite
|
RankPos 📖 | CompData | 17 mathmath: rankPos_iff, IsBase.rankPos_of_nonempty, instRankPosMapEquiv, dual_rankPos_iff_exists_isCircuit, IsCircuit.dual_rankPos, instRankPosOfNonemptyOfLoopless, instRankPosMap, uniqueBaseOn_rankPos, IsNonloop.rankPos, instRankPosElemERestrictSubtype, freeOn_rankPos, rankPos_iff_exists_isCocircuit, not_rankPos_iff, eq_loopyOn_or_rankPos, instRankPosMapEmbedding, Coindep.delete_rankPos, Indep.rankPos_of_nonempty
|
aesop_mat 📖 | CompOp | — |
copy 📖 | CompOp | 3 mathmath: copy_IsBase, copy_E, copy_Indep
|
copyBase 📖 | CompOp | 3 mathmath: copyBase_E, copyBase_Indep, copyBase_IsBase
|
copyIndep 📖 | CompOp | 3 mathmath: copyIndep_IsBase, copyIndep_E, copyIndep_Indep
|