instDecidablePredMemSetColorClassOfDecidableEq

English

If α has decidable equality, then for each color c the predicate x ↦ x ∈ colorClass c is decidable.

Русский

Если равенство в α детерминировано, то для каждого цвета c предикат x ∈ colorClass c детерминирован.

LaTeX

$$$\\forall c, \\operatorname{DecidablePred}(\\lambda x. x \\in C.colorClass c)$$$

Lean4

instance [DecidableEq α] {c : α} : DecidablePred (· ∈ C.colorClass c) :=
  inferInstanceAs <| DecidablePred (· ∈ {v | C v = c})

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