Mathlib.Data.Fintype.Fin

Fin.map_valEmbedding_univ theorem

: (Finset.univ : Finset (Fin n)).map Fin.valEmbedding = Iio n

Full source

theorem map_valEmbedding_univ : (Finset.univ : Finset (Fin n)).map Fin.valEmbedding = Iio n := by
  ext
  simp [orderIsoSubtype.symm.surjective.exists, OrderIso.symm]

Image of Universal Set under Natural Number Embedding Equals Lower Interval in $\mathbb{N}$

Informal description

For any natural number $n$, the image of the universal finite set $\mathrm{univ}$ of $\mathrm{Fin}(n)$ under the natural number embedding $\mathrm{valEmbedding} : \mathrm{Fin}(n) \hookrightarrow \mathbb{N}$ is equal to the open lower interval $Iio(n) = \{k \in \mathbb{N} \mid k < n\}$. In other words, mapping all elements of $\mathrm{Fin}(n)$ to their underlying natural number values via $\mathrm{valEmbedding}$ yields exactly the set of natural numbers less than $n$.

Fin.Ioi_zero_eq_map theorem

: Ioi (0 : Fin n.succ) = univ.map (Fin.succEmb _)

Full source

@[simp]
theorem Ioi_zero_eq_map : Ioi (0 : Fin n.succ) = univ.map (Fin.succEmb _) :=
  coe_injective <| by ext; simp [pos_iff_ne_zero]

Open Upper Interval at Zero in $\mathrm{Fin}(n+1)$ Equals Image of Universal Set under Successor Embedding

Informal description

For any natural number $n$, the open upper interval $(0, \infty)$ in $\mathrm{Fin}(n+1)$ is equal to the image of the universal finite set $\mathrm{univ}$ of $\mathrm{Fin}(n)$ under the successor embedding $\mathrm{succEmb} : \mathrm{Fin}(n) \hookrightarrow \mathrm{Fin}(n+1)$. In symbols: $$(0, \infty) = \mathrm{succEmb}(\mathrm{univ})$$

Fin.Iio_last_eq_map theorem

: Iio (Fin.last n) = Finset.univ.map Fin.castSuccEmb

Full source

@[simp]
theorem Iio_last_eq_map : Iio (Fin.last n) = Finset.univ.map Fin.castSuccEmb :=
  coe_injective <| by ext; simp [lt_def]

Open Lower Interval of Last Element in $\mathrm{Fin}(n+1)$ Equals Image of Universal Set under Successor Embedding

Informal description

For any natural number $n$, the open lower interval $Iio(\mathrm{last}(n))$ in $\mathrm{Fin}(n+1)$ (consisting of all elements less than the last element $\mathrm{last}(n)$) is equal to the image of the universal finite set $\mathrm{univ}$ of $\mathrm{Fin}(n)$ under the embedding $\mathrm{castSuccEmb} : \mathrm{Fin}(n) \hookrightarrow \mathrm{Fin}(n+1)$. In other words, the set $\{x \in \mathrm{Fin}(n+1) \mid x < \mathrm{last}(n)\}$ is exactly the image of all elements of $\mathrm{Fin}(n)$ under the successor-preserving embedding $\mathrm{castSuccEmb}$.

Fin.Ioi_succ theorem

(i : Fin n) : Ioi i.succ = (Ioi i).map (Fin.succEmb _)

Full source

theorem Ioi_succ (i : Fin n) : Ioi i.succ = (Ioi i).map (Fin.succEmb _) := by simp

Successor Mapping Preserves Open Upper Intervals in $\mathrm{Fin}(n)$

Informal description

For any element $i$ in $\mathrm{Fin}(n)$, the open upper interval $(i.\mathrm{succ}, \infty)$ in $\mathrm{Fin}(n+1)$ is equal to the image of the open upper interval $(i, \infty)$ under the successor embedding $\mathrm{succEmb} : \mathrm{Fin}(n) \hookrightarrow \mathrm{Fin}(n+1)$. In symbols: $$(i.\mathrm{succ}, \infty) = \mathrm{succEmb}\big((i, \infty)\big)$$

Fin.Iio_castSucc theorem

(i : Fin n) : Iio (castSucc i) = (Iio i).map Fin.castSuccEmb

