mathlib3 documentation

set_theory.cardinal.finite

Finite Cardinality Functions #

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

Main Definitions #

nat.card α is the cardinality of α as a natural number. If α is infinite, nat.card α = 0.
part_enat.card α is the cardinality of α as an extended natural number (part ℕ implementation). If α is infinite, part_enat.card α = ⊤.

@[protected]

noncomputable def nat.card (α : Type u_1) :

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

Equations

nat.card α = ⇑cardinal.to_nat (cardinal.mk α)

@[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_1} {n : ℕ} (f : α ≃ fin n) :

nat.card α = n

noncomputable def nat.equiv_fin_of_card_pos {α : Type u_1} (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.equiv_fin.

Equations

nat.equiv_fin_of_card_pos h = (fintype_or_infinite α).cases_on (λ (val : fintype α), _.mpr (_.mp (fintype.equiv_fin α))) (λ (val : infinite α), _.mpr (false.rec (α ≃ fin 0) _))

theorem nat.card_of_subsingleton {α : Type u_1} (a : α) [subsingleton α] :

nat.card α = 1

@[simp]

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_is_empty {α : Type u_1} [is_empty α] :

nat.card α = 0

@[simp]

theorem nat.card_prod (α : Type u_1) (β : Type u_2) :

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

@[simp]

theorem nat.card_ulift (α : Type u_1) :

nat.card (ulift α) = nat.card α

@[simp]

theorem nat.card_plift (α : Type u_1) :

nat.card (plift α) = nat.card α

theorem nat.card_pi {α : Type u_1} {β : α → Type u_2} [fintype α] :

nat.card (Π (a : α), β a) = finset.univ.prod (λ (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

noncomputable def part_enat.card (α : Type u_1) :

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

Equations

part_enat.card α = ⇑cardinal.to_part_enat (cardinal.mk α)

@[simp]

theorem part_enat.card_eq_coe_fintype_card {α : Type u_1} [fintype α] :

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

@[simp]

theorem part_enat.card_eq_top_of_infinite {α : Type u_1} [infinite α] :

part_enat.card α = ⊤

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

part_enat.card α = part_enat.card β

theorem part_enat.card_ulift (α : Type u_1) :

part_enat.card (ulift α) = part_enat.card α

@[simp]

theorem part_enat.card_plift (α : Type u_1) :

part_enat.card (plift α) = part_enat.card α

theorem part_enat.card_image_of_inj_on {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} (h : set.inj_on f s) :

part_enat.card ↥(f '' s) = part_enat.card ↥s

theorem part_enat.card_image_of_injective {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) (h : function.injective f) :

part_enat.card ↥(f '' s) = part_enat.card ↥s

@[simp]

theorem cardinal.coe_nat_le_to_part_enat_iff {n : ℕ} {c : cardinal} :

↑n ≤ ⇑cardinal.to_part_enat c ↔ ↑n ≤ c

@[simp]

theorem cardinal.to_part_enat_le_coe_nat_iff {c : cardinal} {n : ℕ} :

⇑cardinal.to_part_enat c ≤ ↑n ↔ c ≤ ↑n

@[simp]

theorem cardinal.coe_nat_eq_to_part_enat_iff {n : ℕ} {c : cardinal} :

↑n = ⇑cardinal.to_part_enat c ↔ ↑n = c

@[simp]

theorem cardinal.to_part_enat_eq_coe_nat_iff {c : cardinal} {n : ℕ} :

⇑cardinal.to_part_enat c = ↑n ↔ c = ↑n

@[simp]

theorem cardinal.coe_nat_lt_coe_iff_lt {n : ℕ} {c : cardinal} :

↑n < ⇑cardinal.to_part_enat c ↔ ↑n < c

@[simp]

theorem cardinal.lt_coe_nat_iff_lt {n : ℕ} {c : cardinal} :

⇑cardinal.to_part_enat c < ↑n ↔ c < ↑n

theorem part_enat.card_eq_zero_iff_empty (α : Type u_1) :

part_enat.card α = 0 ↔ is_empty α

theorem part_enat.card_le_one_iff_subsingleton (α : Type u_1) :

part_enat.card α ≤ 1 ↔ subsingleton α

theorem part_enat.one_lt_card_iff_nontrivial (α : Type u_1) :

1 < part_enat.card α ↔ nontrivial α

theorem part_enat.is_finite_of_card {α : Type u_1} {n : ℕ} (hα : part_enat.card α = ↑n) :