Finiteness of bounded-length lists #
Over a finite alphabet, the lists of length at most n form a finite type — the state
space of window-based transducers.
@[implicit_reducible]
noncomputable instance
List.fintypeSubtypeLengthLE
{α : Type u_1}
[Fintype α]
(n : ℕ)
:
Fintype { l : List α // l.length ≤ n }
The "lists of length at most n" subtype is finite when α is: it is a surjective
image of Σ m : Fin (n + 1), List.Vector α m. Uses classical for the DecidableEq
side condition rather than imposing it on consumers.
Equations
- List.fintypeSubtypeLengthLE n = Fintype.ofSurjective (fun (s : (m : Fin (n + 1)) × List.Vector α ↑m) => ⟨s.snd.toList, ⋯⟩) ⋯