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

source

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

source

@[simp]

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

Nat.card α = Fintype.card α

source

theorem Fintype.card_eq_nat_card {α : Type u_1} :

∀ {x : Fintype α}, Fintype.card α = Nat.card α

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

source

theorem Nat.card_eq_finsetCard {α : Type u_1} (s : Finset α) :

Nat.card { x : α // x ∈ s } = s.card

source

theorem Nat.card_eq_card_toFinset {α : Type u_1} (s : Set α) [Fintype ↑s] :

Nat.card ↑s = (Set.toFinset s).card

source

theorem Nat.card_eq_card_finite_toFinset {α : Type u_1} {s : Set α} (hs : Set.Finite s) :

Nat.card ↑s = (Set.Finite.toFinset hs).card

source

@[simp]

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

Nat.card α = 0

source

@[simp]

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

Nat.card α = 0

source

theorem Set.Infinite.card_eq_zero {α : Type u_1} {s : Set α} (hs : Set.Infinite s) :

Nat.card ↑s = 0

source

theorem Nat.card_eq_zero {α : Type u_1} :

Nat.card α = 0 ↔ IsEmpty α ∨ Infinite α

source

theorem Nat.card_ne_zero {α : Type u_1} :

Nat.card α ≠ 0 ↔ Nonempty α ∧ Finite α

source

theorem Nat.card_pos_iff {α : Type u_1} :

0 < Nat.card α ↔ Nonempty α ∧ Finite α

source

@[simp]

theorem Nat.card_pos {α : Type u_1} [Nonempty α] [Finite α] :

0 < Nat.card α

source

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

Finite α

source

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

Nat.card α = Nat.card β

source

theorem Nat.card_le_card_of_injective {α : Type u} {β : Type v} [Finite β] (f : α → β) (hf : Function.Injective f) :

Nat.card α ≤ Nat.card β

source

theorem Nat.card_le_card_of_surjective {α : Type u} {β : Type v} [Finite α] (f : α → β) (hf : Function.Surjective f) :

Nat.card β ≤ Nat.card α

source

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

Nat.card α = Nat.card β

source

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

Nat.card α = n

source

theorem Nat.card_mono {α : Type u_1} {s : Set α} {t : Set α} (ht : Set.Finite t) (h : s ⊆ t) :

Nat.card ↑s ≤ Nat.card ↑t

source

theorem Nat.card_image_le {α : Type u_1} {s : Set α} :

∀ {α_1 : Type u_3} {f : α → α_1}, Set.Finite s → Nat.card ↑(f '' s) ≤ Nat.card ↑s

source

theorem Nat.card_image_of_injOn {α : Type u_1} {s : Set α} :

∀ {β : Type u_3} {f : α → β}, Set.InjOn f s → Nat.card ↑(f '' s) = Nat.card ↑s

source

theorem Nat.card_image_of_injective {α : Type u_1} :

∀ {β : Type u_3} {f : α → β}, Function.Injective f → ∀ (s : Set α), Nat.card ↑(f '' s) = Nat.card ↑s

source

theorem Nat.card_image_equiv {α : Type u_1} {β : Type u_2} {s : Set α} (e : α ≃ β) :

Nat.card ↑(⇑e '' s) = Nat.card ↑s

source

theorem Nat.card_preimage_of_injOn {β : Type u_2} :

∀ {α : Type u_3} {f : α → β} {s : Set β}, Set.InjOn f (f ⁻¹' s) → s ⊆ Set.range f → Nat.card ↑(f ⁻¹' s) = Nat.card ↑s

source

theorem Nat.card_preimage_of_injective {β : Type u_2} :

∀ {α : Type u_3} {f : α → β} {s : Set β}, Function.Injective f → s ⊆ Set.range f → Nat.card ↑(f ⁻¹' s) = Nat.card ↑s

source

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