lookup_eq_none

Mathlib.Data.List.AList

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

English

For any a and s, lookup a s = none iff a ∉ s.

Русский

Для любых a и s, lookup a s = none эквивалентно a ∉ s.

LaTeX

$$lookup(a,s) = none \iff a \notin s$$

Lean4

theorem lookup_eq_none {a : α} {s : AList β} : lookup a s = none ↔ a ∉ s :=
  dlookup_eq_none

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

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

Разделы

Аффилиация

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