mathlib3 documentation

data.finite.card

Cardinality of finite types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

finite.equiv_fin α = _.mpr (nonempty.some _)

noncomputable def finite.equiv_fin_of_card_eq {α : Type u_1} [finite α] {n : ℕ} (h : nat.card α = n) :

α ≃ fin n

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

Equations

finite.equiv_fin_of_card_eq h = eq.rec (finite.equiv_fin α) h

theorem nat.card_eq (α : Type u_1) :

nat.card α = dite (finite α) (λ (h : finite α), fintype.card α) (λ (h : ¬finite α), 0)

theorem finite.card_pos_iff {α : Type u_1} [finite α] :

0 < nat.card α ↔ nonempty α

theorem finite.card_pos {α : Type u_1} [finite α] [h : nonempty α] :

0 < nat.card α

theorem finite.cast_card_eq_mk {α : Type u_1} [finite α] :

↑(nat.card α) = cardinal.mk α

theorem finite.card_eq {α : Type u_1} {β : Type u_2} [finite α] [finite β] :

nat.card α = nat.card β ↔ nonempty (α ≃ β)

theorem finite.card_le_one_iff_subsingleton {α : Type u_1} [finite α] :

nat.card α ≤ 1 ↔ subsingleton α

theorem finite.one_lt_card_iff_nontrivial {α : Type u_1} [finite α] :

1 < nat.card α ↔ nontrivial α

theorem finite.one_lt_card {α : Type u_1} [finite α] [h : nontrivial α] :

1 < nat.card α

@[simp]

theorem finite.card_option {α : Type u_1} [finite α] :

nat.card (option α) = nat.card α + 1

theorem finite.card_le_of_injective {α : Type u_1} {β : Type u_2} [finite β] (f : α → β) (hf : function.injective f) :

nat.card α ≤ nat.card β

theorem finite.card_le_of_embedding {α : Type u_1} {β : Type u_2} [finite β] (f : α ↪ β) :

nat.card α ≤ nat.card β

theorem finite.card_le_of_surjective {α : Type u_1} {β : Type u_2} [finite α] (f : α → β) (hf : function.surjective f) :

nat.card β ≤ nat.card α

theorem finite.card_eq_zero_iff {α : Type u_1} [finite α] :

nat.card α = 0 ↔ is_empty α

theorem finite.card_le_of_injective' {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.injective f) (h : nat.card β = 0 → nat.card α = 0) :

nat.card α ≤ nat.card β

If f is injective, then nat.card α ≤ nat.card β. We must also assume nat.card β = 0 → nat.card α = 0 since nat.card is defined to be 0 for infinite types.

theorem finite.card_le_of_embedding' {α : Type u_1} {β : Type u_2} (f : α ↪ β) (h : nat.card β = 0 → nat.card α = 0) :

nat.card α ≤ nat.card β

If f is an embedding, then nat.card α ≤ nat.card β. We must also assume nat.card β = 0 → nat.card α = 0 since nat.card is defined to be 0 for infinite types.

theorem finite.card_le_of_surjective' {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.surjective f) (h : nat.card α = 0 → nat.card β = 0) :

nat.card β ≤ nat.card α

If f is surjective, then nat.card β ≤ nat.card α. We must also assume nat.card α = 0 → nat.card β = 0 since nat.card is defined to be 0 for infinite types.

theorem finite.card_eq_zero_of_surjective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.surjective f) (h : nat.card β = 0) :

nat.card α = 0

NB: nat.card is defined to be 0 for infinite types.

theorem finite.card_eq_zero_of_injective {α : Type u_1} {β : Type u_2} [nonempty α] {f : α → β} (hf : function.injective f) (h : nat.card α = 0) :

nat.card β = 0

NB: nat.card is defined to be 0 for infinite types.

theorem finite.card_eq_zero_of_embedding {α : Type u_1} {β : Type u_2} [nonempty α] (f : α ↪ β) (h : nat.card α = 0) :

nat.card β = 0

NB: nat.card is defined to be 0 for infinite types.

theorem finite.card_sum {α : Type u_1} {β : Type u_2} [finite α] [finite β] :

nat.card (α ⊕ β) = nat.card α + nat.card β

theorem finite.card_image_le {α : Type u_1} {β : Type u_2} {s : set α} [finite ↥s] (f : α → β) :

nat.card ↥(f '' s) ≤ nat.card ↥s

theorem finite.card_range_le {α : Type u_1} {β : Type u_2} [finite α] (f : α → β) :

nat.card ↥(set.range f) ≤ nat.card α

theorem finite.card_subtype_le {α : Type u_1} [finite α] (p : α → Prop) :

nat.card {x // p x} ≤ nat.card α

theorem finite.card_subtype_lt {α : Type u_1} [finite α] {p : α → Prop} {x : α} (hx : ¬p x) :

nat.card {x // p x} < nat.card α

theorem part_enat.card_eq_coe_nat_card (α : Type u_1) [finite α] :

part_enat.card α = ↑(nat.card α)

theorem set.card_union_le {α : Type u_1} (s t : set α) :

nat.card ↥(s ∪ t) ≤ nat.card ↥s + nat.card ↥t