data.finite.card

# Cardinality of finite types #

The cardinality of a finite type α is given by nat.card α. This function has the "junk value" of 0 for infinite types, but to ensure the function has valid output, one just needs to know that it's possible to produce a finite instance for the type. (Note: we could have defined a finite.card that required you to supply a finite instance, but (a) the function would be noncomputable anyway so there is no need to supply the instance and (b) the function would have a more complicated dependent type that easily leads to "motive not type correct" errors.)

## Implementation notes #

Theorems about nat.card are sometimes incidentally true for both finite and infinite types. If removing a finiteness constraint results in no loss in legibility, we remove it. We generally put such theorems into the set_theory.cardinal.finite module.

noncomputable def finite.equiv_fin (α : Type u_1) [finite α] :
α fin (nat.card α)

There is (noncomputably) an equivalence between a finite type α and fin (nat.card α).

Equations
noncomputable def finite.equiv_fin_of_card_eq {α : Type u_1} [finite α] {n : } (h : = n) :
α fin n

Similar to finite.equiv_fin but with control over the term used for the cardinality.

Equations
• = eq.rec h
theorem nat.card_eq (α : Type u_1) :
= dite (finite α) (λ (h : finite α), (λ (h : ¬finite α), 0)
theorem finite.card_pos_iff {α : Type u_1} [finite α] :
0 <
theorem finite.card_eq {α : Type u_1} {β : Type u_2} [finite α] [finite β] :
nonempty β)
theorem finite.card_le_one_iff_subsingleton {α : Type u_1} [finite α] :
1
theorem finite.one_lt_card_iff_nontrivial {α : Type u_1} [finite α] :
1 <
theorem finite.one_lt_card {α : Type u_1} [finite α] [h : nontrivial α] :
1 <
@[simp]
theorem finite.card_option {α : Type u_1} [finite α] :
theorem finite.card_le_of_injective {α : Type u_1} {β : Type u_2} [finite β] (f : α → β) (hf : function.injective f) :
theorem finite.card_le_of_embedding {α : Type u_1} {β : Type u_2} [finite β] (f : α β) :
theorem finite.card_le_of_surjective {α : Type u_1} {β : Type u_2} [finite α] (f : α → β) (hf : function.surjective f) :
theorem finite.card_eq_zero_iff {α : Type u_1} [finite α] :
= 0
theorem finite.card_sum {α : Type u_1} {β : Type u_2} [finite α] [finite β] :
nat.card β) =
theorem finite.card_subtype_le {α : Type u_1} [finite α] (p : α → Prop) :
nat.card {x // p x}
theorem finite.card_subtype_lt {α : Type u_1} [finite α] {p : α → Prop} {x : α} (hx : ¬p x) :
nat.card {x // p x} <