mem_of_get_eq

Mathlib.Data.Seq.Computation

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

English

If get s = a, then a ∈ s.

Русский

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

LaTeX

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

Lean4

theorem mem_of_get_eq {a} : get s = a → a ∈ s := by intro h; rw [← h]; apply get_mem

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

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

Разделы

Аффилиация

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