mem_lookup_iff

Mathlib.Data.Finmap

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

← MathLib Explorer

English

For any s,a,b, b ∈ s.lookup a iff ⟨a,b⟩ ∈ s.entries.

Русский

Для любых s,a,b: b ∈ s.lookup a эквивалентно ⟨a,b⟩ ∈ s.entries.

LaTeX

$$$$ b \in s.lookup a \iff \langle a,b\rangle \in s.\mathrm{entries} $$$$

Lean4

theorem mem_lookup_iff {s : Finmap β} {a : α} {b : β a} : b ∈ s.lookup a ↔ Sigma.mk a b ∈ s.entries := by
  rcases s with ⟨⟨l⟩, hl⟩; exact List.mem_dlookup_iff hl

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

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

Разделы

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

Аффилиация

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