Finite Cardinality Functions #

Main Definitions #

Nat.card α is the cardinality of α as a natural number. If α is infinite, Nat.card α = 0.
ENat.card α is the cardinality of α as an extended natural number. If α is infinite, ENat.card α = ⊤.
PartENat.card α is the cardinality of α as an extended natural number (using the legacy definition PartENat := 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 = s.toFinset.card

source

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

Nat.card ↑s = hs.toFinset.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 : s.Infinite) :

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.bijective_iff_injective_and_card {α : Type u_1} {β : Type u_2} [Finite β] (f : α → β) :

Function.Bijective f ↔ Function.Injective f ∧ Nat.card α = Nat.card β

source

theorem Nat.bijective_iff_surjective_and_card {α : Type u_1} {β : Type u_2} [Finite α] (f : α → β) :

Function.Bijective f ↔ Function.Surjective f ∧ Nat.card α = Nat.card β

source

theorem Function.Injective.bijective_of_nat_card_le {α : Type u_1} {β : Type u_2} [Finite β] {f : α → β} (inj : Function.Injective f) (hc : Nat.card β ≤ Nat.card α) :

Function.Bijective f

source

theorem Function.Surjective.bijective_of_nat_card_le {α : Type u_1} {β : Type u_2} [Finite α] {f : α → β} (surj : Function.Surjective f) (hc : Nat.card α ≤ Nat.card β) :

Function.Bijective f

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 t : Set α} (ht : t.Finite) (h : s ⊆ t) :

Nat.card ↑s ≤ Nat.card ↑t

source

theorem Nat.card_image_le {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} (hs : s.Finite) :

Nat.card ↑(f '' s) ≤ Nat.card ↑s

source

theorem Nat.card_image_of_injOn {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} (hf : Set.InjOn f s) :

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

source

theorem Nat.card_image_of_injective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : 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_1} {β : Type u_2} {f : α → β} {s : Set β} (hf : Set.InjOn f (f ⁻¹' s)) (hsf : s ⊆ Set.range f) :

Nat.card ↑(f ⁻¹' s) = Nat.card ↑s

source

theorem Nat.card_preimage_of_injective {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β} (hf : Function.Injective f) (hsf : s ⊆ Set.range f) :

Nat.card ↑(f ⁻¹' s) = Nat.card ↑s

source

@[simp]

theorem Nat.card_univ {α : Type u_1} :

Nat.card ↑Set.univ = Nat.card α

source

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

Nat.card ↑(Set.range f) = Nat.card α

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