symm

Mathlib.Computability.Reduce

URI: https://scilib.ai/kg/mathlib#Equiv.Computable.symm

English

If e.Computable, then e.symm.Computable.

Русский

Если e вычислима, то e.symm вычислима.

LaTeX

$$$e.Computable \Rightarrow e.symm.Computable$$$

Lean4

theorem symm {α β} [Primcodable α] [Primcodable β] {e : α ≃ β} : e.Computable → e.symm.Computable :=
  And.symm

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

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

Разделы

Аффилиация

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