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, card_eq, card_lt_card, eq_of_subset_of_card_le, equiv_image_eq_iff_subset, card_union_le, eq_top_of_card_le_of_finite	29
Total	31

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_iff 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 📖	—	Nat.card	—	—	card_eq_zero_of_injective Function.Embedding.inj'
card_eq_zero_of_injective 📖	—	Nat.card	—	—	card_eq_zero_of_surjective Function.invFun_surjective
card_eq_zero_of_surjective 📖	—	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' 📖	—	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' 📖	—	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' 📖	—	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

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_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
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
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