of_eq — Mathlib

English

Let r and s be relations with r primitive recursive; if r a b ↔ s a b for all a,b, then s is primitive recursive.

Русский

Пусть r и s — отношения; если r дано примитивно вычислимо, и r(a,b) ↔ s(a,b) для всех a,b, то s тоже примитивно вычислима.

LaTeX

$$$\operatorname{PrimrecRel} r \to (\forall a,b, r(a,b) \leftrightarrow s(a,b)) \to \operatorname{PrimrecRel} s$$$

Lean4

theorem of_eq {α} [Primcodable α] {p q : α → Prop} (hp : PrimrecPred p) (H : ∀ a, p a ↔ q a) : PrimrecPred q :=
  funext (fun a => propext (H a)) ▸ hp

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