Documentation

Mathlib.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 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
  • One or more equations did not get rendered due to their size.
Instances For
    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
    Instances For
      theorem Nat.card_eq (α : Type u_4) :
      Nat.card α = if h : Finite α then Fintype.card α else 0
      theorem Finite.card_pos_iff {α : Type u_1} [Finite α] :
      theorem Finite.card_pos {α : Type u_1} [Finite α] [h : Nonempty α] :
      0 < Nat.card α
      theorem Finite.cast_card_eq_mk {α : Type u_4} [Finite α] :
      theorem Finite.card_eq {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] :
      theorem Finite.one_lt_card {α : Type u_1} [Finite α] [h : Nontrivial α] :
      1 < Nat.card α
      @[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 α] :
      theorem Finite.card_le_of_injective' {α : Type u_1} {β : Type u_2} {f : αβ} (hf : Function.Injective f) (h : Nat.card β = 0Nat.card α = 0) :

      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 β = 0Nat.card α = 0) :

      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 α = 0Nat.card β = 0) :

      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 β] :
      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 : αβ) :
      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 Set.card_union_le {α : Type u_1} (s : Set α) (t : Set α) :
      Nat.card (s t) Nat.card s + Nat.card t
      theorem Set.Finite.card_lt_card {α : Type u_1} {s : Set α} {t : Set α} (ht : Set.Finite t) (hsub : s t) :
      Nat.card s < Nat.card t
      theorem Set.Finite.eq_of_subset_of_card_le {α : Type u_1} {s : Set α} {t : Set α} (ht : Set.Finite t) (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 : Set.Finite s) :
      e '' s = s e '' s s