of_eq

Mathlib.Computability.Halting

URI: https://scilib.ai/kg/mathlib#ComputablePred.of_eq

← MathLib Explorer

English

Alternative formulation of dom_re in the Partrec namespace.

Русский

Альтернативная формулировка dom_re в пространстве Partrec.

LaTeX

$$Partrec f → REPred fun a => (f a).Dom$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru