Card

📁 Source: Mathlib/Data/Finite/Card.lean

Statistics

Metric	Count
Definitions equivFin, equivFinOfCardEq	2
Theorems card_eq_coe_natCard, card_eq, card_eq_zero_iff, card_eq_zero_of_embedding, card_eq_zero_of_injective, card_eq_zero_of_surjective, card_image_le, card_le_of_embedding, card_le_of_embedding', card_le_of_injective, card_le_of_injective', card_le_of_surjective, card_le_of_surjective', card_le_one_iff_subsingleton, card_option, card_pos, card_pos_iff, card_range_le, card_subtype_le, card_subtype_lt, card_sum, one_lt_card, one_lt_card_iff_nontrivial, length_le_enatCard, length_le_natCard, card_eq, card_lt_card, card_strictMonoOn, ecard_lt_ecard, ecard_strictMonoOn, eq_of_subset_of_card_le, equiv_image_eq_iff_subset, card_strictMono, card_union_le, ecard_le_ecard, ecard_strictMono, eq_top_of_card_le_of_finite	37
Total	39

ENat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_eq_coe_natCard 📖	mathematical	—	card ENat instNatCast Nat.card	—	symm IsEquiv.toSymm eq_isEquiv Cardinal.natCast_eq_toENat Nat.cast_card

Finite

Definitions

Name	Category	Theorems
equivFin 📖	CompOp	—
equivFinOfCardEq 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_eq 📖	mathematical	—	Nat.card Equiv	—	Nat.card_eq_fintype_card
card_eq_zero_iff 📖	mathematical	—	Nat.card IsEmpty	—	Nat.card_eq_fintype_card
card_eq_zero_of_embedding 📖	mathematical	Nat.card	Nat.card	—	card_eq_zero_of_injective Function.Embedding.inj'
card_eq_zero_of_injective 📖	mathematical	Nat.card	Nat.card	—	card_eq_zero_of_surjective Function.invFun_surjective
card_eq_zero_of_surjective 📖	mathematical	Nat.card	Nat.card	—	finite_or_infinite Nat.card_of_isEmpty Function.isEmpty card_eq_zero_iff Nat.card_eq_zero_of_infinite Infinite.of_surjective
card_image_le 📖	mathematical	—	Nat.card Set.Elem Set.image	—	Nat.card_le_card_of_surjective Set.imageFactorization_surjective
card_le_of_embedding 📖	mathematical	—	Nat.card	—	Nat.card_le_card_of_injective Function.Embedding.injective
card_le_of_embedding' 📖	mathematical	Nat.card	Nat.card	—	card_le_of_injective' Function.Embedding.inj'
card_le_of_injective 📖	mathematical	—	Nat.card	—	Nat.card_le_card_of_injective
card_le_of_injective' 📖	mathematical	Nat.card	Nat.card	—	or_not_of_imp Nat.card_le_card_of_injective Nat.finite_of_card_ne_zero
card_le_of_surjective 📖	mathematical	—	Nat.card	—	Nat.card_le_card_of_surjective
card_le_of_surjective' 📖	mathematical	Nat.card	Nat.card	—	or_not_of_imp Nat.card_le_card_of_surjective Nat.finite_of_card_ne_zero
card_le_one_iff_subsingleton 📖	mathematical	—	Nat.card	—	Nat.card_eq_fintype_card
card_option 📖	mathematical	—	Nat.card	—	Nat.card_eq_fintype_card Fintype.card_option
card_pos 📖	mathematical	—	Nat.card	—	card_pos_iff
card_pos_iff 📖	mathematical	—	Nat.card	—	Nat.card_eq_fintype_card Fintype.card_pos_iff
card_range_le 📖	mathematical	—	Nat.card Set.Elem Set.range	—	Nat.card_le_card_of_surjective Set.rangeFactorization_surjective
card_subtype_le 📖	mathematical	—	Nat.card	—	Nat.card_eq_fintype_card Fintype.card_subtype_le
card_subtype_lt 📖	mathematical	—	Nat.card	—	Nat.card_eq_fintype_card Fintype.card_subtype_lt
card_sum 📖	mathematical	—	Nat.card	—	Nat.card_sum
one_lt_card 📖	mathematical	—	Nat.card	—	one_lt_card_iff_nontrivial
one_lt_card_iff_nontrivial 📖	mathematical	—	Nat.card Nontrivial	—	Nat.card_eq_fintype_card

