mem_of_lookup_eq_some — Mathlib

English

Let α be a type, β a family of types indexed by α, and s a Finmap β. For any a: α and b: β(a), if s.lookup a = some b, then a ∈ s.

Русский

Пусть α — множество, β — семейство типов, индексируемое по α, и s — Finmap β. Для любого a : α и b : β(a), если s.lookup a = some b, то a ∈ s.

LaTeX

$$$ \forall a : \alpha, \forall b : \beta(a), \forall s : Finmap\, \beta, \ lookup(a,s) = \mathrm{Some}(b) \Rightarrow a \in s. $$$

Lean4

theorem mem_of_lookup_eq_some {a : α} {b : β a} {s : Finmap β} (h : s.lookup a = some b) : a ∈ s :=
  mem_iff.mpr ⟨_, h⟩

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