Mathlib.Data.Fintype.Sum

instFintypeSum instance

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

Full source

instance (α : Type u) (β : Type v) [Fintype α] [Fintype β] : Fintype (α ⊕ β) where
  elems := univ.disjSum univ
  complete := by rintro (_ | _) <;> simp

Finite Sum of Finite Types is Finite

Informal description

For any finite types $\alpha$ and $\beta$, the sum type $\alpha \oplus \beta$ is also finite.

Finset.toLeft_eq_univ theorem

: u.toLeft = univ ↔ univ.map .inl ⊆ u

Full source

lemma toLeft_eq_univ : u.toLeft = univ ↔ univ.map .inl ⊆ u := by
  simp [map_inl_subset_iff_subset_toLeft]

Left Projection Equals Universal Finset iff Left Injection Image is Contained

Informal description

For a finite type $\alpha \oplus \beta$ and a subset $u$ of its universal finset, the left projection of $u$ equals the universal finset of $\alpha$ if and only if the image of the universal finset of $\alpha$ under the left injection is contained in $u$. In other words, $u.\text{toLeft} = \text{univ} \leftrightarrow \text{univ.map } \text{inl} \subseteq u$.

Finset.toRight_eq_empty theorem

: u.toRight = ∅ ↔ u ⊆ univ.map .inl

Full source

lemma toRight_eq_empty : u.toRight = ∅ ↔ u ⊆ univ.map .inl := by simp [subset_map_inl]

Right Projection of Subset is Empty iff Subset is Left Injection Image

Informal description

For a finite type $\alpha \oplus \beta$ and a subset $u$ of its universal finset, the right projection of $u$ is empty if and only if $u$ is contained in the image of the universal finset of $\alpha$ under the left injection. In other words, $u.\text{toRight} = \emptyset \leftrightarrow u \subseteq \text{univ.map } \text{inl}$.

Finset.toRight_eq_univ theorem

: u.toRight = univ ↔ univ.map .inr ⊆ u

Full source

lemma toRight_eq_univ : u.toRight = univ ↔ univ.map .inr ⊆ u := by
  simp [map_inr_subset_iff_subset_toRight]

Right Projection Equals Universal Finset iff Right Injection Image is Contained

Informal description

For a finite type $\alpha \oplus \beta$ and a subset $u$ of its universal finset, the right projection of $u$ equals the universal finset of $\beta$ if and only if the image of the universal finset of $\beta$ under the right injection is contained in $u$. In other words, $u.\text{toRight} = \text{univ} \leftrightarrow \text{univ.map } \text{inr} \subseteq u$.

Finset.toLeft_eq_empty theorem

: u.toLeft = ∅ ↔ u ⊆ univ.map .inr

Full source

lemma toLeft_eq_empty : u.toLeft = ∅ ↔ u ⊆ univ.map .inr := by simp [subset_map_inr]

Left Projection of Subset is Empty iff Subset is Right Injection Image

Informal description

For a finite type $\alpha \oplus \beta$ and a subset $u$ of its universal finset, the left projection of $u$ is empty if and only if $u$ is contained in the image of the universal finset of $\beta$ under the right injection. In other words, $u.\text{toLeft} = \emptyset \leftrightarrow u \subseteq \text{univ.map } \text{inr}$.

Finset.univ_disjSum_univ theorem

: univ.disjSum univ = (univ : Finset (α ⊕ β))

Full source

@[simp] lemma univ_disjSum_univ : univ.disjSum univ = (univ : Finset (α ⊕ β)) := rfl

Universal Finset of Sum Type as Disjoint Union

Informal description

For finite types $\alpha$ and $\beta$, the disjoint union of the universal finsets of $\alpha$ and $\beta$ equals the universal finset of the sum type $\alpha \oplus \beta$. That is, $\text{univ.disjSum univ} = \text{univ} : \text{Finset} (\alpha \oplus \beta)$.

Finset.toLeft_univ theorem

: (univ : Finset (α ⊕ β)).toLeft = univ

Full source

@[simp] lemma toLeft_univ : (univ : Finset (α ⊕ β)).toLeft = univ := by ext; simp

Left Projection of Universal Finset for Sum Type

Informal description

