trStmts₁_self

Mathlib.Computability.TMToPartrec

URI: https://scilib.ai/kg/mathlib#Turing.PartrecToTM2.trStmts₁_self

← MathLib Explorer

English

For every q, q belongs to trStmts₁(q).

Русский

Для каждого q выполняется q ∈ trStmts₁(q).

LaTeX

$$$\\forall q:\\; q \\in \\operatorname{trStmts}_1(q)$$$

Lean4

theorem trStmts₁_self (q) : q ∈ trStmts₁ q := by
  induction q <;>
    ·
      first
      | apply Finset.mem_singleton_self
      | apply Finset.mem_insert_self

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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