# 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
Instances For
@[simp]
theorem Nat.card_eq_fintype_card {α : Type u_1} [] :
theorem Fintype.card_eq_nat_card {α : Type u_1} :
∀ {x : },

Because this theorem takes Fintype α as a non-instance argument, it can be used in particular when Fintype.card ends up with different instance than the one found by inference

theorem Nat.card_eq_finsetCard {α : Type u_1} (s : ) :
Nat.card { x : α // x s } = s.card
theorem Nat.card_eq_card_toFinset {α : Type u_1} (s : Set α) [Fintype s] :
Nat.card s = s.toFinset.card
theorem Nat.card_eq_card_finite_toFinset {α : Type u_1} {s : Set α} (hs : s.Finite) :
Nat.card s = hs.toFinset.card
@[simp]
theorem Nat.card_of_isEmpty {α : Type u_1} [] :
= 0
@[simp]
theorem Nat.card_eq_zero_of_infinite {α : Type u_1} [] :
= 0
theorem Set.Infinite.card_eq_zero {α : Type u_1} {s : Set α} (hs : s.Infinite) :
Nat.card s = 0
theorem Nat.card_eq_zero {α : Type u_1} :
= 0
theorem Nat.card_ne_zero {α : Type u_1} :
0
theorem Nat.card_pos_iff {α : Type u_1} :
0 <
@[simp]
theorem Nat.card_pos {α : Type u_1} [] [] :
0 <
theorem Nat.finite_of_card_ne_zero {α : Type u_1} (h : 0) :
theorem Nat.card_congr {α : Type u_1} {β : Type u_2} (f : α β) :
theorem Nat.card_le_card_of_injective {α : Type u} {β : Type v} [] (f : αβ) (hf : ) :
theorem Nat.card_le_card_of_surjective {α : Type u} {β : Type v} [] (f : αβ) (hf : ) :
theorem Nat.card_eq_of_bijective {α : Type u_1} {β : Type u_2} (f : αβ) (hf : ) :
theorem Nat.bijective_iff_injective_and_card {α : Type u_1} {β : Type u_2} [] (f : αβ) :
theorem Nat.bijective_iff_surjective_and_card {α : Type u_1} {β : Type u_2} [] (f : αβ) :
theorem Function.Injective.bijective_of_nat_card_le {α : Type u_1} {β : Type u_2} [] {f : αβ} (inj : ) (hc : ) :
theorem Function.Surjective.bijective_of_nat_card_le {α : Type u_1} {β : Type u_2} [] {f : αβ} (surj : ) (hc : ) :
theorem Nat.card_eq_of_equiv_fin {α : Type u_3} {n : } (f : α Fin n) :
= n
theorem Nat.card_mono {α : Type u_1} {s : Set α} {t : Set α} (ht : t.Finite) (h : s t) :
theorem Nat.card_image_le {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} (hs : s.Finite) :
Nat.card (f '' s) Nat.card s
theorem Nat.card_image_of_injOn {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} (hf : ) :
Nat.card (f '' s) = Nat.card s
theorem Nat.card_image_of_injective {α : Type u_1} {β : Type u_2} {f : αβ} (hf : ) (s : Set α) :
Nat.card (f '' s) = Nat.card s
theorem Nat.card_image_equiv {α : Type u_1} {β : Type u_2} {s : Set α} (e : α β) :
Nat.card (e '' s) = Nat.card s
theorem Nat.card_preimage_of_injOn {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set β} (hf : Set.InjOn f (f ⁻¹' s)) (hsf : s ) :
Nat.card (f ⁻¹' s) = Nat.card s
theorem Nat.card_preimage_of_injective {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set β} (hf : ) (hsf : s ) :
Nat.card (f ⁻¹' s) = Nat.card s
def Nat.equivFinOfCardPos {α : Type u_3} (h : 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 : α) [] :
= 1
theorem Nat.card_unique {α : Type u_1} [] :
= 1
theorem Nat.card_eq_one_iff_unique {α : Type u_1} :
= 1
theorem Nat.card_eq_one_iff_exists {α : Type u_1} :
= 1 ∃ (x : α), ∀ (y : α), y = x
theorem Nat.card_eq_two_iff {α : Type u_1} :
= 2 ∃ (x : α) (y : α), x y {x, y} = Set.univ
theorem Nat.card_eq_two_iff' {α : Type u_1} (x : α) :
= 2 ∃! y : α, y x
@[simp]
theorem Nat.card_sum {α : Type u_1} {β : Type u_2} [] [] :
Nat.card (α β) =
@[simp]
theorem Nat.card_prod (α : Type u_3) (β : Type u_4) :
Nat.card (α × β) =
@[simp]
theorem Nat.card_ulift (α : Type u_3) :
@[simp]
theorem Nat.card_plift (α : Type u_3) :
theorem Nat.card_pi {α : Type u_1} {β : αType u_3} [] :
Nat.card ((a : α) → β a) = a : α, Nat.card (β a)
theorem Nat.card_fun {α : Type u_1} {β : Type u_2} [] :
Nat.card (αβ) =
@[simp]
theorem Nat.card_zmod (n : ) :
theorem Set.card_singleton_prod {α : Type u_1} {β : Type u_2} (a : α) (t : Set β) :
Nat.card ({a} ×ˢ t) = Nat.card t
theorem Set.card_prod_singleton {α : Type u_1} {β : Type u_2} (s : Set α) (b : β) :
Nat.card (s ×ˢ {b}) = Nat.card s
def PartENat.card (α : Type u_3) :

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

Equations
Instances For
@[simp]
theorem PartENat.card_eq_coe_fintype_card {α : Type u_1} [] :
= (Fintype.card α)
@[simp]
theorem PartENat.card_eq_top_of_infinite {α : Type u_1} [] :
@[simp]
theorem PartENat.card_sum (α : Type u_3) (β : Type u_4) :
theorem PartENat.card_congr {α : Type u_3} {β : Type u_4} (f : α β) :
@[simp]
@[simp]
theorem PartENat.card_plift (α : Type u_3) :
theorem PartENat.card_image_of_injOn {α : Type u} {β : Type v} {f : αβ} {s : Set α} (h : ) :
PartENat.card (f '' s) =
theorem PartENat.card_image_of_injective {α : Type u} {β : Type v} (f : αβ) (s : Set α) (h : ) :
PartENat.card (f '' 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