For any finite types $\alpha$ and $\beta$, the left projection of the universal finset of the sum type $\alpha \oplus \beta$ equals the universal finset of $\alpha$. That is, $\text{toLeft}(\text{univ}_{\alpha \oplus \beta}) = \text{univ}_\alpha$.

Finset.toRight_univ theorem

: (univ : Finset (α ⊕ β)).toRight = univ

Full source

@[simp] lemma toRight_univ : (univ : Finset (α ⊕ β)).toRight = univ := by ext; simp

Right Projection of Universal Finset for Sum Type

Informal description

For any finite types $\alpha$ and $\beta$, the right projection of the universal finset of the sum type $\alpha \oplus \beta$ equals the universal finset of $\beta$. That is, $\text{toRight}(\text{univ}_{\alpha \oplus \beta}) = \text{univ}_\beta$.

Fintype.card_sum theorem

[Fintype α] [Fintype β] : Fintype.card (α ⊕ β) = Fintype.card α + Fintype.card β

Full source

@[simp]
theorem Fintype.card_sum [Fintype α] [Fintype β] :
    Fintype.card (α ⊕ β) = Fintype.card α + Fintype.card β :=
  card_disjSum _ _

Cardinality of Sum of Finite Types

Informal description

For any finite types $\alpha$ and $\beta$, the cardinality of the sum type $\alpha \oplus \beta$ is equal to the sum of the cardinalities of $\alpha$ and $\beta$, i.e., $|\alpha \oplus \beta| = |\alpha| + |\beta|$.

fintypeOfFintypeNe definition

