equiv₂

Mathlib.Computability.Reduce

URI: https://scilib.ai/kg/mathlib#Computable.equiv₂

English

Computable denumerable equivalence for α, β: Denumerable.equiv₂ α β is computable.

Русский

Вычислимая денумерируемая эквивалентность Denumerable.equiv₂ α β.

LaTeX

$$$\text{Computable}(\text{Denumerable.equiv₂}\;\alpha\;\beta)$$$

Lean4

theorem equiv₂ (α β) [Denumerable α] [Denumerable β] : (Denumerable.equiv₂ α β).Computable :=
  (Computable.eqv _).trans (Computable.eqv _).symm

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

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

Разделы

Аффилиация

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