Instances

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

ink

instance instFintypeSum (α : Type u) (β : Type v) [inst : Fintype α] [inst : Fintype β] : Fintype (α ⊕ β)

Equations

• instFintypeSum α β = { elems := Finset.disjSum Finset.univ Finset.univ, complete := (_ : ∀ (x : α ⊕ β), x ∈ Finset.disjSum Finset.univ Finset.univ) }

ink

@[simp]

theorem Finset.univ_disjSum_univ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : Fintype β] : Finset.disjSum Finset.univ Finset.univ = Finset.univ

ink

@[simp]

theorem Fintype.card_sum {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : Fintype β] : Fintype.card (α ⊕ β) = Fintype.card α + Fintype.card β

ink

def fintypeOfFintypeNe {α : Type u_1} (a : α) (h : Fintype { b // b ≠ a }) : Fintype α

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

Equations

• fintypeOfFintypeNe a h = Fintype.ofBijective (Sum.elim Subtype.val Subtype.val) (_ : Function.Bijective ↑(Equiv.sumCompl fun x => x = a))

ink

theorem image_subtype_ne_univ_eq_image_erase {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : DecidableEq β] (k : β) (b : α → β) : Finset.image (fun i => b ↑i) Finset.univ = Finset.erase (Finset.image b Finset.univ) k

ink

theorem image_subtype_univ_ssubset_image_univ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : DecidableEq β] (k : β) (b : α → β) (hk : k ∈ Finset.image b Finset.univ) (p : β → Prop) [inst : DecidablePred p] (hp : ¬p k) : Finset.image (fun i => b ↑i) Finset.univ ⊂ Finset.image b Finset.univ

ink

theorem Finset.exists_equiv_extend_of_card_eq {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : DecidableEq β] {t : Finset β} (hαt : Fintype.card α = Finset.card t) {s : Finset α} {f : α → β} (hfst : Finset.image f s ⊆ 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.

ink

theorem Set.MapsTo.exists_equiv_extend_of_card_eq {α : Type u_1} {β : Type u_2} [inst : Fintype α] {t : Finset β} (hαt : Fintype.card α = Finset.card t) {s : Set α} {f : α → β} (hfst : Set.MapsTo f s ↑t) (hfs : Set.InjOn f s) : ∃ 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.

ink

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 }

ink

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 }

ink

@[simp]

theorem infinite_sum {α : Type u_2} {β : Type u_1} : Infinite (α ⊕ β) ↔ Infinite α ∨ Infinite β