keys_singleton

Mathlib.Data.Finmap

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

English

The keys of a singleton Finmap contain exactly the single key.

Русский

Ключи синглтона Finmap содержат ровно один ключ.

LaTeX

$$$$ (singleton a b).\mathrm{keys} = { a } $$$$

Lean4

@[simp]
theorem keys_singleton (a : α) (b : β a) : (singleton a b).keys = { a } :=
  rfl

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

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

Разделы

Аффилиация

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