eraseNone_image_some

Mathlib.Data.Finset.Option

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

← MathLib Explorer

English

The eraseNone of the image of s under some equals s with none removed, i.e., s.erase none.

Русский

eraseNone от image some s равно s, удалив none.

LaTeX

$$$\\text{eraseNone}(\\text{image} \\text{Some}\, s) = s \\;\\text{erase} \\;\\text{none}$$$

Lean4

@[simp]
theorem eraseNone_image_some [DecidableEq (Option α)] (s : Finset α) : eraseNone (s.image some) = s := by
  simpa only [map_eq_image] using eraseNone_map_some s

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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