reflexive_oneOneReducible — Mathlib

English

For any type α with Primcodable structure, the relation ≤₁ on predicates p: α→Prop is reflexive.

Русский

Для любого типа α с примитивной кодируемостью отношение ≤₁ на предикатах p: α→Prop является рефлексивным.

LaTeX

$$$\forall \alpha\ ([Primcodable\ \alpha])\;\text{Reflexive}(@OneOneReducible\ \alpha\ \alpha\_\_\_)$$$

Lean4

theorem reflexive_oneOneReducible {α} [Primcodable α] : Reflexive (@OneOneReducible α α _ _) :=
  oneOneReducible_refl

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