instSubsingleton — Mathlib

English

If α is a subsingleton, then for every n, Sym α n is a subsingleton.

Русский

Если α — подсущностный тип, то для каждого n Sym α n является подсущностным.

LaTeX

$$$\\operatorname{Subsingleton}(\\alpha) \\Rightarrow \\forall n, \\operatorname{Subsingleton}(\\mathrm{Sym}(\\alpha,n)).$$$

Lean4

instance [Subsingleton α] (n : ℕ) : Subsingleton (Sym α n) :=
  ⟨by
    cases n
    · simp [eq_iff_true_of_subsingleton]
    · intro s s'
      obtain ⟨b, -⟩ := exists_mem s
      rw [eq_replicate_of_subsingleton b s', eq_replicate_of_subsingleton b s]⟩

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