eraseNone_insertNone

Mathlib.Data.Finset.Option

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

English

Applying insertNone after eraseNone recovers the original Finset augmented by none: insertNone(eraseNone(s)) = insert none s.

Русский

Применение insertNone после eraseNone восстанавливает исходное Finset, дополненное none.

LaTeX

$$$\\text{insertNone}(\\text{eraseNone}(s)) = \\text{insertNone}(s)$$$

Lean4

@[simp]
theorem eraseNone_insertNone (s : Finset α) : eraseNone (insertNone s) = s :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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