of_think_mem

Mathlib.Data.Seq.Computation

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

English

If a' ∈ think s, then a' ∈ s.

Русский

Если a' принадлежит think s, то принадлежит s.

LaTeX

$$$a' \in \mathrm{think}(s) \Rightarrow a' \in s$$$

Lean4

theorem of_think_mem {s : Computation α} {a} : a ∈ think s → a ∈ s
  | ⟨n, h⟩ => by
    rcases n with - | n'
    · contradiction
    · exact ⟨n', h⟩

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

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

Разделы

Аффилиация

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