trans — Mathlib

English

If f ≡ᵀ g and g ≡ᵀ h, then f ≡ᵀ h.

Русский

Если f эквивалентно g и g эквивалентно h по Тьюрингу, то f эквивалентно h.

LaTeX

$$$ \forall {f g h : PFun Nat Nat}, TuringEquivalent f g \rightarrow TuringEquivalent g h \rightarrow TuringEquivalent f h$$$

Lean4

@[trans]
theorem trans (f g h : ℕ →. ℕ) (h₁ : f ≡ᵀ g) (h₂ : g ≡ᵀ h) : f ≡ᵀ h :=
  Equivalence.trans equivalence h₁ h₂

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