reduceOption_cons_of_none

Mathlib.Data.List.ReduceOption

URI: https://scilib.ai/kg/mathlib#List.reduceOption_cons_of_none

← MathLib Explorer

English

Removing all None entries from the front or from a list does not change the remaining tail.

Русский

Удаление None в начале списка не изменяет оставшийся хвост.

LaTeX

$$$\operatorname{reduceOption}(\mathrm{none} :: l) = l.reduceOption$$$

Lean4

@[simp]
theorem reduceOption_cons_of_none (l : List (Option α)) : reduceOption (none :: l) = l.reduceOption := by
  simp only [reduceOption, filterMap, id]

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

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

Разделы

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

Аффилиация

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