get_eq_of_mem

Mathlib.Data.Seq.Computation

URI: https://scilib.ai/kg/mathlib#Computation.get_eq_of_mem

English

If a ∈ s, then get s = a.

Русский

Если a ∈ s, то get(s) = a.

LaTeX

$$$\forall s\,[\text{Terminates}(s)],\; \forall a,\ (a \in s) \rightarrow \text{get }s = a$$$

Lean4

theorem get_eq_of_mem {a} : a ∈ s → get s = a :=
  mem_unique (get_mem _)

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

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

Разделы

Аффилиация

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