dlookup_eq_none

Mathlib.Data.List.Sigma

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

English

dlookup a l equals none if and only if a is not in the keys of l.

Русский

dlookup a l равно none тогда и только тогда, когда a не принадлежит ключам l.

LaTeX

$$$ dlookup a l = \\mathrm{none} \\iff a \\notin l.keys $$$

Lean4

theorem dlookup_eq_none {a : α} {l : List (Sigma β)} : dlookup a l = none ↔ a ∉ l.keys := by
  simp [← dlookup_isSome, Option.isNone_iff_eq_none]

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

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

Разделы

Аффилиация

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