Documentation

Mathlib.SetTheory.Cardinal.Finite

Finite Cardinality Functions #

Main Definitions #

source
noncomputable 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
    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 α} :
    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 ↥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
    theorem Nat.subtype_card {α : Type u_1} {p : α → Prop} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ p x) :
    Nat.card { x : α // p x } = s.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 Nat.cast_card {α : Type u_1} [Finite α] :
    ↑(Nat.card α) = Cardinal.mk α
    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
    instance Nat.instNeZeroCardOfNonemptyOfFinite {α : Type u_1} [Nonempty α] [Finite α] :
    NeZero (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 : Injective f) (hc : Nat.card β ≤ Nat.card α) :
    Bijective f
    source
    theorem Function.Surjective.bijective_of_nat_card_le {α : Type u_1} {β : Type u_2} [Finite α] {f : α → β} (surj : Surjective f) (hc : Nat.card α ≤ Nat.card β) :
    Bijective f
    source
    theorem Nat.card_eq_of_equiv_fin {α : Type u_3} {n : ℕ} (f : α ≃ Fin n) :
    Nat.card α = n
    source
    theorem Nat.card_fin (n : ℕ) :
    Nat.card (Fin n) = 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
    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
    noncomputable 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
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Nat.card_of_subsingleton {α : Type u_1} (a : α) [Subsingleton α] :
      Nat.card α = 1
      source
      theorem Nat.card_eq_one_iff_unique {α : Type u_1} :
      Nat.card α = 1 ↔ Subsingleton α ∧ Nonempty α
      source
      @[simp]
      theorem Nat.card_unique {α : Type u_1} [Nonempty α] [Subsingleton α] :
      Nat.card α = 1
      source
      theorem Nat.card_eq_one_iff_exists {α : Type u_1} :
      Nat.card α = 1 ↔ ∃ (x : α), ∀ (y : α), y = x
      source
      theorem Nat.card_eq_two_iff {α : Type u_1} :
      Nat.card α = 2 ↔ ∃ (x : α) (y : α), x ≠ y ∧ {x, y} = Set.univ
      source
      theorem Nat.card_eq_two_iff' {α : Type u_1} (x : α) :
      Nat.card α = 2 ↔ ∃! y : α, y ≠ x
      source
      @[simp]
      theorem Nat.card_subtype_true {α : Type u_1} :
      Nat.card { _a : α // True } = Nat.card α
      source
      @[simp]
      theorem Nat.card_sum {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] :
      Nat.card (α ⊕ β) = Nat.card α + Nat.card β
      source
      @[simp]
      theorem Nat.card_prod (α : Type u_3) (β : Type u_4) :
      Nat.card (α × β) = Nat.card α * Nat.card β
      source
      @[simp]
      theorem Nat.card_ulift (α : Type u_3) :
      Nat.card (ULift.{u_4, u_3} α) = Nat.card α
      source
      @[simp]
      theorem Nat.card_plift (α : Type u_3) :
      Nat.card (PLift α) = Nat.card α
      source
      theorem Nat.card_sigma {α : Type u_1} {β : α → Type u_3} [Fintype α] [∀ (a : α), Finite (β a)] :
      Nat.card (Sigma β) = ∑ a : α, Nat.card (β a)
      source
      theorem Nat.card_pi {α : Type u_1} {β : α → Type u_3} [Fintype α] :
      Nat.card ((a : α) → β a) = ∏ a : α, Nat.card (β a)
      source
      theorem Nat.card_fun {α : Type u_1} {β : Type u_2} [Finite α] :
      Nat.card (α → β) = Nat.card β ^ Nat.card α
      source
      @[simp]
      theorem Nat.card_zmod (n : ℕ) :
      Nat.card (ZMod n) = n
      source
      theorem Set.card_singleton_prod {α : Type u_1} {β : Type u_2} (a : α) (t : Set β) :
      Nat.card ↑({a} ×ˢ t) = Nat.card ↑t
      source
      theorem Set.card_prod_singleton {α : Type u_1} {β : Type u_2} (s : Set α) (b : β) :
      Nat.card ↑(s ×ˢ {b}) = Nat.card ↑s
      source
      theorem Set.natCard_pos {α : Type u_1} {s : Set α} (hs : s.Finite) :
      0 < Nat.card ↑s ↔ s.Nonempty
      source
      theorem Set.Nonempty.natCard_pos {α : Type u_1} {s : Set α} (hs : s.Finite) :
      s.Nonempty → 0 < Nat.card ↑s

      Alias of the reverse direction of Set.natCard_pos.

      source
      theorem Set.natCard_graphOn {α : Type u_1} {β : Type u_2} (s : Set α) (f : α → β) :
      Nat.card ↑(graphOn f s) = Nat.card ↑s
      source
      noncomputable def ENat.card (α : Type u_3) :
      ℕ∞

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

      Equations
      Instances For
        source
        @[simp]
        theorem ENat.card_eq_coe_fintype_card {α : Type u_1} [Fintype α] :
        card α = ↑(Fintype.card α)
        source
        @[simp]
        theorem ENat.card_eq_top_of_infinite {α : Type u_1} [Infinite α] :
        card α = ⊤
        source
        @[simp]
        theorem ENat.card_eq_top {α : Type u_1} :
        card α = ⊤ ↔ Infinite α
        source
        @[simp]
        theorem ENat.card_lt_top_of_finite {α : Type u_1} [Finite α] :
        card α < ⊤
        source
        @[simp]
        theorem ENat.card_lt_top {α : Type u_1} :
        card α < ⊤ ↔ Finite α
        source
        @[simp]
        theorem ENat.card_sum (α : Type u_3) (β : Type u_4) :
        card (α ⊕ β) = card α + card β
        source
        theorem ENat.card_congr {α : Type u_3} {β : Type u_4} (f : α ≃ β) :
        card α = card β
        source
        @[simp]
        theorem ENat.card_ulift (α : Type u_3) :
        card (ULift.{u_4, u_3} α) = card α
        source
        @[simp]
        theorem ENat.card_plift (α : Type u_3) :
        card (PLift α) = card α
        source
        theorem ENat.card_image_of_injOn {α : Type u_3} {β : Type u_4} {f : α → β} {s : Set α} (h : Set.InjOn f s) :
        card ↑(f '' s) = card ↑s
        source
        theorem ENat.card_image_of_injective {α : Type u_3} {β : Type u_4} (f : α → β) (s : Set α) (h : Function.Injective f) :
        card ↑(f '' s) = card ↑s
        source
        theorem ENat.card_le_card_of_injective {α : Type u_3} {β : Type u_4} {f : α → β} (hf : Function.Injective f) :
        card α ≤ card β
        source
        theorem ENat.card_eq_zero_iff_empty (α : Type u_3) :
        card α = 0 ↔ IsEmpty α
        source
        theorem ENat.card_ne_zero_iff_nonempty (α : Type u_3) :
        card α ≠ 0 ↔ Nonempty α
        source
        @[simp]
        theorem ENat.card_ne_zero {α : Type u_1} [Nonempty α] :
        card α ≠ 0
        source
        theorem ENat.card_pos_iff_nonempty (α : Type u_3) :
        0 < card α ↔ Nonempty α
        source
        theorem ENat.one_le_card_iff_nonempty (α : Type u_3) :
        1 ≤ card α ↔ Nonempty α
        source
        @[simp]
        theorem ENat.card_pos {α : Type u_1} [Nonempty α] :
        0 < card α
        source
        theorem ENat.card_le_one_iff_subsingleton (α : Type u_3) :
        card α ≤ 1 ↔ Subsingleton α
        source
        @[simp]
        theorem ENat.card_le_one {α : Type u_1} [Subsingleton α] :
        card α ≤ 1
        source
        theorem ENat.card_eq_one_iff_unique {α : Type u_3} :
        card α = 1 ↔ Nonempty (Unique α)
        source
        theorem ENat.one_lt_card_iff_nontrivial (α : Type u_3) :
        1 < card α ↔ Nontrivial α
        source
        @[simp]
        theorem ENat.one_lt_card {α : Type u_1} [Nontrivial α] :
        1 < card α
        source
        theorem ENat.exists_ne_ne_of_three_le {α : Type u_1} (h : 3 ≤ card α) (x y : α) :
        ∃ (z : α), z ≠ x ∧ z ≠ y
        source
        @[simp]
        theorem ENat.card_prod (α : Type u_3) (β : Type u_4) :
        card (α × β) = card α * card β
        source
        @[simp]
        theorem ENat.card_fun {α : Type u_3} {β : Type u_4} :
        card (α → β) = card β ^ card α