computable_iff — Mathlib

English

A predicate is computable if and only if it can be represented as a computable predicate paired with a computable function returning a Boolean value.

Русский

Предикат вычислим тогда и только тогда, когда его можно представить как вычислимый предикат в паре с вычислимой функцией, возвращающей значение Bool.

LaTeX

$$ComputablePred p ↔ ∃ f : α → Bool, Computable f ∧ p = fun a => (f a : Prop)$$

Lean4

theorem computable_iff {p : α → Prop} : ComputablePred p ↔ ∃ f : α → Bool, Computable f ∧ p = fun a => (f a : Prop) :=
  ⟨fun ⟨_, h⟩ => ⟨_, h, funext fun _ => propext (Bool.decide_iff _).symm⟩, by rintro ⟨f, h, rfl⟩;
    exact ⟨by infer_instance, by simpa using h⟩⟩

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