lookup_eq_none

Mathlib.Data.Finmap

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

English

Lookup equals none iff the key is not in the Finmap.

Русский

Поиск равен none тогда, когда ключ отсутствует в Finmap.

LaTeX

$$$$ lookup a s = none \iff a \notin s $$$$

Lean4

theorem lookup_eq_none {a} {s : Finmap β} : lookup a s = none ↔ a ∉ s :=
  induction_on s fun _ => AList.lookup_eq_none

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

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

Разделы

Аффилиация

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