exists_univ_list — Mathlib

English

For any finite α, there exists a list listing all elements of α without repetition.

Русский

Для любого конечного типа α существует список без повторений, содержащий все элементы α.

LaTeX

$$$ \exists l : \mathrm{List}(\alpha), l.\mathrm{Nodup} \land \forall x : \alpha, x \in l $$$

Lean4

theorem exists_univ_list (α) [Finite α] : ∃ l : List α, l.Nodup ∧ ∀ x : α, x ∈ l :=
  by
  cases nonempty_fintype α
  obtain ⟨l, e⟩ := Quotient.exists_rep (@univ α _).1
  have := And.intro (@univ α _).2 (@mem_univ_val α _)
  exact ⟨_, by rwa [← e] at this⟩

Похожие утверждения