Documentation

Mathlib.SetTheory.Cardinal.Finite

Finite Cardinality Functions #

Main Definitions #

Nat.card α is the cardinality of α as a natural number. If α is infinite, Nat.card α = 0.
PartENat.card α is the cardinality of α as an extended natural number (using Part ℕ). If α is infinite, PartENat.card α = ⊤.

def Nat.card (α : Type u_3) :

Nat.card α is the cardinality of α as a natural number. If α is infinite, Nat.card α = 0.

Equations

Nat.card α = ↑Cardinal.toNat (Cardinal.mk α)

Instances For

@[simp]

theorem Nat.card_eq_fintype_card {α : Type u_1} [Fintype α] :

Nat.card α = Fintype.card α

@[simp]

theorem Nat.card_eq_zero_of_infinite {α : Type u_1} [Infinite α] :

Nat.card α = 0

theorem Nat.finite_of_card_ne_zero {α : Type u_1} (h : Nat.card α ≠ 0) :

theorem Nat.card_congr {α : Type u_1} {β : Type u_2} (f : α ≃ β) :

Nat.card α = Nat.card β

theorem Nat.card_eq_of_bijective {α : Type u_1} {β : Type u_2} (f : α → β) (hf : Function.Bijective f) :

Nat.card α = Nat.card β

theorem Nat.card_eq_of_equiv_fin {α : Type u_3} {n : ℕ} (f : α ≃ Fin n) :

Nat.card α = n

def Nat.equivFinOfCardPos {α : Type u_3} (h : Nat.card α ≠ 0) :

α ≃ Fin (Nat.card α)

If the cardinality is positive, that means it is a finite type, so there is an equivalence between α and Fin (Nat.card α). See also Finite.equivFin.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Nat.card_of_subsingleton {α : Type u_1} (a : α) [Subsingleton α] :

Nat.card α = 1

theorem Nat.card_unique {α : Type u_1} [Unique α] :

Nat.card α = 1

theorem Nat.card_eq_one_iff_unique {α : Type u_1} :

Nat.card α = 1 ↔ Subsingleton α ∧ Nonempty α

theorem Nat.card_eq_two_iff {α : Type u_1} :

Nat.card α = 2 ↔ ∃ x y, x ≠ y ∧ {x, y} = Set.univ

theorem Nat.card_eq_two_iff' {α : Type u_1} (x : α) :

Nat.card α = 2 ↔ ∃! y, y ≠ x

theorem Nat.card_of_isEmpty {α : Type u_1} [IsEmpty α] :

Nat.card α = 0

@[simp]

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

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

@[simp]

theorem Nat.card_prod (α : Type u_3) (β : Type u_4) :

Nat.card (α × β) = Nat.card α * Nat.card β

@[simp]

theorem Nat.card_ulift (α : Type u_3) :

Nat.card (ULift.{u_4, u_3} α) = Nat.card α

@[simp]

theorem Nat.card_plift (α : Type u_3) :

Nat.card (PLift α) = Nat.card α

theorem Nat.card_pi {α : Type u_1} {β : α → Type u_3} [Fintype α] :

Nat.card ((a : α) → β a) = Finset.prod Finset.univ fun a => Nat.card (β a)

theorem Nat.card_fun {α : Type u_1} {β : Type u_2} [Finite α] :

Nat.card (α → β) = Nat.card β ^ Nat.card α

@[simp]

theorem Nat.card_zmod (n : ℕ) :

Nat.card (ZMod n) = n

def PartENat.card (α : Type u_3) :

PartENat.card α is the cardinality of α as an extended natural number. If α is infinite, PartENat.card α = ⊤.

Equations

PartENat.card α = ↑Cardinal.toPartENat (Cardinal.mk α)

Instances For

@[simp]

theorem PartENat.card_eq_coe_fintype_card {α : Type u_1} [Fintype α] :

PartENat.card α = ↑(Fintype.card α)

@[simp]

theorem PartENat.card_eq_top_of_infinite {α : Type u_1} [Infinite α] :

PartENat.card α = ⊤

@[simp]

theorem PartENat.card_sum (α : Type u_3) (β : Type u_4) :

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

theorem PartENat.card_congr {α : Type u_3} {β : Type u_4} (f : α ≃ β) :

PartENat.card α = PartENat.card β

theorem PartENat.card_uLift (α : Type u_3) :

PartENat.card (ULift.{u_4, u_3} α) = PartENat.card α

@[simp]

theorem PartENat.card_pLift (α : Type u_3) :

PartENat.card (PLift α) = PartENat.card α

theorem PartENat.card_image_of_injOn {α : Type u} {β : Type v} {f : α → β} {s : Set α} (h : Set.InjOn f s) :

PartENat.card ↑(f '' s) = PartENat.card ↑s

theorem PartENat.card_image_of_injective {α : Type u} {β : Type v} (f : α → β) (s : Set α) (h : Function.Injective f) :

PartENat.card ↑(f '' s) = PartENat.card ↑s

@[simp]

theorem Cardinal.natCast_le_toPartENat_iff {n : ℕ} {c : Cardinal.{u_3}} :

↑n ≤ ↑Cardinal.toPartENat c ↔ ↑n ≤ c

@[simp]

theorem Cardinal.toPartENat_le_natCast_iff {c : Cardinal.{u_3}} {n : ℕ} :

↑Cardinal.toPartENat c ≤ ↑n ↔ c ≤ ↑n

@[simp]

theorem Cardinal.natCast_eq_toPartENat_iff {n : ℕ} {c : Cardinal.{u_3}} :

↑n = ↑Cardinal.toPartENat c ↔ ↑n = c

@[simp]

theorem Cardinal.toPartENat_eq_natCast_iff {c : Cardinal.{u_3}} {n : ℕ} :

↑Cardinal.toPartENat c = ↑n ↔ c = ↑n

@[simp]

theorem Cardinal.natCast_lt_toPartENat_iff {n : ℕ} {c : Cardinal.{u_3}} :

↑n < ↑Cardinal.toPartENat c ↔ ↑n < c

@[simp]

theorem Cardinal.toPartENat_lt_natCast_iff {n : ℕ} {c : Cardinal.{u_3}} :

↑Cardinal.toPartENat c < ↑n ↔ c < ↑n

theorem PartENat.card_eq_zero_iff_empty (α : Type u_3) :

PartENat.card α = 0 ↔ IsEmpty α

theorem PartENat.card_le_one_iff_subsingleton (α : Type u_3) :

PartENat.card α ≤ 1 ↔ Subsingleton α

theorem PartENat.one_lt_card_iff_nontrivial (α : Type u_3) :

1 < PartENat.card α ↔ Nontrivial α