eq_replicate_of_subsingleton — Mathlib

English

If α is a subsingleton, then for every a ∈ α and every n ∈ ℕ, every s ∈ Sym α n satisfies s = replicate n a.

Русский

Пусть α является подсущностным типом. Тогда для любого элемента a ∈ α и любого n ∈ ℕ любой s ∈ Sym α n равен replicate n a.

LaTeX

$$$\\operatorname{Subsingleton}(\\alpha) \\Rightarrow \\forall a : \\alpha, \\forall n \\in \\mathbb{N}, \\forall s \\in \\mathrm{Sym}(\\alpha,n), s = \\mathrm{replicate}(n,a).$$$

Lean4

theorem eq_replicate_of_subsingleton [Subsingleton α] (a : α) {n : ℕ} (s : Sym α n) : s = replicate n a :=
  eq_replicate.2 fun _ _ => Subsingleton.elim _ _

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