manyOneEquiv_toNat

Mathlib.Computability.Reduce

URI: https://scilib.ai/kg/mathlib#manyOneEquiv_toNat

English

There is an equivalence between toNat-pairs and p-pairs under ManyOneEquiv.

Русский

Существует эквивалентность между парами toNat и парами p под ManyOneEquiv.

LaTeX

$$$ \\ManyOneEquiv (toNat p) (toNat q) \\iff \\ManyOneEquiv p q $$$

Lean4

@[simp]
theorem manyOneEquiv_toNat (p : Set α) (q : Set β) : ManyOneEquiv (toNat p) (toNat q) ↔ ManyOneEquiv p q := by
  simp [ManyOneEquiv]

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

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

Разделы

Аффилиация

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