toFinset_some

Mathlib.Data.Finset.Option

URI: https://scilib.ai/kg/mathlib#Option.toFinset_some

English

The toFinset of some a is the singleton {a}.

Русский

toFinset от some a равен {a}.

LaTeX

$$$ toFinset (\mathrm{some}\ a) = \{ a \}$$$

Lean4

@[simp]
theorem toFinset_some {a : α} : (some a).toFinset = { a } :=
  rfl

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

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

Разделы

Аффилиация

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