decidableMemRangeFintype — Mathlib

English

In a finite domain, for any f: α → β with DecidableEq β, the predicate x ∈ Set.range(f) is decidable.

Русский

В конечном домене для любой функции f: α → β с DecidableEq β принадлежность x ∈ Set.range(f) разрешима (решаема).

LaTeX

$$$\\forall f : \\alpha \\to \\beta,\\; \\operatorname{DecidablePred}(\\lambda x. x \\in \\mathrm{Set.range}(f))$$$

Lean4

instance decidableMemRangeFintype [Fintype α] [DecidableEq β] (f : α → β) : DecidablePred (· ∈ Set.range f) := fun _ =>
  Fintype.decidableExistsFintype

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