Mathlib.Data.Fintype.Prod

Set.toFinset_prod theorem

 (s : Set α) (t : Set β) [Fintype s] [Fintype t] [Fintype (s ×ˢ t)] : (s ×ˢ t).toFinset = s.toFinset ×ˢ t.toFinset

Full source

theorem toFinset_prod (s : Set α) (t : Set β) [Fintype s] [Fintype t] [Fintype (s ×ˢ t)] :
    (s ×ˢ t).toFinset = s.toFinset ×ˢ t.toFinset := by
  ext
  simp

Finite Set Conversion Preserves Cartesian Product

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$ with finite type instances, the finite set corresponding to their Cartesian product $s \timesˢ t$ is equal to the Cartesian product of their corresponding finite sets, i.e., $(s \timesˢ t).\mathrm{toFinset} = s.\mathrm{toFinset} \timesˢ t.\mathrm{toFinset}$.

Set.toFinset_off_diag theorem

{s : Set α} [DecidableEq α] [Fintype s] [Fintype s.offDiag] : s.offDiag.toFinset = s.toFinset.offDiag

Full source

theorem toFinset_off_diag {s : Set α} [DecidableEq α] [Fintype s] [Fintype s.offDiag] :
    s.offDiag.toFinset = s.toFinset.offDiag :=
  Finset.ext <| by simp

Equality of Finite Sets for Off-Diagonal Elements

Informal description

For any set $s$ over a type $\alpha$ with decidable equality, if both $s$ and its off-diagonal $s.\mathrm{offDiag}$ are finite types, then the finite set obtained from the off-diagonal of $s$ is equal to the off-diagonal of the finite set obtained from $s$. In symbols: $$ \mathrm{toFinset}(s.\mathrm{offDiag}) = (\mathrm{toFinset}\, s).\mathrm{offDiag} $$

instFintypeProd instance

(α β : Type*) [Fintype α] [Fintype β] : Fintype (α × β)

Full source

instance instFintypeProd (α β : Type*) [Fintype α] [Fintype β] : Fintype (α × β) :=
  ⟨univ ×ˢ univ, fun ⟨a, b⟩ => by simp⟩

Finite Product of Finite Types

Informal description

For any finite types $\alpha$ and $\beta$, the product type $\alpha \times \beta$ is also finite.

Finset.univ_product_univ theorem

: univ ×ˢ univ = (univ : Finset (α × β))

Full source

@[simp] lemma univ_product_univ : univ ×ˢ univ = (univ : Finset (α × β)) := rfl

Universal Finite Set of Product Type Equals Product of Universal Finite Sets

Informal description

For finite types $\alpha$ and $\beta$, the Cartesian product of their universal finite sets equals the universal finite set of their product type, i.e., $\text{univ}_{\alpha} \times \text{univ}_{\beta} = \text{univ}_{\alpha \times \beta}$.

Finset.product_eq_univ theorem

[Nonempty α] [Nonempty β] : s ×ˢ t = univ ↔ s = univ ∧ t = univ

Full source

@[simp] lemma product_eq_univ [Nonempty α] [Nonempty β] : s ×ˢ t = univ ↔ s = univ ∧ t = univ := by
  simp [eq_univ_iff_forall, forall_and]

Product of Finite Sets is Universal iff Both Sets are Universal

Informal description

For nonempty finite types $\alpha$ and $\beta$, and finite sets $s \subseteq \alpha$, $t \subseteq \beta$, the Cartesian product $s \times t$ equals the universal finite set of $\alpha \times \beta$ if and only if $s$ equals the universal finite set of $\alpha$ and $t$ equals the universal finite set of $\beta$. In other words, $s \times t = \text{univ}_{\alpha \times \beta} \leftrightarrow s = \text{univ}_\alpha \land t = \text{univ}_\beta$.

Fintype.card_prod theorem

(α β : Type*) [Fintype α] [Fintype β] : Fintype.card (α × β) = Fintype.card α * Fintype.card β

Full source

@[simp]
theorem Fintype.card_prod (α β : Type*) [Fintype α] [Fintype β] :
    Fintype.card (α × β) = Fintype.card α * Fintype.card β :=
  card_product _ _

Cardinality of Product of Finite Types

Informal description

infinite_prod theorem

: Infinite (α × β) ↔ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β

Full source

@[simp]
theorem infinite_prod : InfiniteInfinite (α × β) ↔ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β := by
  refine
    ⟨fun H => ?_, fun H =>
      H.elim (and_imp.2 <| @Prod.infinite_of_left α β) (and_imp.2 <| @Prod.infinite_of_right α β)⟩
  rw [and_comm]; contrapose! H; intro H'
  rcases Infinite.nonempty (α × β) with ⟨a, b⟩
  haveI := fintypeOfNotInfinite (H.1 ⟨b⟩); haveI := fintypeOfNotInfinite (H.2 ⟨a⟩)
  exact H'.false

