trans — Mathlib

English

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

Русский

Если f сводимо к g, а g сводимо к h, то f сводимо к h.

LaTeX

$$$ f \le_T g \rightarrow g \le_T h \rightarrow f \le_T h $$$

Lean4

theorem trans (hg : f ≤ᵀ g) (hh : g ≤ᵀ h) : f ≤ᵀ h := by
  induction hg with
    repeat { constructor
    }
  | oracle _ hg => rw [Set.mem_singleton_iff] at hg; rw [hg]; exact hh
  | pair _ _ ih₁ ih₂ => exact RecursiveIn.pair ih₁ ih₂
  | comp _ _ ih₁ ih₂ => exact RecursiveIn.comp ih₁ ih₂
  | prec _ _ ih₁ ih₂ => exact RecursiveIn.prec ih₁ ih₂
  | rfind _ ih => exact RecursiveIn.rfind ih

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