manyOneReducible_toNat

Mathlib.Computability.Reduce

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

English

toNat p is ManyOne-equivalent to p.

Русский

toNat p эквивалентно p поManyOneEquiv.

LaTeX

$$$ \\ManyOneEquiv (toNat p) p $$$

Lean4

@[simp]
theorem manyOneReducible_toNat {p : Set α} : p ≤₀ toNat p :=
  ⟨Encodable.encode, Computable.encode, by simp [toNat, setOf]⟩

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

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

Разделы

Аффилиация

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