scilib 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 α = ⊤