# Finiteness of products #

source
instance Finite.instProd {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] :
Finite (α × β)
source
instance Finite.instPProd {α : Sort u_3} {β : Sort u_4} [Finite α] [Finite β] :
Finite (α ×' β)
source
theorem Finite.prod_left {α : Type u_1} (β : Type u_3) [Finite (α × β)] [Nonempty β] :
Finite α
source
theorem Finite.prod_right {β : Type u_2} (α : Type u_3) [Finite (α × β)] [Nonempty α] :
Finite β
source
theorem Prod.finite_iff {α : Type u_1} {β : Type u_2} [Nonempty α] [Nonempty β] :
Finite (α × β) ↔ Finite α ∧ Finite β
source
instance Pi.finite {α : Sort u_3} {β : α → Sort u_4} [Finite α] [∀ (a : α), Finite (β a)] :
Finite ((a : α) → β a)
source
instance Function.Embedding.finite {α : Sort u_3} {β : Sort u_4} [Finite β] :
Finite (α ↪ β)
source
instance Equiv.finite_right {α : Sort u_3} {β : Sort u_4} [Finite β] :
Finite (α ≃ β)
source
instance Equiv.finite_left {α : Sort u_3} {β : Sort u_4} [Finite α] :
Finite (α ≃ β)
source
instance MulEquiv.finite_left {α : Type u_3} {β : Type u_4} [Mul α] [Mul β] [Finite α] :
Finite (α ≃* β)
source
instance AddEquiv.finite_left {α : Type u_3} {β : Type u_4} [Add α] [Add β] [Finite α] :
Finite (α ≃+ β)
source
instance MulEquiv.finite_right {α : Type u_3} {β : Type u_4} [Mul α] [Mul β] [Finite β] :
Finite (α ≃* β)
source
instance AddEquiv.finite_right {α : Type u_3} {β : Type u_4} [Add α] [Add β] [Finite β] :
Finite (α ≃+ β)

### Fintype instances #

Every instance here should have a corresponding `Set.Finite` constructor in the next section.

source
instance Set.fintypeProd {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) [Fintype ↑s] [Fintype ↑t] :
Fintype ↑(s ×ˢ t)
Equations

- s.fintypeProd t = Fintype.ofFinset (s.toFinset ×ˢ t.toFinset) ⋯

source
instance Set.fintypeOffDiag {α : Type u_1} [DecidableEq α] (s : Set α) [Fintype ↑s] :
Fintype ↑s.offDiag
Equations

- s.fintypeOffDiag = Fintype.ofFinset s.toFinset.offDiag ⋯

source
instance Set.fintypeImage2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq γ] (f : α → β → γ) (s : Set α) (t : Set β) [hs : Fintype ↑s] [ht : Fintype ↑t] :
Fintype ↑(image2 f s t)

`image2 f s t` is `Fintype` if `s` and `t` are.

Equations

- Set.fintypeImage2 f s t = ⋯.mpr ((s ×ˢ t).fintypeImage fun (x : α × β) => f x.1 x.2)

### 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.

source
instance Finite.Set.finite_prod {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) [Finite ↑s] [Finite ↑t] :
Finite ↑(s ×ˢ t)
source
instance Finite.Set.finite_image2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (s : Set α) (t : Set β) [Finite ↑s] [Finite ↑t] :
Finite ↑(Set.image2 f s t)

### 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.

source
theorem Set.Finite.prod {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (hs : s.Finite) (ht : t.Finite) :
(s ×ˢ t).Finite
source
theorem Set.Finite.of_prod_left {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (h : (s ×ˢ t).Finite) :
t.Nonempty → s.Finite
source
theorem Set.Finite.of_prod_right {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (h : (s ×ˢ t).Finite) :
s.Nonempty → t.Finite
source
theorem Set.Infinite.prod_left {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (hs : s.Infinite) (ht : t.Nonempty) :
(s ×ˢ t).Infinite
source
theorem Set.Infinite.prod_right {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (ht : t.Infinite) (hs : s.Nonempty) :
(s ×ˢ t).Infinite
source
theorem Set.infinite_prod {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} :
(s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
source
theorem Set.finite_prod {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} :
(s ×ˢ t).Finite ↔ (s.Finite ∨ t = ∅) ∧ (t.Finite ∨ s = ∅)
source
theorem Set.Finite.offDiag {α : Type u_1} {s : Set α} (hs : s.Finite) :
s.offDiag.Finite
source
theorem Set.Finite.image2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} (f : α → β → γ) (hs : s.Finite) (ht : t.Finite) :
(image2 f s t).Finite

### Properties #

source
theorem Set.Finite.toFinset_prod {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (hs : s.Finite) (ht : t.Finite) :
hs.toFinset ×ˢ ht.toFinset = ⋯.toFinset
source
theorem Set.Finite.toFinset_offDiag {α : Type u_1} {s : Set α} [DecidableEq α] (hs : s.Finite) :
⋯.toFinset = hs.toFinset.offDiag
source
theorem Set.finite_image_fst_and_snd_iff {α : Type u_1} {β : Type u_2} {s : Set (α × β)} :
(Prod.fst '' s).Finite ∧ (Prod.snd '' s).Finite ↔ s.Finite

### Infinite sets #

source
theorem Set.Infinite.image2_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : Set α} {t : Set β} {b : β} (hs : s.Infinite) (hb : b ∈ t) (hf : InjOn (fun (a : α) => f a b) s) :
(image2 f s t).Infinite
source
theorem Set.Infinite.image2_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : Set α} {t : Set β} {a : α} (ht : t.Infinite) (ha : a ∈ s) (hf : InjOn (f a) t) :
(image2 f s t).Infinite
source
theorem Set.infinite_image2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : Set α} {t : Set β} (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
source
theorem Set.finite_image2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : Set α} {t : Set β} (hfs : ∀ b ∈ t, InjOn (fun (x : α) => f x b) s) (hft : ∀ a ∈ s, InjOn (f a) t) :
(image2 f s t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