Mathlib.SetTheory.Cardinal.Finsupp

Cardinal.mk_finsupp_lift_of_fintype theorem

(α : Type u) (β : Type v) [Fintype α] [Zero β] : #(α →₀ β) = lift.{u} #β ^ Fintype.card α

Full source

@[simp]
theorem mk_finsupp_lift_of_fintype (α : Type u) (β : Type v) [Fintype α] [Zero β] :
    #(α →₀ β) = lift.{u} #β ^ Fintype.card α := by
  simpa using (@Finsupp.equivFunOnFinite α β _ _).cardinal_eq

Cardinality of Finitely Supported Functions on a Finite Type

Informal description

For a finite type $\alpha$ and a type $\beta$ with a zero element, the cardinality of the type of finitely supported functions $\alpha \to₀ \beta$ is equal to the cardinality of $\beta$ raised to the power of the cardinality of $\alpha$, where the cardinality of $\beta$ is lifted to the universe level of $\alpha$.

Cardinal.mk_finsupp_of_fintype theorem

(α β : Type u) [Fintype α] [Zero β] : #(α →₀ β) = #β ^ Fintype.card α

Full source

theorem mk_finsupp_of_fintype (α β : Type u) [Fintype α] [Zero β] :
    #(α →₀ β) = #β ^ Fintype.card α := by simp

Cardinality of Finitely Supported Functions on a Finite Type: $\#(\alpha \to₀ \beta) = \#\beta^{\#\alpha}$

Informal description

For a finite type $\alpha$ and a type $\beta$ with a zero element, the cardinality of the type of finitely supported functions $\alpha \to₀ \beta$ is equal to the cardinality of $\beta$ raised to the power of the cardinality of $\alpha$, i.e., $\#(\alpha \to₀ \beta) = \#\beta^{\#\alpha}$.

Cardinal.mk_finsupp_lift_of_infinite theorem

 (α : Type u) (β : Type v) [Infinite α] [Zero β] [Nontrivial β] : #(α →₀ β) = max (lift.{v} #α) (lift.{u} #β)

Full source

