get_mem

Mathlib.Data.Seq.Computation

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

English

If s terminates, then the value obtained by get s is an element of s.

Русский

Если вычисление s завершается, то значение get(s) принадлежит s.

LaTeX

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

Lean4

theorem get_mem : get s ∈ s :=
  Exists.intro (length s) (Option.eq_some_of_isSome _).symm

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

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

Разделы

Аффилиация

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