Instances

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

@[implicit_reducible]

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

Equations

• instFintypeSum α β = { elems := Finset.univ.disjSum Finset.univ, complete := ⋯ }

theorem Finset.toLeft_eq_univ {α : Type u_3} {β : Type u_4} [Fintype α] {u : Finset (α ⊕ β)} : u.toLeft = univ ↔ map Function.Embedding.inl univ ⊆ u

theorem Finset.toRight_eq_empty {α : Type u_3} {β : Type u_4} [Fintype α] {u : Finset (α ⊕ β)} : u.toRight = ∅ ↔ u ⊆ map Function.Embedding.inl univ

theorem Finset.toRight_eq_univ {α : Type u_3} {β : Type u_4} [Fintype β] {u : Finset (α ⊕ β)} : u.toRight = univ ↔ map Function.Embedding.inr univ ⊆ u

theorem Finset.toLeft_eq_empty {α : Type u_3} {β : Type u_4} [Fintype β] {u : Finset (α ⊕ β)} : u.toLeft = ∅ ↔ u ⊆ map Function.Embedding.inr univ

@[simp]

theorem Finset.univ_disjSum_univ {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] : univ.disjSum univ = univ

@[simp]

theorem Finset.toLeft_univ {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] : univ.toLeft = univ

@[simp]

theorem Finset.toRight_univ {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] : univ.toRight = univ

@[simp]

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

@[implicit_reducible]

def fintypeOfFintypeNe {α : Type u_1} (a : α) : 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 x✝ = Fintype.ofBijective (Sum.elim Subtype.val Subtype.val) ⋯

theorem image_subtype_ne_univ_eq_image_erase {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (k : β) (b : α → β) : Finset.image (fun (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 α] [DecidableEq β] (k : β) (b : α → β) (hk : k ∈ Finset.image b Finset.univ) (p : β → Prop) [DecidablePred p] (hp : ¬p k) : Finset.image (fun (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 α] [DecidableEq β] {t : Finset β} (hαt : Fintype.card α = t.card) {s : Finset α} {f : α → β} (hfst : image f s ⊆ t) (hfs : Set.InjOn f ↑s) : ∃ (g : α ≃ ↥t), ∀ 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} [Fintype α] {t : Finset β} (hαt : Fintype.card α = t.card) {s : Set α} {f : α → β} (hfst : MapsTo f s ↑t) (hfs : InjOn f s) : ∃ (g : α ≃ ↥t), ∀ 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 }] : card { x : α // p x ∨ q x } ≤ card { x : α // p x } + 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 }] : card { x : α // p x ∨ q x } = card { x : α // p x } + card { x : α // q x }

theorem Fintype.card_subtype_eq_or_eq_of_ne {α : Type u_3} [Fintype α] [DecidableEq α] {a b : α} (h : a ≠ b) : card { c : α // c = a ∨ c = b } = 2

@[simp]

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