lookup_isSome

Mathlib.Data.Finmap

URI: https://scilib.ai/kg/mathlib#Finmap.lookup_isSome

English

The lookup of a is Some precisely when a is in the Finmap.

Русский

Поиск элемента a в Finmap даёт Some тогда, когда a в Finmap.

LaTeX

$$$$ (s.lookup a).isSome \leftrightarrow a \in s $$$$

Lean4

theorem lookup_isSome {a : α} {s : Finmap β} : (s.lookup a).isSome ↔ a ∈ s :=
  induction_on s fun _ => AList.lookup_isSome

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

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

Разделы

Аффилиация

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