instDecidableCurryOfMk_mathlib — Mathlib

English

There is a typeclass instance that provides a decidable instance for the curry of a relation r on α × β, given decidability of r at each pair (a,b).

Русский

Существет экземпляр типа decidable для карри-отношения r на α×β, при условии существования decidable(r (a,b)) для каждого пары.

LaTeX

$${[Decidable (r (a,b))]} ⇒ Decidable (Function.curry r a b)$$

Lean4

instance {α β : Type*} {r : α × β → Prop} {a : α} {b : β} [Decidable (r (a, b))] : Decidable (curry r a b) :=
  ‹Decidable _›

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