Documentation

Mathlib.Data.Fintype.Sum

Instances #

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

instance instFintypeSum (α : Type u) (β : Type v) [Fintype α] [Fintype β] :
Fintype (α β)
Equations
    theorem Finset.toLeft_eq_univ {α : Type u_3} {β : Type u_4} [Fintype α] {u : Finset (α β)} :
    theorem Finset.toRight_eq_empty {α : Type u_3} {β : Type u_4} [Fintype α] {u : Finset (α β)} :
    theorem Finset.toRight_eq_univ {α : Type u_3} {β : Type u_4} [Fintype β] {u : Finset (α β)} :
    theorem Finset.toLeft_eq_empty {α : Type u_3} {β : Type u_4} [Fintype β] {u : Finset (α β)} :
    @[simp]
    theorem Finset.univ_disjSum_univ {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] :
    @[simp]
    theorem Finset.toLeft_univ {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] :
    @[simp]
    theorem Finset.toRight_univ {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] :
    @[simp]
    theorem Fintype.card_sum {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] :
    card (α β) = card α + card β
    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
      Instances For
        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 : α { x : β // x t }), is, (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 : α { x : β // x t }), is, (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 }
        @[simp]
        theorem infinite_sum {α : Type u_1} {β : Type u_2} :