| Metric | Count |
|---|
Definitionsencard, ncard, tacticToFinite_tac, tacticTo_encard_tac | 4 |
Theoremscard_coe_set_eq, exists_not_mem_of_card_lt_enatCard, encard_le, encard_image, encard_range, card_le_card_add_one_iff, card_coe_set_eq, cast_ncard_eq, encard_eq_coe, encard_eq_coe_toFinset_card, encard_lt_encard, encard_lt_top, encard_strictMonoOn, eq_insert_of_subset_of_encard_eq_succ, eq_of_subset_of_encard_le, eq_of_subset_of_encard_le', exists_bijOn_of_encard_eq, exists_encard_eq_coe, exists_injOn_of_encard_le, finite_of_encard_le, injOn_of_encard_image_eq, ncard_strictMonoOn, encard_eq, exists_subset_ncard_eq, exists_superset_ncard_eq, ncard, encard_image, ncard_image, encard_range, encard_pos, ncard_pos, cast_ncard, cast_ncard_sdiff, coe_fintypeCard, diff_nonempty_of_ncard_lt_ncard, encard_add_encard_compl, encard_coe_eq_coe_finsetCard, encard_congr, encard_diff, encard_diff_add_encard, encard_diff_add_encard_inter, encard_diff_add_encard_of_subset, encard_diff_singleton_add_one, encard_diff_singleton_of_mem, encard_empty, encard_eq_add_one_iff, encard_eq_coe_toFinset_card, encard_eq_encard_iff_encard_diff_eq_encard_diff, encard_eq_four, encard_eq_one, encard_eq_three, encard_eq_top, encard_eq_top_iff, encard_eq_two, encard_eq_zero, encard_exchange, encard_exchange', encard_image_le, encard_insert_le, encard_insert_of_notMem, encard_le_card, encard_le_coe_iff, encard_le_coe_iff_finite_ncard_le, encard_le_encard, encard_le_encard_diff_add_encard, encard_le_encard_iff_encard_diff_le_encard_diff, encard_le_encard_of_injOn, encard_le_one_iff, encard_le_one_iff_eq, encard_le_one_iff_subsingleton, encard_lt_encard_iff_encard_diff_lt_encard_diff, encard_lt_top_iff, encard_mono, encard_ne_add_one, encard_ne_top_iff, encard_ne_zero, encard_ne_zero_of_mem, encard_pair, encard_pi_eq_prod_encard, encard_pos, encard_preimage_of_bijective, encard_preimage_of_injective_subset_range, encard_preimage_val_le_encard_left, encard_preimage_val_le_encard_right, encard_prod, encard_singleton, encard_singleton_inter, encard_strictMono, encard_tsub_one_le_encard_diff_singleton, encard_union_add_encard_inter, encard_union_eq, encard_union_le, encard_univ, encard_univ_coe, eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt, eq_insert_of_ncard_eq_succ, eq_of_subset_of_ncard_le, eq_univ_iff_ncard, even_card_insert_iff, even_ncard_compl_iff, exists_eq_insert_iff_ncard, exists_mem_notMem_of_ncard_lt_ncard, exists_ne_map_eq_of_encard_lt_of_maps_to, exists_ne_map_eq_of_ncard_lt_of_maps_to, exists_ne_of_one_lt_encard, exists_ne_of_one_lt_ncard, exists_subset_card_eq, exists_subset_encard_eq, exists_subset_or_subset_of_two_mul_lt_ncard, exists_subsuperset_card_eq, exists_superset_subset_encard_eq, fiber_ncard_ne_zero_iff_mem_image, finite_iff_finite_of_encard_eq_encard, finite_of_encard_eq_coe, finite_of_encard_le_coe, finite_of_ncard_ne_zero, finite_of_ncard_pos, infinite_iff_infinite_of_encard_eq_encard, injOn_of_ncard_image_eq, inj_on_of_surj_on_of_ncard_le, le_ncard_diff, le_ncard_of_inj_on_range, map_eq_of_subset, ncard_add_ncard_compl, ncard_coe, ncard_coe_finset, ncard_compl, ncard_congr, ncard_congr', ncard_def, ncard_diff, ncard_diff_add_ncard, ncard_diff_add_ncard_of_subset, ncard_diff_singleton_add_one, ncard_diff_singleton_le, ncard_diff_singleton_lt_of_mem, ncard_diff_singleton_of_mem, ncard_empty, ncard_eq_four, ncard_eq_ncard_iff_ncard_diff_eq_ncard_diff, ncard_eq_of_bijective, ncard_eq_one, ncard_eq_succ, ncard_eq_three, ncard_eq_toFinset_card, ncard_eq_toFinset_card', ncard_eq_two, ncard_eq_zero, ncard_exchange, ncard_exchange', ncard_graphOn, ncard_image_iff, ncard_image_le, ncard_image_of_injOn, ncard_image_of_injective, ncard_insert_eq_ite, ncard_insert_le, ncard_insert_of_mem, ncard_insert_of_notMem, ncard_inter_add_ncard_diff_eq_ncard, ncard_inter_add_ncard_union, ncard_inter_le_ncard_left, ncard_inter_le_ncard_right, ncard_le_card, ncard_le_encard, ncard_le_ncard, ncard_le_ncard_diff_add_ncard, ncard_le_ncard_iff_ncard_diff_le_ncard_diff, ncard_le_ncard_image_add_one_iff, ncard_le_ncard_insert, ncard_le_ncard_of_injOn, ncard_le_one, ncard_le_one_iff, ncard_le_one_iff_eq, ncard_le_one_iff_subset_singleton, ncard_le_one_iff_subsingleton, ncard_le_one_of_subsingleton, ncard_lt_card, ncard_lt_ncard, ncard_lt_ncard_iff_ncard_diff_lt_ncard_diff, ncard_map, ncard_mono, ncard_ne_zero_of_mem, ncard_pair, ncard_pos, ncard_powerset, ncard_preimage_of_injective_subset_range, ncard_prod, ncard_range_of_injective, ncard_singleton, ncard_singleton_inter, ncard_strictMono, ncard_subtype, ncard_union_add_ncard_inter, ncard_union_eq, ncard_union_eq_iff, ncard_union_le, ncard_union_lt, ncard_univ, nonempty_inter_compl_of_ncard_add_ncard_lt, nonempty_inter_of_le_ncard_add_ncard, nonempty_inter_of_lt_ncard_add_ncard, nonempty_of_encard_ne_zero, nonempty_of_ncard_ne_zero, odd_card_insert_iff, odd_ncard_compl_iff, one_le_encard_iff_nonempty, one_le_encard_insert, one_le_ncard_insert, one_lt_encard_iff, one_lt_encard_iff_nontrivial, one_lt_ncard, one_lt_ncard_iff, one_lt_ncard_iff_nontrivial, one_lt_ncard_iff_nontrivial_and_finite, one_lt_ncard_of_nonempty_of_even, pred_ncard_le_ncard_diff_singleton, sep_of_ncard_eq, subset_iff_eq_of_ncard_le, surj_on_of_inj_on_of_ncard_le, three_lt_ncard, three_lt_ncard_iff, toENat_cardinalMk, toENat_cardinalMk_subtype, tsub_encard_le_encard_diff, two_lt_ncard, two_lt_ncard_iff, union_ne_univ_of_ncard_add_ncard_lt | 228 |
| Total | 232 |
| Name | Category | Theorems |
|---|
encard 📖 | CompOp | 176 mathmath: Function.Embedding.encard_le, Matroid.IsBase.encard_eq_eRank, Matroid.IsBase.encard_diff_comm, encard_eq_zero, toENat_cardinalMk_subtype, Matroid.eRk_lt_encard_iff_dep, encard_diff_add_encard, ENNReal.tsum_set_const, encard_union_eq, encard_prod, tsub_encard_le_encard_diff, AddCircle.card_torsion_le_of_isSMulRegular, ncard_le_encard, encard_univ_coe, Metric.encard_minimalCover, Finset.set_encard_biUnion_le, ncard_def, encard_preimage_val_le_encard_left, encard_pair, Matroid.eRank_le_encard_add_eRk_compl, Matroid.Indep.eRk_eq_encard, Matroid.isBasis_iff_indep_encard_eq_of_finite, Matroid.eRank_freeOn, MeasureTheory.Measure.count_apply, chainHeight_le_encard, Submodule.spanRank_toENat_eq_iInf_encard, Matroid.le_eRk_iff, Matroid.IsBase.encard_eq_encard_of_isBase, Nat.count_le_setENCard, Subgroup.IsComplement.encard_left, encard_union_add_encard_inter, encard_preimage_val_le_encard_right, encard_exchange, Matroid.eRk_lt_encard_iff_dep_of_finite, Metric.exists_set_encard_eq_coveringNumber, encard_neg, Matroid.IsBasis.eRk_eq_encard, Matroid.eRk_dual_add_eRank', Subgroup.IsComplement.encard_right, Finite.encard_lt_top, encard_union_le, encard_strictMono, encard_iUnion_of_finite, coe_fintypeCard, Matroid.IsBasis'.encard_eq_eRk, ENNReal.tsum_set_one, encard_empty, eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt, encard_eq_top_iff, encard_congr, encard_eq_encard_iff_encard_diff_eq_encard_diff, encard_eq_three, AddSubgroup.IsComplement.encard_right, AddSubgroup.IsComplement.encard_left, Matroid.IsBasis.encard_eq_eRk, Matroid.eRk_dual_add_eRank, Metric.IsCover.externalCoveringNumber_le_encard, encard_diff_add_encard_of_subset, encard_eq_top, Nat.encard_range, encard_lt_top_iff, encard_le_card, Metric.coveringNumber_zero, Finite.encard_lt_encard, Matroid.IsBasis.encard_eq_encard, SimpleGraph.vertexCoverNum_le_encard_edgeSet, Matroid.Indep.encard_le_eRk_of_subset, Matroid.eRank_le_encard_ground, encard_preimage_of_injective_subset_range, Matroid.IsBasis'.eRk_eq_encard, exists_eq_chainHeight_of_chainHeight_ne_top, encard_univ, Submodule.spanFinrank_span_le_encard, Matroid.Indep.encard_le_eRank, Matrix.eRank_diagonal, Metric.IsCover.coveringNumber_le_encard, measurable_encard, Matroid.eRk_le_iff, one_le_encard_insert, Nonempty.encard_pos, SimpleGraph.IsVertexCover.vertexCoverNum_le, Matroid.indep_iff_eRk_eq_encard_of_finite, encard_iUnion_le_of_finite, AddCircle.card_torsion_le_of_isSMulRegular_int, Ideal.height_le_ringKrullDim_quotient_add_encard, encard_eq_coe_toFinset_card, Matroid.IsCircuit.eRk_add_one_eq, toENat_rank_span_set, encard_mono, encard_singleton_inter, Infinite.encard_eq, Matroid.ExchangeProperty.encard_diff_le_aux, Function.Injective.encard_image, encard_le_coe_iff_finite_ncard_le, encard_eq_one, encard_eq_add_one_iff, encard_le_encard_iff_encard_diff_le_encard_diff, encard_ne_add_one, Matroid.eRank_add_eRank_dual, Matroid.eRk_lt_encard_of_dep_of_finite, InjOn.encard_image, Finite.exists_encard_eq_coe, Matroid.indep_iff_eRk_eq_encard, encard_eq_four, Finite.encard_eq_coe, Matroid.eRk_freeOn, encard_image_le, Matroid.eRk_union_le_encard_add_eRk, Matroid.eRk_union_le_eRk_add_encard, encard_coe_eq_coe_finsetCard, toENat_cardinalMk, encard_smul_set, one_lt_encard_iff, encard_pos, SimpleGraph.vertexCoverNum_exists, encard_le_coe_iff, encard_eq_two, encard_lt_encard_iff_encard_diff_lt_encard_diff, encard_pi_eq_prod_encard, encard_le_chainHeight_of_isChain, encard_diff, Matroid.ExchangeProperty.encard_isBase_eq, Ideal.height_le_height_add_encard_of_subset, Matroid.Dep.eRk_lt_encard, Metric.externalCoveringNumber_le_encard_self, Finite.encard_biUnion, Finite.encard_eq_coe_toFinset_card, Matroid.isBasis'_iff_indep_encard_eq_of_finite, encard_insert_le, encard_le_one_iff, Metric.encard_maximalSeparatedSet, encard_diff_singleton_add_one, Metric.IsSeparated.encard_le_packingNumber, encard_le_encard_of_injOn, encard_tsub_one_le_encard_diff_singleton, LinearIndepOn.encard_le_toENat_rank, Matroid.eq_eRk_iff, one_lt_encard_iff_nontrivial, Metric.packingNumber_zero, exists_isChain_of_le_chainHeight, ENat.card_coe_set_eq, encard_diff_add_encard_inter, Function.Injective.encard_range, encard_le_one_iff_eq, encard_add_encard_compl, encard_le_encard, Metric.exists_set_encard_eq_packingNumber, Metric.encard_le_of_isSeparated, Matroid.eRk_le_encard, encard_exchange', encard_iUnion_le_of_fintype, one_le_encard_iff_nonempty, Submodule.FG.exists_span_set_encard_eq_spanFinrank, encard_eq_chainHeight_of_isChain, encard_insert_of_notMem, encard_diff_singleton_of_mem, Metric.coveringNumber_le_encard_self, chainHeight_eq_iSup, Finite.cast_ncard_eq, Matroid.ExchangeProperty.encard_diff_eq, Finite.encard_biUnion_le, exists_eq_chainHeight_of_finite, Metric.packingNumber_le_encard_self, Matroid.IsBase.encard_compl_eq, Finite.encard_strictMonoOn, encard_le_one_iff_subsingleton, encard_singleton, SimpleGraph.exists_of_le_vertexCoverNum, Metric.externalCoveringNumber_zero, Matroid.IsBasis'.encard_eq_encard, encard_preimage_of_bijective, encard_le_encard_diff_add_encard, ringKrullDim_le_ringKrullDim_quotient_add_encard, encard_inv, encard_vadd_set, chainHeight_eq_top_iff
|
ncard 📖 | CompOp | 175 mathmath: ncard_vadd_set, ncard_mono, ncard_image_le, even_ncard_compl_iff, ncard_eq_four, MulAction.IsBlock.ncard_dvd_card, Matroid.IsBase.ncard_eq_ncard_of_isBase, ncard_subtype, finsum_one, ncard_eq_three, IsCyclotomicExtension.Rat.ncard_primesOver_of_prime_pow, ncard_le_encard, Submodule.spanFinrank_span_le_ncard_of_finite, ncard_exchange', Infinite.ncard, SimpleGraph.Walk.IsPath.ncard_neighborSet_toSubgraph_internal_eq_two, AddAction.IsBlock.ncard_block_add_ncard_orbit_eq, ncard_def, AddSubgroup.IsComplement.ncard_right, three_lt_ncard_iff, Ideal.ncard_primesOver_mul_ncard_primesOver, ncard_inv, ncard_le_one_iff_subset_singleton, ncard_Ioo_nat, ncard_Ico_nat, odd_ncard_compl_iff, ncard_Iio_nat, three_lt_ncard, ncard_diff_add_ncard_of_subset, odd_card_insert_iff, SimpleGraph.IsClique.even_iff_exists_isMatching, ncard_eq_two, SimpleGraph.ncard_oddComponents_mono, one_lt_ncard, SimpleGraph.ConnectedComponent.even_ncard_supp_sdiff_rep, one_le_primesOver_ncard, ProbabilityTheory.setBernoulli_singleton, MulAction.index_stabilizer, ncard_eq_of_bijective, ncard_le_card, Polynomial.card_eq_of_natDegree_le_of_coeff_le, ncard_le_ncard_insert, ncard_Iic_nat, ncard_lt_card, SubAddAction.ofFixingAddSubgroup.append_left, exists_eq_insert_iff_ncard, ncard_empty, ncard_diff_singleton_le, ncard_uIcc_nat, ncard_map, ncard_le_one_iff_subsingleton, SimpleGraph.ConnectedComponent.Represents.ncard_sdiff_of_mem, one_lt_ncard_iff_nontrivial, ncard_compl, ncard_eq_one, Setoid.IsPartition.ncard_eq_finsum, Ideal.height_le_card_of_mem_minimalPrimes_span, ncard_le_one, ncard_smul_set, ncard_union_eq, SimpleGraph.Walk.IsCycle.ncard_neighborSet_toSubgraph_eq_two, ncard_Icc_nat, ncard_le_ncard_image_add_one_iff, ncard_le_one_of_subsingleton, ncard_congr, even_card_insert_iff, ncard_inter_add_ncard_union, Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn, ncard_diff_add_ncard, Nat.card_coe_set_eq, Finset.set_ncard_biUnion_le, ncard_graphOn, ncard_inter_le_ncard_left, ncard_coe, one_le_ncard_insert, ncard_insert_eq_ite, ncard_powerset, ncard_add_ncard_compl, Subgroup.IsComplement.ncard_right, ncard_eq_zero, ncard_inter_add_ncard_diff_eq_ncard, ncard_le_ncard_iff_ncard_diff_le_ncard_diff, ncard_union_le, SimpleGraph.ConnectedComponent.Represents.ncard_eq, ncard_pair, ncard_eq_toFinset_card', ncard_diff_singleton_add_one, Nonempty.ncard_pos, ncard_le_ncard_diff_add_ncard, IsCyclotomicExtension.Rat.ncard_primesOver_of_prime, ncard_union_lt, ncard_le_one_iff_eq, RootPairing.ncard_eq_finrank_of_linearIndepOn_of, ncard_Ioc_nat, two_lt_ncard, two_lt_ncard_iff, ncard_iUnion_le_of_fintype, encard_le_coe_iff_finite_ncard_le, Matroid.IsBase.ncard_diff_comm, Nat.count_le_setNCard, Finite.ncard_biUnion, ncard_insert_of_mem, SubMulAction.ofFixingSubgroup.append_left, MulAction.IsBlock.ncard_block_eq_relIndex, Finite.ncard_biUnion_le, MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup_eq, AddAction.IsBlock.ncard_dvd_card, PowerSeries.exist_eq_span_eq_ncard_of_X_notMem, pred_ncard_le_ncard_diff_singleton, ncard_prod, ncard_le_one_iff, ncard_preimage_of_injective_subset_range, SubMulAction.ofFixingSubgroup.append_right, ncard_union_eq_iff, InjOn.ncard_image, exists_union_disjoint_cardinal_eq_iff, cast_ncard, Infinite.exists_subset_ncard_eq, ncard_diff, SimpleGraph.even_ncard_image_val_supp_sdiff_image_val_rep_union, cast_ncard_sdiff, ncard_iUnion_of_finite, MulAction.IsBlock.ncard_block_mul_ncard_orbit_eq, ncard_congr', ncard_lt_ncard, ncard_pos, eq_univ_iff_ncard, ncard_union_add_ncard_inter, Matrix.trace_permutation, le_ncard_of_inj_on_range, SimpleGraph.odd_ncard_oddComponents, Submodule.FG.generators_ncard, ncard_insert_le, Polynomial.ncard_rootSet_le, ncard_image_of_injective, ncard_image_of_injOn, SimpleGraph.ConnectedComponent.Represents.ncard_inter, AddSubgroup.IsComplement.ncard_left, ncard_inter_le_ncard_right, one_lt_ncard_iff_nontrivial_and_finite, ncard_eq_toFinset_card, ncard_singleton, SubAddAction.ofFixingAddSubgroup.append_right, Ideal.ncard_primesOver_mul_card_inertia_mul_finrank, ncard_image_iff, ncard_diff_singleton_lt_of_mem, Finite.ncard_strictMonoOn, Subgroup.IsComplement.ncard_left, DomMulAct.stabilizer_ncard, SimpleGraph.ConnectedComponent.Represents.ncard_sdiff_of_notMem, ncard_univ, ncard_insert_of_notMem, ncard_eq_succ, ncard_le_ncard, one_lt_ncard_iff, Finite.cast_ncard_eq, powersetCard.ncard_eq, ncard_neg, SimpleGraph.ConnectedComponent.odd_oddComponents_ncard_subset_supp, ncard_strictMono, AddAction.IsBlock.ncard_block_eq_relIndex, AddAction.index_stabilizer, ncard_range_of_injective, Group.sum_card_conj_classes_eq_card, ncard_coe_finset, ncard_lt_ncard_iff_ncard_diff_lt_ncard_diff, Polynomial.card_mahlerMeasure_le_prod, ncard_exchange, ncard_eq_ncard_iff_ncard_diff_eq_ncard_diff, ncard_diff_singleton_of_mem, ncard_le_ncard_of_injOn, le_ncard_diff, ncard_singleton_inter, ncard_iUnion_le_of_finite, measurable_ncard
|
tacticToFinite_tac 📖 | CompOp | — |
tacticTo_encard_tac 📖 | CompOp | — |