keys_erase

Mathlib.Data.Finmap

URI: https://scilib.ai/kg/mathlib#Finmap.keys_erase

English

Erasing a key a from s reduces the keys by removing a: (erase a s).keys = (s.keys).erase a.

Русский

Удаление ключа a из s сокращает множество ключей на удаление a: (erase a s).keys = (s.keys).erase a.

LaTeX

$$$ (erase\ a\ s).keys = (s.keys).erase a $$$

Lean4

@[simp]
theorem keys_erase (a : α) (s : Finmap β) : (erase a s).keys = s.keys.erase a :=
  induction_on s fun s => by simp

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

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

Разделы

Аффилиация

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