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 SetTheory.Cardinal.Finite module.

def Finite.equivFin (α : Type u_4) [Finite α] : α ≃ Fin (Nat.card α)

There is (noncomputably) an equivalence between a finite type α and Fin (Nat.card α).

Equations

• Finite.equivFin α = ⋯.mpr ⋯.some

def Finite.equivFinOfCardEq {α : Type u_1} [Finite α] {n : ℕ} (h : Nat.card α = n) : α ≃ Fin n

Similar to Finite.equivFin but with control over the term used for the cardinality.

Equations

• Finite.equivFinOfCardEq h = h ▸ Finite.equivFin α

theorem Nat.card_eq (α : Type u_4) : Nat.card α = if x : Finite α then Fintype.card α else 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_4} [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 ↔ IsEmpty α

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 ENat.card_eq_coe_natCard (α : Type u_4) [Finite α] : 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

theorem Set.Finite.card_lt_card {α : Type u_1} {s t : Set α} (ht : t.Finite) (hsub : s ⊂ t) : Nat.card ↑s < Nat.card ↑t

theorem Set.Finite.eq_of_subset_of_card_le {α : Type u_1} {s t : Set α} (ht : t.Finite) (hsub : s ⊆ t) (hcard : Nat.card ↑t ≤ Nat.card ↑s) : s = t

theorem Set.Finite.equiv_image_eq_iff_subset {α : Type u_1} {s : Set α} (e : α ≃ α) (hs : s.Finite) : ⇑e '' s = s ↔ ⇑e '' s ⊆ s

theorem Set.eq_top_of_card_le_of_finite {α : Type u_1} [Finite α] {s : Set α} (h : Nat.card α ≤ Nat.card ↑s) : s = ⊤