pure_def

Mathlib.Data.Finset.Functor

URI: https://scilib.ai/kg/mathlib#Finset.pure_def

English

The Pure construction on Finset equals the singleton function; i.e., pure x = {x}.

Русский

Конструкция Pure на Finset равна функции-одиночке; то есть pure x = {x}.

LaTeX

$$$$ \\mathrm{pure} = \\mathrm{singleton}. $$$$

Lean4

@[simp]
theorem pure_def {α} : (pure : α → Finset α) = singleton :=
  rfl

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

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

Разделы

Аффилиация

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