toNat_manyOneReducible

Mathlib.Computability.Reduce

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

← MathLib Explorer

English

For any set p, toNat p is reducible to p.

Русский

Для любого множества p из α, toNat p редуцируется к p.

LaTeX

$$$ toNat\ p \\le_0 p $$$

Lean4

@[simp]
theorem toNat_manyOneReducible {p : Set α} : toNat p ≤₀ p :=
  ⟨fun n => (Encodable.decode (α := α) n).getD default, Computable.option_getD Computable.decode (Computable.const _),
    fun _ => Iff.rfl⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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