manyOneEquiv_refl

Mathlib.Computability.Reduce

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

English

For any p, ManyOneEquiv p p holds.

Русский

Для любого p выполняется ManyOneEquiv p p.

LaTeX

$$$\forall p:\alpha\to\mathrm{Prop},\ ManyOneEquiv\,p\,p$$$

Lean4

@[refl]
theorem manyOneEquiv_refl {α} [Primcodable α] (p : α → Prop) : ManyOneEquiv p p :=
  ⟨manyOneReducible_refl _, manyOneReducible_refl _⟩

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

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

Разделы

Аффилиация

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