keys_append

Mathlib.Data.List.Sigma

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

English

The keys of the concatenation of two lists equal the concatenation of their keys.

Русский

Ключи конкатенации двух списков равны конкатенации их ключей.

LaTeX

$$$ (l_1 \\; ++ \\; l_2).keys = l_1.keys ++ l_2.keys. $$$

Lean4

@[simp, grind =]
theorem keys_append : (l₁ ++ l₂).keys = l₁.keys ++ l₂.keys := by simp [keys]

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

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

Разделы

Аффилиация

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