decidablePred — Mathlib

English

There is a decidable predicate for membership in Sym2.fromRel when r is symmetric and decidable.

Русский

Существуют определяемые по знаку принадлежности в Sym2.fromRel при условии, что r симметрично и разрешимо.

LaTeX

$$$$ \text{There is a } \mathrm{DecidablePred}\ (\cdot \in \mathrm{Sym2.fromRel}(sym)) \text{ given } (sym : \mathrm{Symmetric}\ r) \text{ and } [\,h: \mathrm{DecidableRel}\ r\]. $$$$

Lean4

instance decidablePred (sym : Symmetric r) [h : DecidableRel r] : DecidablePred (· ∈ Sym2.fromRel sym) := fun z =>
  z.recOnSubsingleton fun _ => h _ _

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