computable_of_manyOneReducible — Mathlib

English

If p ≤₀ q and q is computable, then p is computable.

Русский

Если p ≤₀ q и q вычислимо, то p вычислимо.

LaTeX

$$$p\le_0 q\quad\land\quad ComputablePred\,q\; \Rightarrow\; ComputablePred\,p$$$

Lean4

theorem computable_of_manyOneReducible {p : α → Prop} {q : β → Prop} (h₁ : p ≤₀ q) (h₂ : ComputablePred q) :
    ComputablePred p := by
  rcases h₁ with ⟨f, c, hf⟩
  rw [show p = fun a => q (f a) from Set.ext hf]
  rcases computable_iff.1 h₂ with ⟨g, hg, rfl⟩
  exact ⟨by infer_instance, by simpa using hg.comp c⟩

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