reduceOption_mem_iff

Mathlib.Data.List.ReduceOption

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

← MathLib Explorer

English

An element x belongs to reduceOption(l) iff some x belongs to l.

Русский

Элемент x принадлежит reduceOption(l) тогда и только тогда, когда some x принадлежит l.

LaTeX

$$$x \in \mathrm{reduceOption}(l) \iff \mathrm{some}(x) \in l$$$

Lean4

theorem reduceOption_mem_iff {l : List (Option α)} {x : α} : x ∈ l.reduceOption ↔ some x ∈ l := by
  simp only [reduceOption, id, mem_filterMap, exists_eq_right]

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

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

Разделы

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

Аффилиация

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