Full source

theorem Iio_castSucc (i : Fin n) : Iio (castSucc i) = (Iio i).map Fin.castSuccEmb := by simp

Open Lower Interval Preservation under Successor Embedding in $\mathrm{Fin}(n)$

Informal description

For any element $i$ in $\mathrm{Fin}(n)$, the open lower interval $(-\infty, \mathrm{castSucc}(i))$ in $\mathrm{Fin}(n+1)$ is equal to the image of the open lower interval $(-\infty, i)$ under the embedding $\mathrm{castSuccEmb} : \mathrm{Fin}(n) \hookrightarrow \mathrm{Fin}(n+1)$. In symbols: $$(-\infty, \mathrm{castSucc}(i)) = \mathrm{castSuccEmb}\big((-\infty, i)\big)$$

Fin.card_filter_univ_succ theorem

(p : Fin (n + 1) → Prop) [DecidablePred p] : #{x | p x} = if p 0 then #{x | p (.succ x)} + 1 else #{x | p (.succ x)}

Full source

theorem card_filter_univ_succ (p : Fin (n + 1) → Prop) [DecidablePred p] :
    #{x | p x} = if p 0 then #{x | p (.succ x)} + 1 else #{x | p (.succ x)} := by
  rw [Fin.univ_succ, filter_cons, apply_ite Finset.card, card_cons, filter_map, card_map]; rfl

Cardinality of Filtered Subset of $\mathrm{Fin}(n+1)$ via Successor Function

Informal description

For any natural number $n$ and any decidable predicate $p$ on $\mathrm{Fin}(n+1)$, the cardinality of the subset $\{x \mid p(x)\}$ of $\mathrm{Fin}(n+1)$ is equal to $\#\{x \mid p(\mathrm{succ}(x))\} + 1$ if $p(0)$ holds, and $\#\{x \mid p(\mathrm{succ}(x))\}$ otherwise.

Fin.card_filter_univ_succ' theorem

(p : Fin (n + 1) → Prop) [DecidablePred p] : #{x | p x} = ite (p 0) 1 0 + #{x | p (.succ x)}

Full source

theorem card_filter_univ_succ' (p : Fin (n + 1) → Prop) [DecidablePred p] :
    #{x | p x} = ite (p 0) 1 0 + #{x | p (.succ x)}:= by
  rw [card_filter_univ_succ]; split_ifs <;> simp [add_comm]

Cardinality of Filtered Subset of $\mathrm{Fin}(n+1)$ via Successor Function (Alternative Form)

Informal description

For any natural number $n$ and any decidable predicate $p$ on $\mathrm{Fin}(n+1)$, the cardinality of the subset $\{x \mid p(x)\}$ is equal to $1 + \#\{x \mid p(\mathrm{succ}(x))\}$ if $p(0)$ holds, and $\#\{x \mid p(\mathrm{succ}(x))\}$ otherwise. Here, $\mathrm{succ}$ denotes the successor function on $\mathrm{Fin}(n+1)$ and $\#$ denotes the cardinality of a finite set.

Fin.card_filter_univ_eq_vector_get_eq_count theorem

[DecidableEq α] (a : α) (v : List.Vector α n) : #{i | v.get i = a} = v.toList.count a

Full source

theorem card_filter_univ_eq_vector_get_eq_count [DecidableEq α] (a : α) (v : List.Vector α n) :
    #{i | v.get i = a} = v.toList.count a := by
  induction' v with n x xs hxs
  · simp
  · simp_rw [card_filter_univ_succ', Vector.get_cons_zero, Vector.toList_cons, Vector.get_cons_succ,
      hxs, List.count_cons, add_comm (ite (x = a) 1 0), beq_iff_eq]

Cardinality of Matching Indices Equals List Count: $|\{i \mid v_i = a\}| = \text{count}(a, v.\text{toList})$

Informal description

For any decidable equality type $\alpha$, element $a \in \alpha$, and vector $v$ of length $n$ over $\alpha$, the cardinality of the set $\{i \in \mathrm{Fin}(n) \mid v_i = a\}$ is equal to the count of $a$ in the underlying list of $v$. In symbols: $|\{i \in \mathrm{Fin}(n) \mid v_i = a\}| = \text{count}(a, v.\text{toList})$.