reflexive_manyOneReducible

Mathlib.Computability.Reduce

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

English

Redundantly restating reflexivity for the same reducibility relation.

Русский

Редуктивность для той же самой редукции повторяется.

LaTeX

$$$\mathrm{reflexive\_manyOneReducible} :\ Reflexive\ ManyOneReducible$$$

Lean4

theorem reflexive_manyOneReducible {α} [Primcodable α] : Reflexive (@ManyOneReducible α α _ _) :=
  manyOneReducible_refl

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

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

Разделы

Аффилиация

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