Finiteness of products

instance Finite.instProd {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] : Finite (α × β)

instance Finite.instPProd {α : Sort u_3} {β : Sort u_4} [Finite α] [Finite β] : Finite (α ×' β)

theorem Finite.prod_left {α : Type u_1} (β : Type u_3) [Finite (α × β)] [Nonempty β] : Finite α

theorem Finite.prod_right {β : Type u_2} (α : Type u_3) [Finite (α × β)] [Nonempty α] : Finite β

instance Pi.finite {α : Sort u_3} {β : α → Sort u_4} [Finite α] [∀ (a : α), Finite (β a)] : Finite ((a : α) → β a)

instance Function.Embedding.finite {α : Sort u_3} {β : Sort u_4} [Finite β] : Finite (α ↪ β)

instance Equiv.finite_right {α : Sort u_3} {β : Sort u_4} [Finite β] : Finite (α ≃ β)

instance Equiv.finite_left {α : Sort u_3} {β : Sort u_4} [Finite α] : Finite (α ≃ β)

instance MulEquiv.finite_left {α : Type u_3} {β : Type u_4} [Mul α] [Mul β] [Finite α] : Finite (α ≃* β)

instance AddEquiv.finite_left {α : Type u_3} {β : Type u_4} [Add α] [Add β] [Finite α] : Finite (α ≃+ β)

instance MulEquiv.finite_right {α : Type u_3} {β : Type u_4} [Mul α] [Mul β] [Finite β] : Finite (α ≃* β)

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.

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) ⋯

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

Equations

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

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.

instance Finite.Set.finite_prod {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) [Finite ↑s] [Finite ↑t] : Finite ↑(s ×ˢ t)

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.

theorem Set.Finite.prod {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (hs : s.Finite) (ht : t.Finite) : (s ×ˢ t).Finite

theorem Set.Finite.of_prod_left {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (h : (s ×ˢ t).Finite) : t.Nonempty → s.Finite

theorem Set.Finite.of_prod_right {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (h : (s ×ˢ t).Finite) : s.Nonempty → t.Finite

theorem Set.Infinite.prod_left {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (hs : s.Infinite) (ht : t.Nonempty) : (s ×ˢ t).Infinite

theorem Set.Infinite.prod_right {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (ht : t.Infinite) (hs : s.Nonempty) : (s ×ˢ t).Infinite

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

theorem Set.finite_prod {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : (s ×ˢ t).Finite ↔ (s.Finite ∨ t = ∅) ∧ (t.Finite ∨ s = ∅)

theorem Set.Finite.offDiag {α : Type u_1} {s : Set α} (hs : s.Finite) : s.offDiag.Finite

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

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

theorem Set.Finite.toFinset_offDiag {α : Type u_1} {s : Set α} [DecidableEq α] (hs : s.Finite) : ⋯.toFinset = hs.toFinset.offDiag

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

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

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

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

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 = ∅