mathlib3 documentation

data.fintype.sum

Instances #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[protected, instance]
def sum.fintype (α : Type u) (β : Type v) [fintype α] [fintype β] :
fintype β)
Equations
@[simp]
theorem fintype.card_sum {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] :
def fintype_of_fintype_ne {α : 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} [fintype α] [decidable_eq β] (k : β) (b : α β) :
finset.image (λ (i : {a // b a k}), b i) finset.univ = (finset.image b finset.univ).erase k
theorem image_subtype_univ_ssubset_image_univ {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (k : β) (b : α β) (hk : k finset.image b finset.univ) (p : β Prop) [decidable_pred p] (hp : ¬p k) :
finset.image (λ (i : {a // p (b a)}), b i) finset.univ finset.image b finset.univ
theorem finset.exists_equiv_extend_of_card_eq {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {t : finset β} (hαt : fintype.card α = t.card) {s : finset α} {f : α β} (hfst : finset.image f s t) (hfs : set.inj_on f s) :
(g : α t), (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.maps_to.exists_equiv_extend_of_card_eq {α : Type u_1} {β : Type u_2} [fintype α] {t : finset β} (hαt : fintype.card α = t.card) {s : set α} {f : α β} (hfst : set.maps_to f s t) (hfs : set.inj_on f s) :
(g : α t), (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 q : α Prop) [fintype {x // p x}] [fintype {x // q x}] [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 q : α Prop) (h : disjoint p q) [fintype {x // p x}] [fintype {x // q x}] [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_1} {β : Type u_2} :