trStmts — Mathlib

English

The set of translated statements is built from the TM1 stmts extended by all possibilities in Finite universe.

Русский

Переведённое множество утверждений строится из TM1 stmts и всех возможностей во множестве Finite.

LaTeX

$$trStmts (S) = TM1.stmts M S ×ˢ Finset.univ$$

Lean4

/-- Given a finite set of accessible `Λ` machine states, there is a finite set of accessible
machine states in the target (even though the type `Λ'` is infinite). -/
noncomputable def trStmts (S : Finset Λ) : Finset (Λ' M) :=
  (TM1.stmts M S) ×ˢ Finset.univ

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