pure

Mathlib.Data.Finset.Functor

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

English

The Pure construction on Finset is the singleton construction; each element maps to its singleton set.

Русский

Конструкция Pure на Finset совпадает с операцией единичной свертки: каждое элементу отображается в его одинокое множество.

LaTeX

$$$$ \\mathrm{pure}(x) = \\{x\\}. $$$$

Lean4

protected instance pure : Pure Finset :=
  ⟨fun x => { x }⟩

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

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

Разделы

Аффилиация

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