doc-next-gen

Mathlib.Data.Finite.Prod

Module docstring

{"# Finiteness of products ","### Fintype instances

Every instance here should have a corresponding Set.Finite constructor in the next section. ","### Finite instances

There is seemingly some overlap between the following instances and the Fintype instances in Data.Set.Finite. While every Fintype instance gives a Finite instance, those instances that depend on Fintype or Decidable instances need an additional Finite instance to be able to generally apply.

Some set instances do not appear here since they are consequences of others, for example Subtype.Finite for subsets of a finite type. ","### Constructors for Set.Finite

Every constructor here should have a corresponding Fintype instance in the previous section (or in the Fintype module).

The implementation of these constructors ideally should be no more than Set.toFinite, after possibly setting up some Fintype and classical Decidable instances. ","### Properties ","### Infinite sets "}

Finite.instPProd instance
{α β : Sort*} [Finite α] [Finite β] : Finite (PProd α β)
Full source 
instance {α β : Sort*} [Finite α] [Finite β] : Finite (PProd α β) :=
  of_equiv _ Equiv.pprodEquivProdPLift.symm
Finiteness of Parallel Product Types
Informal description
For any finite types $\alpha$ and $\beta$, the parallel product type $\mathrm{PProd}\,\alpha\,\beta$ is also finite.
Finite.prod_left theorem
(β) [Finite (α × β)] [Nonempty β] : Finite α
Full source 
theorem prod_left (β) [Finite (α × β)] [Nonempty β] : Finite α :=
  of_surjective (Prod.fst : α × β → α) Prod.fst_surjective
Finiteness of the Left Factor in a Finite Product with Nonempty Right Factor
Informal description
For any types $\alpha$ and $\beta$, if the product type $\alpha \times \beta$ is finite and $\beta$ is nonempty, then $\alpha$ is finite.
Finite.prod_right theorem
(α) [Finite (α × β)] [Nonempty α] : Finite β
Full source 
theorem prod_right (α) [Finite (α × β)] [Nonempty α] : Finite β :=
  of_surjective (Prod.snd : α × β → β) Prod.snd_surjective
Finiteness of the Right Factor in a Finite Product with Nonempty Left Factor
Informal description
For any types $\alpha$ and $\beta$, if the product type $\alpha \times \beta$ is finite and $\alpha$ is nonempty, then $\beta$ is finite.
Pi.finite instance
{α : Sort*} {β : α → Sort*} [Finite α] [∀ a, Finite (β a)] : Finite (∀ a, β a)
Full source 
instance Pi.finite {α : Sort*} {β : α → Sort*} [Finite α] [∀ a, Finite (β a)] :
    Finite (∀ a, β a) := by
  classical
  haveI := Fintype.ofFinite (PLift α)
  haveI := fun a => Fintype.ofFinite (PLift (β a))
  exact
    Finite.of_equiv (∀ a : PLift α, PLift (β (Equiv.plift a)))
      (Equiv.piCongr Equiv.plift fun _ => Equiv.plift)
Finiteness of Dependent Function Types
Informal description
For any finite type $\alpha$ and a family of types $\beta : \alpha \to \text{Type}$ where each $\beta(a)$ is finite, the dependent function type $(\forall a, \beta(a))$ is also finite.
Function.Embedding.finite instance
{α β : Sort*} [Finite β] : Finite (α ↪ β)
Full source 
instance Function.Embedding.finite {α β : Sort*} [Finite β] : Finite (α ↪ β) := by
  rcases isEmpty_or_nonempty (α ↪ β) with _ | h
  · infer_instance
  · refine h.elim fun f => ?_
    haveI : Finite α := Finite.of_injective _ f.injective
    exact Finite.of_injective _ DFunLike.coe_injective
Finiteness of Injective Function Embeddings from Any Type to a Finite Type
Informal description
For any types $\alpha$ and $\beta$, if $\beta$ is finite, then the type of injective function embeddings from $\alpha$ to $\beta$ is also finite.
MulEquiv.finite_left instance
{α β : Type*} [Mul α] [Mul β] [Finite α] : Finite (α ≃* β)
Full source 
@[to_additive]
instance MulEquiv.finite_left {α β : Type*} [Mul α] [Mul β] [Finite α] : Finite (α ≃* β) :=
  Finite.of_injective toEquiv toEquiv_injective
Finiteness of Multiplicative Isomorphisms from a Finite Type
Informal description
For any types $\alpha$ and $\beta$ equipped with multiplication operations, if $\alpha$ is finite, then the type of multiplicative equivalences (multiplicative isomorphisms) between $\alpha$ and $\beta$ is also finite.
MulEquiv.finite_right instance
{α β : Type*} [Mul α] [Mul β] [Finite β] : Finite (α ≃* β)
Full source 
@[to_additive]
instance MulEquiv.finite_right {α β : Type*} [Mul α] [Mul β] [Finite β] : Finite (α ≃* β) :=
  Finite.of_injective toEquiv toEquiv_injective
Finiteness of Multiplicative Isomorphisms to a Finite Type
Informal description
For any types $\alpha$ and $\beta$ equipped with multiplication operations, if $\beta$ is finite, then the type of multiplicative equivalences (multiplicative isomorphisms) between $\alpha$ and $\beta$ is also finite.
Set.fintypeProd instance
(s : Set α) (t : Set β) [Fintype s] [Fintype t] : Fintype (s ×ˢ t : Set (α × β))
Full source 
instance fintypeProd (s : Set α) (t : Set β) [Fintype s] [Fintype t] :
    Fintype (s ×ˢ t : Set (α × β)) :=
  Fintype.ofFinset (s.toFinset ×ˢ t.toFinset) <| by simp
Finiteness of Cartesian Product of Finite Sets
Informal description
For any finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, the Cartesian product $s \times t$ is also finite.
Set.fintypeOffDiag instance
[DecidableEq α] (s : Set α) [Fintype s] : Fintype s.offDiag
Full source 
instance fintypeOffDiag [DecidableEq α] (s : Set α) [Fintype s] : Fintype s.offDiag :=
  Fintype.ofFinset s.toFinset.offDiag <| by simp
Finiteness of the Off-Diagonal of a Finite Set
Informal description
For any type $\alpha$ with decidable equality and any finite set $s \subseteq \alpha$, the off-diagonal of $s$ (the set of pairs $(a, b) \in s \times s$ with $a \neq b$) is finite.
Set.fintypeImage2 instance
[DecidableEq γ] (f : α → β → γ) (s : Set α) (t : Set β) [hs : Fintype s] [ht : Fintype t] : Fintype (image2 f s t : Set γ)
Full source 
/-- `image2 f s t` is `Fintype` if `s` and `t` are. -/
instance fintypeImage2 [DecidableEq γ] (f : α → β → γ) (s : Set α) (t : Set β) [hs : Fintype s]
    [ht : Fintype t] : Fintype (image2 f s t : Set γ) := by
  rw [← image_prod]
  apply Set.fintypeImage
Finiteness of the Image of a Binary Function on Finite Sets
Informal description
For any sets $s \subseteq \alpha$ and $t \subseteq \beta$ with finite type structures, and any binary function $f : \alpha \to \beta \to \gamma$ where $\gamma$ has decidable equality, the set $\{f(a, b) \mid a \in s, b \in t\}$ is finite.
Finite.Set.finite_prod instance
(s : Set α) (t : Set β) [Finite s] [Finite t] : Finite (s ×ˢ t : Set (α × β))
Full source 
instance finite_prod (s : Set α) (t : Set β) [Finite s] [Finite t] :
    Finite (s ×ˢ t : Set (α × β)) :=
  Finite.of_equiv _ (Equiv.Set.prod s t).symm
Finiteness of Cartesian Product of Finite Sets
Informal description
For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, if $s$ and $t$ are finite, then their Cartesian product $s \timesˢ t \subseteq \alpha \times \beta$ is also finite.
Finite.Set.finite_image2 instance
(f : α → β → γ) (s : Set α) (t : Set β) [Finite s] [Finite t] : Finite (image2 f s t : Set γ)
Full source 
instance finite_image2 (f : α → β → γ) (s : Set α) (t : Set β) [Finite s] [Finite t] :
    Finite (image2 f s t : Set γ) := by
  rw [← image_prod]
  infer_instance
Finiteness of the Image of a Binary Function on Finite Sets
Informal description
For any binary function $f : \alpha \to \beta \to \gamma$ and finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, the set $\{f(a, b) \mid a \in s, b \in t\}$ is finite.
Set.Finite.prod theorem
(hs : s.Finite) (ht : t.Finite) : (s ×ˢ t : Set (α × β)).Finite
Full source 
protected theorem Finite.prod (hs : s.Finite) (ht : t.Finite) : (s ×ˢ t : Set (α × β)).Finite := by
  have := hs.to_subtype
  have := ht.to_subtype
  apply toFinite
Finiteness of Cartesian Product of Finite Sets
Informal description
For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, if $s$ and $t$ are finite, then their Cartesian product $s \times t \subseteq \alpha \times \beta$ is also finite.
Set.Finite.of_prod_left theorem
(h : (s ×ˢ t : Set (α × β)).Finite) : t.Nonempty → s.Finite
Full source 
theorem Finite.of_prod_left (h : (s ×ˢ t : Set (α × β)).Finite) : t.Nonempty → s.Finite :=
  fun ⟨b, hb⟩ => (h.image Prod.fst).subset fun a ha => ⟨(a, b), ⟨ha, hb⟩, rfl⟩
Finiteness of First Factor from Finite Product with Nonempty Second Factor
Informal description
If the Cartesian product $s \times t$ of two sets $s \subseteq \alpha$ and $t \subseteq \beta$ is finite and $t$ is nonempty, then $s$ is finite.
Set.Finite.of_prod_right theorem
(h : (s ×ˢ t : Set (α × β)).Finite) : s.Nonempty → t.Finite
Full source 
theorem Finite.of_prod_right (h : (s ×ˢ t : Set (α × β)).Finite) : s.Nonempty → t.Finite :=
  fun ⟨a, ha⟩ => (h.image Prod.snd).subset fun b hb => ⟨(a, b), ⟨ha, hb⟩, rfl⟩
Finiteness of Second Factor in Finite Cartesian Product with Nonempty First Factor
Informal description
Let $s$ and $t$ be sets in types $\alpha$ and $\beta$ respectively. If the Cartesian product $s \times t$ is finite and $s$ is nonempty, then $t$ is finite.
Set.Infinite.prod_left theorem
(hs : s.Infinite) (ht : t.Nonempty) : (s ×ˢ t).Infinite
Full source 
protected theorem Infinite.prod_left (hs : s.Infinite) (ht : t.Nonempty) : (s ×ˢ t).Infinite :=
  fun h => hs <| h.of_prod_left ht
Infinite Set Implies Infinite Product with Nonempty Set
Informal description
For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, if $s$ is infinite and $t$ is nonempty, then their Cartesian product $s \times t$ is infinite.
Set.Infinite.prod_right theorem
(ht : t.Infinite) (hs : s.Nonempty) : (s ×ˢ t).Infinite
Full source 
protected theorem Infinite.prod_right (ht : t.Infinite) (hs : s.Nonempty) : (s ×ˢ t).Infinite :=
  fun h => ht <| h.of_prod_right hs
Infinite Right Factor Implies Infinite Product for Nonempty Left Factor
Informal description
For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, if $t$ is infinite and $s$ is nonempty, then the Cartesian product $s \times t$ is infinite.
Set.infinite_prod theorem
: (s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
Full source 
protected theorem infinite_prod :
    (s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty := by
  refine ⟨fun h => ?_, ?_⟩
  · simp_rw [Set.Infinite, @and_comm ¬_, ← Classical.not_imp]
    by_contra!
    exact h ((this.1 h.nonempty.snd).prod <| this.2 h.nonempty.fst)
  · rintro (h | h)
    · exact h.1.prod_left h.2
    · exact h.1.prod_right h.2
Infinite Product Condition: $s \times t$ infinite $\iff$ ($s$ infinite and $t$ nonempty) or ($t$ infinite and $s$ nonempty)
Informal description
For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the Cartesian product $s \times t$ is infinite if and only if either $s$ is infinite and $t$ is nonempty, or $t$ is infinite and $s$ is nonempty.
Set.finite_prod theorem
: (s ×ˢ t).Finite ↔ (s.Finite ∨ t = ∅) ∧ (t.Finite ∨ s = ∅)
Full source 
theorem finite_prod : (s ×ˢ t).Finite ↔ (s.Finite ∨ t = ∅) ∧ (t.Finite ∨ s = ∅) := by
  simp only [← not_infinite, Set.infinite_prod, not_or, not_and_or, not_nonempty_iff_eq_empty]
Finite Product Condition for Sets: $s \times t$ finite $\iff$ ($s$ finite or $t$ empty) and ($t$ finite or $s$ empty)
Informal description
For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the Cartesian product $s \times t$ is finite if and only if either $s$ is finite or $t$ is empty, and either $t$ is finite or $s$ is empty.
Set.Finite.offDiag theorem
{s : Set α} (hs : s.Finite) : s.offDiag.Finite
Full source 
protected theorem Finite.offDiag {s : Set α} (hs : s.Finite) : s.offDiag.Finite :=
  (hs.prod hs).subset s.offDiag_subset_prod
Finiteness of the Off-Diagonal of a Finite Set
Informal description
For any finite set $s$ over a type $\alpha$, the off-diagonal $\{(a, b) \in s \times s \mid a \neq b\}$ is also finite.
Set.Finite.image2 theorem
(f : α → β → γ) (hs : s.Finite) (ht : t.Finite) : (image2 f s t).Finite
Full source 
protected theorem Finite.image2 (f : α → β → γ) (hs : s.Finite) (ht : t.Finite) :
    (image2 f s t).Finite := by
  have := hs.to_subtype
  have := ht.to_subtype
  apply toFinite
Finiteness of the Image of a Binary Function on Finite Sets
Informal description
For any binary function $f \colon \alpha \to \beta \to \gamma$ and finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, the image set $\{f(a, b) \mid a \in s, b \in t\}$ is finite.
Set.Finite.toFinset_prod theorem
{s : Set α} {t : Set β} (hs : s.Finite) (ht : t.Finite) : hs.toFinset ×ˢ ht.toFinset = (hs.prod ht).toFinset
Full source 
theorem Finite.toFinset_prod {s : Set α} {t : Set β} (hs : s.Finite) (ht : t.Finite) :
    hs.toFinset ×ˢ ht.toFinset = (hs.prod ht).toFinset :=
  Finset.ext <| by simp
Equality of Finset Product and Product of Finsets for Finite Sets
Informal description
For any finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, the Cartesian product of their finset representations equals the finset representation of their Cartesian product. That is, if $hs$ and $ht$ are proofs that $s$ and $t$ are finite, then $hs.\text{toFinset} \times ht.\text{toFinset} = (hs.\text{prod} ht).\text{toFinset}$.
Set.Finite.toFinset_offDiag theorem
{s : Set α} [DecidableEq α] (hs : s.Finite) : hs.offDiag.toFinset = hs.toFinset.offDiag
Full source 
theorem Finite.toFinset_offDiag {s : Set α} [DecidableEq α] (hs : s.Finite) :
    hs.offDiag.toFinset = hs.toFinset.offDiag :=
  Finset.ext <| by simp
Equality of Finset Off-Diagonal and Off-Diagonal of Finset for Finite Sets
Informal description
For any finite set $s$ in a type $\alpha$ with decidable equality, the finset representation of the off-diagonal $\{(a, b) \in s \times s \mid a \neq b\}$ is equal to the off-diagonal of the finset representation of $s$.
Set.finite_image_fst_and_snd_iff theorem
{s : Set (α × β)} : (Prod.fst '' s).Finite ∧ (Prod.snd '' s).Finite ↔ s.Finite
Full source 
theorem finite_image_fst_and_snd_iff {s : Set (α × β)} :
    (Prod.fst '' s).Finite ∧ (Prod.snd '' s).Finite(Prod.fst '' s).Finite ∧ (Prod.snd '' s).Finite ↔ s.Finite :=
  ⟨fun h => (h.1.prod h.2).subset fun _ h => ⟨mem_image_of_mem _ h, mem_image_of_mem _ h⟩,
    fun h => ⟨h.image _, h.image _⟩⟩
Finiteness of a Product Set via Projections
Informal description
For any set $s \subseteq \alpha \times \beta$, the set $s$ is finite if and only if both the projection of $s$ onto the first component $\{a \mid \exists b, (a,b) \in s\}$ and the projection of $s$ onto the second component $\{b \mid \exists a, (a,b) \in s\}$ are finite.
Set.Infinite.image2_left theorem
(hs : s.Infinite) (hb : b ∈ t) (hf : InjOn (fun a => f a b) s) : (image2 f s t).Infinite
Full source 
protected theorem Infinite.image2_left (hs : s.Infinite) (hb : b ∈ t)
    (hf : InjOn (fun a => f a b) s) : (image2 f s t).Infinite :=
  (hs.image hf).mono <| image_subset_image2_left hb
Infinite image under partial application implies infinite binary image
Informal description
Let $s$ be an infinite subset of a type $\alpha$, $t$ be a subset of a type $\beta$, and $b \in t$. If the function $a \mapsto f(a, b)$ is injective on $s$, then the image $\text{image2}(f, s, t) = \{f(a, b') \mid a \in s, b' \in t\}$ is infinite.
Set.Infinite.image2_right theorem
(ht : t.Infinite) (ha : a ∈ s) (hf : InjOn (f a) t) : (image2 f s t).Infinite
Full source 
protected theorem Infinite.image2_right (ht : t.Infinite) (ha : a ∈ s) (hf : InjOn (f a) t) :
    (image2 f s t).Infinite :=
  (ht.image hf).mono <| image_subset_image2_right ha
Infinite Image under Right Injection in Binary Function
Informal description
Let $s$ and $t$ be sets, and let $f : \alpha \to \beta \to \gamma$ be a binary function. If $t$ is infinite, there exists an element $a \in s$ such that $f(a, \cdot)$ is injective on $t$, then the image $\{f(a, b) \mid a \in s, b \in t\}$ is infinite.
Set.infinite_image2 theorem
(hfs : ∀ b ∈ t, InjOn (fun a => f a b) s) (hft : ∀ a ∈ s, InjOn (f a) t) : (image2 f s t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
Full source 
theorem infinite_image2 (hfs : ∀ b ∈ t, InjOn (fun a => f a b) s) (hft : ∀ a ∈ s, InjOn (f a) t) :
    (image2 f s t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty := by
  refine ⟨fun h => Set.infinite_prod.1 ?_, ?_⟩
  · rw [← image_uncurry_prod] at h
    exact h.of_image _
  · rintro (⟨hs, b, hb⟩ | ⟨ht, a, ha⟩)
    · exact hs.image2_left hb (hfs _ hb)
    · exact ht.image2_right ha (hft _ ha)
Infinite Binary Image Condition under Injectivity: $\text{image2}(f, s, t)$ infinite $\iff$ ($s$ infinite and $t$ nonempty) or ($t$ infinite and $s$ nonempty)
Informal description
Let $f : \alpha \to \beta \to \gamma$ be a binary function, and let $s \subseteq \alpha$ and $t \subseteq \beta$ be sets. Suppose that for every $b \in t$, the function $a \mapsto f(a, b)$ is injective on $s$, and for every $a \in s$, the function $f(a, \cdot)$ is injective on $t$. Then the image $\{f(a, b) \mid a \in s, b \in t\}$ is infinite if and only if either $s$ is infinite and $t$ is nonempty, or $t$ is infinite and $s$ is nonempty.
Set.finite_image2 theorem
(hfs : ∀ b ∈ t, InjOn (f · b) s) (hft : ∀ a ∈ s, InjOn (f a) t) : (image2 f s t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅
Full source 
lemma finite_image2 (hfs : ∀ b ∈ t, InjOn (f · b) s) (hft : ∀ a ∈ s, InjOn (f a) t) :
    (image2 f s t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅ := by
  rw [← not_infinite, infinite_image2 hfs hft]
  simp [not_or, -not_and, not_and_or, not_nonempty_iff_eq_empty]
  aesop
Finite Binary Image Condition under Injectivity: $\text{image2}(f, s, t)$ finite $\iff$ ($s$ and $t$ finite) or ($s$ or $t$ empty)
Informal description
Let $f : \alpha \to \beta \to \gamma$ be a binary function, and let $s \subseteq \alpha$ and $t \subseteq \beta$ be sets. Suppose that for every $b \in t$, the function $a \mapsto f(a, b)$ is injective on $s$, and for every $a \in s$, the function $f(a, \cdot)$ is injective on $t$. Then the image $\{f(a, b) \mid a \in s, b \in t\}$ is finite if and only if either both $s$ and $t$ are finite, or at least one of $s$ or $t$ is empty.