replicate_subset_singleton

Mathlib.Data.List.Basic

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

English

For any n and a, replicate(n, a) is contained in the singleton list [a].

Русский

Для любого n и a множество replicate(n, a) содержится в одиночном списке [a].

LaTeX

$$$$\\forall a:\\\\alpha,\\\\forall n:\\\\mathbb{N},\\\\ replicate(n, a) \\\\subseteq [a].$$$$

Lean4

theorem replicate_subset_singleton (n) (a : α) : replicate n a ⊆ [a] := fun _ h =>
  mem_singleton.2 (eq_of_mem_replicate h)

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

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

Разделы

Аффилиация

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