oneOneReducible_refl

Mathlib.Computability.Reduce

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

English

The one-one reducibility relation is reflexive.

Русский

Редукция one-one рефлексивна.

LaTeX

$$$\forall {\alpha} [Primcodable \alpha],\forall p: \alpha \to Prop,\ p ≤₁ p$$$

Lean4

@[refl]
theorem oneOneReducible_refl {α} [Primcodable α] (p : α → Prop) : p ≤₁ p :=
  ⟨id, Computable.id, injective_id, by simp⟩

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

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

Разделы

Аффилиация

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