get_eq_of_promises

Mathlib.Data.Seq.Computation

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

English

If a ∈ s, then get s = a.

Русский

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

LaTeX

$$$\forall s\,[h:\,\text{ Terminates } s], {a:\,\alpha}, a \in s \rightarrow \text{get } s = a$$$

Lean4

theorem get_eq_of_promises {a} : s ~> a → get s = a :=
  get_eq_of_mem _ ∘ mem_of_promises _

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

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

Разделы

Аффилиация

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