data.fintype.sum - mathlib3 docs

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 β] :

Equations

@[simp]

theorem finset.univ_disj_sum_univ {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] :

@[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 : α → β) :

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

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}] :

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} :