(a : α) (_ : Fintype { b // b ≠ a }) : Fintype α

Full source

/-- If the subtype of all-but-one elements is a `Fintype` then the type itself is a `Fintype`. -/
def fintypeOfFintypeNe (a : α) (_ : Fintype { b // b ≠ a }) : Fintype α :=
  Fintype.ofBijective (Sum.elim ((↑) : { b // b = a } → α) ((↑) : { b // b ≠ a } → α)) <| by
    classical exact (Equiv.sumCompl (· = a)).bijective

Finiteness of a type via finiteness of its complement to a singleton

Informal description

Given an element $a$ of type $\alpha$ and a proof that the subtype $\{b \mid b \neq a\}$ is finite, then the type $\alpha$ itself is finite. The finiteness is established by constructing a bijection between $\alpha$ and the sum of the singleton subtype $\{b \mid b = a\}$ and the given finite subtype $\{b \mid b \neq a\}$.

image_subtype_ne_univ_eq_image_erase theorem

 [Fintype α] [DecidableEq β] (k : β) (b : α → β) :
  image (fun i : { a // b a ≠ k } => b ↑i) univ = (image b univ).erase k

Full source

theorem image_subtype_ne_univ_eq_image_erase [Fintype α] [DecidableEq β] (k : β) (b : α → β) :
    image (fun i : { a // b a ≠ k } => b ↑i) univ = (image b univ).erase k := by
  apply subset_antisymm
  · rw [image_subset_iff]
    intro i _
    apply mem_erase_of_ne_of_mem i.2 (mem_image_of_mem _ (mem_univ _))
  · intro i hi
    rw [mem_image]
    rcases mem_image.1 (erase_subset _ _ hi) with ⟨a, _, ha⟩
    subst ha
    exact ⟨⟨a, ne_of_mem_erase hi⟩, mem_univ _, rfl⟩

Image of Complement Subtype Equals Erased Image

Informal description

Let $\alpha$ be a finite type and $\beta$ a type with decidable equality. For any element $k \in \beta$ and function $b : \alpha \to \beta$, the image of the restriction of $b$ to the subtype $\{a \mid b(a) \neq k\}$ under the universal finite set of $\alpha$ is equal to the image of $b$ under the universal finite set of $\alpha$ with $k$ removed. In symbols: $$ \text{image } \left( \lambda (i : \{a \mid b(a) \neq k\}), b(i) \right) \text{ univ} = (\text{image } b \text{ univ}).\text{erase } k. $$

image_subtype_univ_ssubset_image_univ theorem

 [Fintype α] [DecidableEq β] (k : β) (b : α → β) (hk : k ∈ Finset.image b univ) (p : β → Prop) [DecidablePred p]
  (hp : ¬p k) : image (fun i : { a // p (b a) } => b ↑i) univ ⊂ image b univ

Full source

theorem image_subtype_univ_ssubset_image_univ [Fintype α] [DecidableEq β] (k : β) (b : α → β)
    (hk : k ∈ Finset.image b univ) (p : β → Prop) [DecidablePred p] (hp : ¬p k) :
    imageimage (fun i : { a // p (b a) } => b ↑i) univ ⊂ image b univ := by
  constructor
  · intro x hx
    rcases mem_image.1 hx with ⟨y, _, hy⟩
    exact hy ▸ mem_image_of_mem b (mem_univ (y : α))
  · intro h
    rw [mem_image] at hk
    rcases hk with ⟨k', _, hk'⟩
    subst hk'
    have := h (mem_image_of_mem b (mem_univ k'))
    rw [mem_image] at this
    rcases this with ⟨j, _, hj'⟩
    exact hp (hj' ▸ j.2)

Strict Subset Property for Images of Predicate-Restricted Subtypes

Informal description

Let $\alpha$ be a finite type and $\beta$ a type with decidable equality. Given an element $k \in \beta$, a function $b : \alpha \to \beta$ such that $k$ is in the image of $b$ over the universal finite set of $\alpha$, and a decidable predicate $p : \beta \to \mathrm{Prop}$ such that $\neg p(k)$, then the image of the restriction of $b$ to the subtype $\{a \mid p(b(a))\}$ is a strict subset of the image of $b$ over the universal finite set of $\alpha$. In symbols: $$ \text{image } \left( \lambda (i : \{a \mid p(b(a))\}), b(i) \right) \text{ univ} \subset \text{image } b \text{ univ}. $$

Finset.exists_equiv_extend_of_card_eq theorem

 [Fintype α] [DecidableEq β] {t : Finset β} (hαt : Fintype.card α = #t) {s : Finset α} {f : α → β}
  (hfst : Finset.image f s ⊆ t) (hfs : Set.InjOn f s) : ∃ g : α ≃ t, ∀ i ∈ s, (g i : β) = f i

Full source

/-- 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 Finset.exists_equiv_extend_of_card_eq [Fintype α] [DecidableEq β] {t : Finset β}
    (hαt : Fintype.card α = #t) {s : Finset α} {f : α → β} (hfst : Finset.imageFinset.image f s ⊆ t)
    (hfs : Set.InjOn f s) : ∃ g : α ≃ t, ∀ i ∈ s, (g i : β) = f i := by
  classical
    induction' s using Finset.induction with a s has H generalizing f
    · obtain ⟨e⟩ : Nonempty (α ≃ ↥t) := by rwa [← Fintype.card_eq, Fintype.card_coe]
      use e
      simp
    have hfst' : Finset.imageFinset.image f s ⊆ t := (Finset.image_mono _ (s.subset_insert a)).trans hfst
    have hfs' : Set.InjOn f s := hfs.mono (s.subset_insert a)
    obtain ⟨g', hg'⟩ := H hfst' hfs'
    have hfat : f a ∈ t := hfst (mem_image_of_mem _ (s.mem_insert_self a))
    use g'.trans (Equiv.swap (⟨f a, hfat⟩ : t) (g' a))
    simp_rw [mem_insert]
    rintro i (rfl | hi)
    · simp
    rw [Equiv.trans_apply, Equiv.swap_apply_of_ne_of_ne, hg' _ hi]
    · exact
        ne_of_apply_ne Subtype.val
          (ne_of_eq_of_ne (hg' _ hi) <|
            hfs.ne (subset_insert _ _ hi) (mem_insert_self _ _) <| ne_of_mem_of_not_mem hi has)
    · exact g'.injective.ne (ne_of_mem_of_not_mem hi has)

Extension of Injective Function on Finite Subset to Bijection on Equicardinal Sets

Informal description

Let $\alpha$ be a finite type and $\beta$ a type with decidable equality. Given a finite set $t \subseteq \beta$ with the same cardinality as $\alpha$, a finite subset $s \subseteq \alpha$, and an injective function $f \colon s \to \beta$ whose image is contained in $t$, there exists a bijection $g \colon \alpha \simeq t$ that extends $f$, i.e., $g(i) = f(i)$ for all $i \in s$.

Set.MapsTo.exists_equiv_extend_of_card_eq theorem

 [Fintype α] {t : Finset β} (hαt : Fintype.card α = #t) {s : Set α} {f : α → β} (hfst : s.MapsTo f t)
  (hfs : Set.InjOn f s) : ∃ g : α ≃ t, ∀ i ∈ s, (g i : β) = f i

Full source

/-- 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 Set.MapsTo.exists_equiv_extend_of_card_eq [Fintype α] {t : Finset β}
    (hαt : Fintype.card α = #t) {s : Set α} {f : α → β} (hfst : s.MapsTo f t)
    (hfs : Set.InjOn f s) : ∃ g : α ≃ t, ∀ i ∈ s, (g i : β) = f i := by
  classical
    let s' : Finset α := s.toFinset
    have hfst' : s'.image f ⊆ t := by simpa [s', ← Finset.coe_subset] using hfst
    have hfs' : Set.InjOn f s' := by simpa [s'] using hfs
    obtain ⟨g, hg⟩ := Finset.exists_equiv_extend_of_card_eq hαt hfst' hfs'
    refine ⟨g, fun i hi => ?_⟩
    apply hg
    simpa [s'] using hi

Extension of Injective Function on Subset to Bijection on Equicardinal Sets

Informal description

Let $\alpha$ be a finite type and $\beta$ a type with decidable equality. Given a finite set $t \subseteq \beta$ with the same cardinality as $\alpha$, a subset $s \subseteq \alpha$, and a function $f \colon \alpha \to \beta$ such that $f$ maps $s$ into $t$ and is injective on $s$, there exists a bijection $g \colon \alpha \simeq t$ that extends $f$ on $s$, i.e., $g(i) = f(i)$ for all $i \in s$.

Fintype.card_subtype_or theorem

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

Full source

theorem Fintype.card_subtype_or (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 } := by
  classical
    convert Fintype.card_le_of_embedding (subtypeOrLeftEmbedding p q)
    rw [Fintype.card_sum]

Cardinality Bound for Disjunctive Subtype: $|\{x \mid p x \lor q x\}| \leq |\{x \mid p x\}| + |\{x \mid q x\}|$

Informal description

For any type $\alpha$ and predicates $p, q : \alpha \to \mathrm{Prop}$, if the subtypes $\{x \mid p x\}$ and $\{x \mid q x\}$ are finite, then the cardinality of the subtype $\{x \mid p x \lor q x\}$ is less than or equal to the sum of the cardinalities of $\{x \mid p x\}$ and $\{x \mid q x\}$, i.e., $$|\{x \mid p x \lor q x\}| \leq |\{x \mid p x\}| + |\{x \mid q x\}|.$$

Fintype.card_subtype_or_disjoint theorem

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

Full source

theorem Fintype.card_subtype_or_disjoint (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 } := by
  classical
    convert Fintype.card_congr (subtypeOrEquiv p q h)
    simp

Cardinality of Disjunctive Subtype for Disjoint Predicates: $|\{x \mid p x \lor q x\}| = |\{x \mid p x\}| + |\{x \mid q x\}|$

Informal description

For any type $\alpha$ and disjoint predicates $p, q : \alpha \to \mathrm{Prop}$ (i.e., no element satisfies both $p$ and $q$), if the subtypes $\{x \mid p x\}$ and $\{x \mid q x\}$ are finite, then the cardinality of the subtype $\{x \mid p x \lor q x\}$ is equal to the sum of the cardinalities of $\{x \mid p x\}$ and $\{x \mid q x\}$, i.e., $$|\{x \mid p x \lor q x\}| = |\{x \mid p x\}| + |\{x \mid q x\}|.$$

infinite_sum theorem

: Infinite (α ⊕ β) ↔ Infinite α ∨ Infinite β

Full source

@[simp]
theorem infinite_sum : InfiniteInfinite (α ⊕ β) ↔ Infinite α ∨ Infinite β := by
  refine ⟨fun H => ?_, fun H => H.elim (@Sum.infinite_of_left α β) (@Sum.infinite_of_right α β)⟩
  contrapose! H; haveI := fintypeOfNotInfinite H.1; haveI := fintypeOfNotInfinite H.2
  exact Infinite.false

Sum Type is Infinite if and only if One Component is Infinite

Informal description

For any types $\alpha$ and $\beta$, the sum type $\alpha \oplus \beta$ is infinite if and only if at least one of $\alpha$ or $\beta$ is infinite.