@[simp]
theorem mk_finsupp_lift_of_infinite (α : Type u) (β : Type v) [Infinite α] [Zero β] [Nontrivial β] :
    #(α →₀ β) = max (lift.{v} #α) (lift.{u} #β) := by
  apply le_antisymm
  · calc
      #(α →₀ β) ≤ #(Finset (α × β)) := mk_le_of_injective (Finsupp.graph_injective α β)
      _ = #(α × β) := mk_finset_of_infinite _
      _ = max (lift.{v} #α) (lift.{u} #β) := by
        rw [mk_prod, mul_eq_max_of_aleph0_le_left] <;> simp

  · apply max_le <;> rw [← lift_id #(α →₀ β), ← lift_umax]
    · obtain ⟨b, hb⟩ := exists_ne (0 : β)
      exact lift_mk_le.{v}.2 ⟨⟨_, Finsupp.single_left_injective hb⟩⟩
    · inhabit α
      exact lift_mk_le.{u}.2 ⟨⟨_, Finsupp.single_injective default⟩⟩

Cardinality of Finitely Supported Functions on Infinite Domain: $\#(\alpha \to_{\text{f}} \beta) = \max(\#\alpha, \#\beta)$

Informal description

Let $\alpha$ be an infinite type and $\beta$ be a nontrivial type with a zero element. Then the cardinality of the type of finitely supported functions $\alpha \to_{\text{f}} \beta$ is equal to the maximum of the cardinalities of $\alpha$ and $\beta$, where the cardinalities are lifted to appropriate universe levels. That is, $\#(\alpha \to_{\text{f}} \beta) = \max(\#\alpha, \#\beta)$.

Cardinal.mk_finsupp_of_infinite theorem

(α β : Type u) [Infinite α] [Zero β] [Nontrivial β] : #(α →₀ β) = max #α #β

Full source

theorem mk_finsupp_of_infinite (α β : Type u) [Infinite α] [Zero β] [Nontrivial β] :
    #(α →₀ β) = max #α #β := by simp

Cardinality of Finitely Supported Functions on Infinite Domain: $\#(\alpha \to_{\text{f}} \beta) = \max(\#\alpha, \#\beta)$

Informal description

Let $\alpha$ be an infinite type and $\beta$ be a nontrivial type with a zero element. Then the cardinality of the type of finitely supported functions $\alpha \to_{\text{f}} \beta$ is equal to the maximum of the cardinalities of $\alpha$ and $\beta$, i.e., $\#(\alpha \to_{\text{f}} \beta) = \max(\#\alpha, \#\beta)$.

Cardinal.mk_finsupp_lift_of_infinite' theorem

(α : Type u) (β : Type v) [Nonempty α] [Zero β] [Infinite β] : #(α →₀ β) = max (lift.{v} #α) (lift.{u} #β)

Full source

@[simp]
theorem mk_finsupp_lift_of_infinite' (α : Type u) (β : Type v) [Nonempty α] [Zero β] [Infinite β] :
    #(α →₀ β) = max (lift.{v} #α) (lift.{u} #β) := by
  cases fintypeOrInfinite α
  · rw [mk_finsupp_lift_of_fintype]
    have : ℵ₀ ≤ (#β).lift := aleph0_le_lift.2 (aleph0_le_mk β)
    rw [max_eq_right (le_trans _ this), power_nat_eq this]
    exacts [Fintype.card_pos, lift_le_aleph0.2 (lt_aleph0_of_finite _).le]
  · apply mk_finsupp_lift_of_infinite

Cardinality of Finitely Supported Functions on Nonempty Domain with Infinite Codomain: $\#(\alpha \to_{\text{f}} \beta) = \max(\#\alpha, \#\beta)$

Informal description

Let $\alpha$ be a nonempty type and $\beta$ be an infinite type with a zero element. Then the cardinality of the type of finitely supported functions $\alpha \to_{\text{f}} \beta$ is equal to the maximum of the cardinalities of $\alpha$ and $\beta$, where the cardinalities are lifted to appropriate universe levels. That is, $\#(\alpha \to_{\text{f}} \beta) = \max(\#\alpha, \#\beta)$.

Cardinal.mk_finsupp_of_infinite' theorem

(α β : Type u) [Nonempty α] [Zero β] [Infinite β] : #(α →₀ β) = max #α #β

Full source

theorem mk_finsupp_of_infinite' (α β : Type u) [Nonempty α] [Zero β] [Infinite β] :
    #(α →₀ β) = max #α #β := by simp

Cardinality of Finitely Supported Functions on Nonempty Domain with Infinite Codomain: $\#(\alpha \to_{\text{f}} \beta) = \max(\#\alpha, \#\beta)$

Informal description

Let $\alpha$ be a nonempty type and $\beta$ be an infinite type with a zero element. Then the cardinality of the type of finitely supported functions $\alpha \to_{\text{f}} \beta$ is equal to the maximum of the cardinalities of $\alpha$ and $\beta$, i.e., $\#(\alpha \to_{\text{f}} \beta) = \max(\#\alpha, \#\beta)$.

Cardinal.mk_finsupp_nat theorem

(α : Type u) [Nonempty α] : #(α →₀ ℕ) = max #α ℵ₀

Full source

theorem mk_finsupp_nat (α : Type u) [Nonempty α] : #(α →₀ ℕ) = max #α ℵ₀ := by simp

Cardinality of Finitely Supported Functions to Natural Numbers: $\#(\alpha \to_{\text{f}} \mathbb{N}) = \max(\#\alpha, \aleph_0)$

Informal description

For any nonempty type $\alpha$, the cardinality of the type of finitely supported functions from $\alpha$ to $\mathbb{N}$ is equal to the maximum of the cardinality of $\alpha$ and $\aleph_0$. That is, $\#(\alpha \to_{\text{f}} \mathbb{N}) = \max(\#\alpha, \aleph_0)$.

Cardinal.mk_multiset_of_isEmpty theorem

(α : Type u) [IsEmpty α] : #(Multiset α) = 1

Full source

theorem mk_multiset_of_isEmpty (α : Type u) [IsEmpty α] : #(Multiset α) = 1 :=
  Multiset.toFinsupp.toEquiv.cardinal_eq.trans (by simp)

Cardinality of Multisets over an Empty Type is One

Informal description

For any empty type $\alpha$, the cardinality of the type of multisets over $\alpha$ is $1$.

Cardinal.mk_multiset_of_nonempty theorem

(α : Type u) [Nonempty α] : #(Multiset α) = max #α ℵ₀

Full source

@[simp]
theorem mk_multiset_of_nonempty (α : Type u) [Nonempty α] : #(Multiset α) = max #α ℵ₀ := by
  classical
  exact Multiset.toFinsupp.toEquiv.cardinal_eq.trans (mk_finsupp_nat α)

Cardinality of Multisets over Nonempty Type: $\#(\text{Multiset } \alpha) = \max(\#\alpha, \aleph_0)$

Informal description

For any nonempty type $\alpha$, the cardinality of the collection of multisets over $\alpha$ is equal to the maximum of the cardinality of $\alpha$ and $\aleph_0$. That is, $\#(\text{Multiset } \alpha) = \max(\#\alpha, \aleph_0)$.

Cardinal.mk_multiset_of_infinite theorem

(α : Type u) [Infinite α] : #(Multiset α) = #α

Full source

theorem mk_multiset_of_infinite (α : Type u) [Infinite α] : #(Multiset α) = #α := by simp

Cardinality of Multisets over Infinite Type: $\#(\text{Multiset } \alpha) = \#\alpha$

Informal description

For any infinite type $\alpha$, the cardinality of the collection of multisets over $\alpha$ is equal to the cardinality of $\alpha$ itself, i.e., $\#(\text{Multiset } \alpha) = \#\alpha$.

Cardinal.mk_multiset_of_countable theorem

(α : Type u) [Countable α] [Nonempty α] : #(Multiset α) = ℵ₀

Full source

theorem mk_multiset_of_countable (α : Type u) [Countable α] [Nonempty α] : #(Multiset α) = ℵ₀ := by
  classical
  exact Multiset.toFinsupp.toEquiv.cardinal_eq.trans (by simp)

Cardinality of Multisets over a Countable Type: $\#(\text{Multiset } \alpha) = \aleph_0$

Informal description

For any nonempty countable type $\alpha$, the cardinality of the collection of multisets over $\alpha$ is $\aleph_0$ (the cardinality of the natural numbers). That is, $\#(\text{Multiset } \alpha) = \aleph_0$.