toFinset_replicate — Mathlib

English

Replicating an element n times and then coercing to a finset yields the empty finset if n = 0, and the singleton {a} if n > 0.

Русский

Повторение элемента n раз и приведение к Finset даёт пустой финсет, если n = 0, и синглтон {a}, если n > 0.

LaTeX

$$$\\\\big(\\\\mathrm{Multiset.replicate} n a\\\\big).toFinset = \\\\begin{cases} \\\\emptyset, & n = 0 \\\\cr \\\\{a\\\\}, & n > 0 \\\\end{cases}$$$

Lean4

@[simp]
theorem toFinset_replicate (n : ℕ) (a : α) : (replicate n a).toFinset = if n = 0 then ∅ else { a } :=
  by
  ext x
  simp only [mem_toFinset, mem_replicate]
  split_ifs with hn <;> simp [hn]

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