eqv

Mathlib.Computability.Reduce

URI: https://scilib.ai/kg/mathlib#Computable.eqv

English

If α is denumerable, then the equivalence Denumerable.eqv α is computable.

Русский

Для денумерируемого множества α эквивалентность Denumerable.eqv α вычислима.

LaTeX

$$$(\text{Denumerable.eqv}\; \alpha).\Computable$$$

Lean4

theorem eqv (α) [Denumerable α] : (Denumerable.eqv α).Computable :=
  ⟨Computable.encode, Computable.ofNat _⟩

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

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

Разделы

Аффилиация

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