mk

Mathlib.Computability.Reduce

URI: https://scilib.ai/kg/mathlib#OneOneReducible.mk

Lean4

theorem mk {α β} [Primcodable α] [Primcodable β] {f : α → β} (q : β → Prop) (h : Computable f) (i : Injective f) :
    (fun a => q (f a)) ≤₁ q :=
  ⟨f, h, i, fun _ => Iff.rfl⟩

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

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

Разделы

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

Аффилиация

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