Finiteness of sets of lists

Tags

finite sets

theorem List.finite_length_eq (α : Type u_1) [Finite α] (n : ℕ) : {l : List α | l.length = n}.Finite

theorem List.finite_length_lt (α : Type u_1) [Finite α] (n : ℕ) : {l : List α | l.length < n}.Finite

theorem List.finite_length_le (α : Type u_1) [Finite α] (n : ℕ) : {l : List α | l.length ≤ n}.Finite