mem_iff — Mathlib

English

An element a belongs to Finmap s iff there exists b with s.lookup a = some b.

Русский

Элемент a принадлежит Finmap s тогда, когда существует b, такое что s.lookup a = some b.

LaTeX

$$$$ a \in s \iff \exists b, s.lookup a = \mathrm{some} b $$$$

Lean4

theorem mem_iff {a : α} {s : Finmap β} : a ∈ s ↔ ∃ b, s.lookup a = some b :=
  induction_on s fun s => Iff.trans List.mem_keys <| exists_congr fun _ => (mem_dlookup_iff s.nodupKeys).symm

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