Characterization of Infinite Product Types: $\text{Infinite}(\alpha \times \beta) \leftrightarrow (\text{Infinite}(\alpha) \land \text{Nonempty}(\beta)) \lor (\text{Nonempty}(\alpha) \land \text{Infinite}(\beta))$

Informal description

The product type $\alpha \times \beta$ is infinite if and only if either $\alpha$ is infinite and $\beta$ is nonempty, or $\alpha$ is nonempty and $\beta$ is infinite.

Pi.infinite_of_left instance

{ι : Sort*} {π : ι → Type*} [∀ i, Nontrivial <| π i] [Infinite ι] : Infinite (∀ i : ι, π i)

Full source

instance Pi.infinite_of_left {ι : Sort*} {π : ι → Type*} [∀ i, Nontrivial <| π i] [Infinite ι] :
    Infinite (∀ i : ι, π i) := by
  classical
  choose m n hm using fun i => exists_pair_ne (π i)
  refine Infinite.of_injective (fun i => update m i (n i)) fun x y h => of_not_not fun hne => ?_
  simp_rw [update_eq_iff, update_of_ne hne] at h
  exact (hm x h.1.symm).elim

Infinite Product of Nontrivial Types over Infinite Index

Informal description

For any infinite type $\iota$ and a family of types $\pi_i$ indexed by $\iota$, if each $\pi_i$ is nontrivial, then the product type $\forall i : \iota, \pi_i$ is infinite.

Pi.infinite_of_exists_right theorem

{ι : Sort*} {π : ι → Sort*} (i : ι) [Infinite <| π i] [∀ i, Nonempty <| π i] : Infinite (∀ i : ι, π i)

Full source

/-- If at least one `π i` is infinite and the rest nonempty, the pi type of all `π` is infinite. -/
theorem Pi.infinite_of_exists_right {ι : Sort*} {π : ι → Sort*} (i : ι) [Infinite <| π i]
    [∀ i, Nonempty <| π i] : Infinite (∀ i : ι, π i) := by
  classical
  let ⟨m⟩ := @Pi.instNonempty ι π _
  exact Infinite.of_injective _ (update_injective m i)

Infinite Product Type via Infinite Component

Informal description

Let $\iota$ be a type and $\pi \colon \iota \to \text{Sort}^*$ be a family of types. If there exists an index $i \in \iota$ such that $\pi i$ is infinite, and for every $i \in \iota$ the type $\pi i$ is nonempty, then the product type $\forall i \in \iota, \pi i$ is infinite.

Pi.infinite_of_right instance

{ι : Sort*} {π : ι → Type*} [∀ i, Infinite <| π i] [Nonempty ι] : Infinite (∀ i : ι, π i)

Full source

/-- See `Pi.infinite_of_exists_right` for the case that only one `π i` is infinite. -/
instance Pi.infinite_of_right {ι : Sort*} {π : ι → Type*} [∀ i, Infinite <| π i] [Nonempty ι] :
    Infinite (∀ i : ι, π i) :=
  Pi.infinite_of_exists_right (Classical.arbitrary ι)

Infinite Product of Infinite Types over Nonempty Index

Informal description

For any nonempty type $\iota$ and a family of types $\pi_i$ indexed by $\iota$, if each $\pi_i$ is infinite, then the product type $\forall i : \iota, \pi_i$ is infinite.

Function.infinite_of_left instance

{ι : Sort*} {π : Type*} [Nontrivial π] [Infinite ι] : Infinite (ι → π)

Full source

/-- Non-dependent version of `Pi.infinite_of_left`. -/
instance Function.infinite_of_left {ι : Sort*} {π : Type*} [Nontrivial π] [Infinite ι] :
    Infinite (ι → π) :=
  Pi.infinite_of_left

Infinite Function Space from Infinite Domain to Nontrivial Codomain

Informal description

For any infinite type $\iota$ and a nontrivial type $\pi$, the function type $\iota \to \pi$ is infinite.

Function.infinite_of_right instance

{ι : Sort*} {π : Type*} [Infinite π] [Nonempty ι] : Infinite (ι → π)

Full source

/-- Non-dependent version of `Pi.infinite_of_exists_right` and `Pi.infinite_of_right`. -/
instance Function.infinite_of_right {ι : Sort*} {π : Type*} [Infinite π] [Nonempty ι] :
    Infinite (ι → π) :=
  Pi.infinite_of_right

Infinite Function Space from Nonempty Domain to Infinite Codomain

Informal description

For any nonempty type $\iota$ and an infinite type $\pi$, the function type $\iota \to \pi$ is infinite.