List.Nodup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
length_le_enatCard 📖	mathematical	—	ENat instLEENat ENat.instNatCast ENat.card	—	finite_or_infinite le_imp_le_of_le_of_le Nat.mono_cast IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid length_le_natCard le_refl ENat.card_eq_coe_natCard ENat.card_eq_top_of_infinite le_top
length_le_natCard 📖	mathematical	—	Nat.card	—	le_imp_le_of_le_of_le length_le_card le_refl Fintype.card_eq_nat_card

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_eq 📖	mathematical	—	card Finite Fintype.card Fintype.ofFinite	—	finite_or_infinite card_eq_fintype_card card_eq_zero_of_infinite not_finite_iff_infinite

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_strictMono 📖	mathematical	—	StrictMono Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra Nat.instPreorder Nat.card Elem	—	Finite.card_lt_card toFinite Subtype.finite
card_union_le 📖	mathematical	—	Nat.card Elem Set instUnion	—	finite_or_infinite finite_coe_iff finite_union Nat.cast_le Cardinal.addLeftMono IsOrderedRing.toZeroLEOneClass Cardinal.isOrderedRing Cardinal.instCharZero Nat.cast_add Nat.cast_card Finite.Set.finite_union Cardinal.mk_union_le Eq.trans_le Nat.card_eq_zero_of_infinite zero_le Nat.instCanonicallyOrderedAdd
ecard_le_ecard 📖	mathematical	Set instHasSubset	ENat instLEENat ENat.card Elem	—	ENat.card_le_card_of_injective inclusion_injective
ecard_strictMono 📖	mathematical	—	StrictMono Set ENat PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra instPreorderENat ENat.card Elem	—	Finite.ecard_lt_ecard toFinite Subtype.finite
eq_top_of_card_le_of_finite 📖	mathematical	Nat.card Elem	Top.top Set BooleanAlgebra.toTop instBooleanAlgebra	—	Finite.eq_of_subset_of_card_le toFinite Subtype.finite subset_univ Nat.card_congr

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_lt_card 📖	mathematical	Set Set.instHasSSubset	Nat.card Set.Elem	—	subset subset_of_ssubset Set.instIsNonstrictStrictOrderSubsetSSubset Nat.card_eq_fintype_card Set.card_lt_card
card_strictMonoOn 📖	mathematical	—	StrictMonoOn Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Nat.instPreorder Nat.card Set.Elem setOf Set.Finite	—	card_lt_card
ecard_lt_ecard 📖	mathematical	Set Set.instHasSSubset	ENat instLTENat ENat.card Set.Elem	—	le_add_of_le_right ENat.card_sum ENat.card_congr Set.disjoint_sdiff_left Set.diff_union_of_subset HasSSubset.SSubset.subset Set.instIsNonstrictStrictOrderSubsetSSubset WithTop.le_of_add_le_add_right IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid LT.lt.ne ENat.card_lt_top Set.diff_eq_empty Set.isEmpty_coe_sort ENat.card_eq_zero_iff_empty nonpos_iff_eq_zero lt_of_le_not_ge Set.ecard_le_ecard not_subset_of_ssubset
ecard_strictMonoOn 📖	mathematical	—	StrictMonoOn Set ENat PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPreorderENat ENat.card Set.Elem setOf Set.Finite	—	ecard_lt_ecard
eq_of_subset_of_card_le 📖	—	Set Set.instHasSubset Nat.card Set.Elem	—	—	eq_or_ssubset_of_subset Set.instIsNonstrictStrictOrderSubsetSSubset Set.instAntisymmSubset not_le_of_gt card_lt_card
equiv_image_eq_iff_subset 📖	mathematical	—	Set.image DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Set Set.instHasSubset	—	subset_refl Set.instReflSubset eq_of_subset_of_card_le ge_of_eq Nat.card_congr

---

← Back to Index