toFinset_replicate_of_ne_zero

Mathlib.Data.Finset.Insert

URI: https://scilib.ai/kg/mathlib#List.toFinset_replicate_of_ne_zero

English

If n ≠ 0, then the toFinset of List.replicate n a equals the singleton {a}.

Русский

Если n ≠ 0, то toFinset списока List.replicate n a равно {a}.

LaTeX

$$$\\operatorname{toFinset}(\\operatorname{List.replicate} \\ n\\ a) = \\{a\\}$, for $n \\neq 0$.$$

Lean4

theorem toFinset_replicate_of_ne_zero {n : ℕ} (hn : n ≠ 0) : (List.replicate n a).toFinset = { a } :=
  by
  ext x
  simp [hn, List.mem_replicate]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru