# Documentation

Mathlib.Data.Fintype.Sum

## Instances #

We provide the Fintype instance for the sum of two fintypes.

instance instFintypeSum (α : Type u) (β : Type v) [inst : ] [inst : ] :
Fintype (α β)
Equations
@[simp]
theorem Finset.univ_disjSum_univ {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
Finset.disjSum Finset.univ Finset.univ = Finset.univ
@[simp]
theorem Fintype.card_sum {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
Fintype.card (α β) =
def fintypeOfFintypeNe {α : Type u_1} (a : α) (h : Fintype { b // b a }) :

If the subtype of all-but-one elements is a Fintype then the type itself is a Fintype.

Equations
theorem image_subtype_ne_univ_eq_image_erase {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (k : β) (b : αβ) :
Finset.image (fun i => b i) Finset.univ = Finset.erase (Finset.image b Finset.univ) k
theorem image_subtype_univ_ssubset_image_univ {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (k : β) (b : αβ) (hk : k Finset.image b Finset.univ) (p : βProp) [inst : ] (hp : ¬p k) :
Finset.image (fun i => b i) Finset.univ Finset.image b Finset.univ
theorem Finset.exists_equiv_extend_of_card_eq {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {t : } (hαt : ) {s : } {f : αβ} (hfst : t) (hfs : Set.InjOn f s) :
g, ∀ (i : α), i s↑(g i) = f i

Any injection from a finset s in a fintype α to a finset t of the same cardinality as α can be extended to a bijection between α and t.

theorem Set.MapsTo.exists_equiv_extend_of_card_eq {α : Type u_1} {β : Type u_2} [inst : ] {t : } (hαt : ) {s : Set α} {f : αβ} (hfst : Set.MapsTo f s t) (hfs : ) :
g, ∀ (i : α), i s↑(g i) = f i

Any injection from a set s in a fintype α to a finset t of the same cardinality as α can be extended to a bijection between α and t.

theorem Fintype.card_subtype_or {α : Type u_1} (p : αProp) (q : αProp) [inst : Fintype { x // p x }] [inst : Fintype { x // q x }] [inst : Fintype { x // p x q x }] :
Fintype.card { x // p x q x } Fintype.card { x // p x } + Fintype.card { x // q x }
theorem Fintype.card_subtype_or_disjoint {α : Type u_1} (p : αProp) (q : αProp) (h : Disjoint p q) [inst : Fintype { x // p x }] [inst : Fintype { x // q x }] [inst : Fintype { x // p x q x }] :
Fintype.card { x // p x q x } = Fintype.card { x // p x } + Fintype.card { x // q x }
@[simp]
theorem infinite_sum {α : Type u_2} {β : Type u_1} :
Infinite (α β)