decidableMemRange — Mathlib

English

There is a decidable predicate for membership in the range of sigmaCongrRightHom when α and β are finite and have decidable equality.

Русский

СуществуютDecidablePred для принадлежности к образу sigmaCongrRightHom при конечных типах с заданной эквивалентностью.

LaTeX

$$$\\text{DecidablePred}(\\,x\\in (\\mathrm{sigmaCongrRightHom}\\;\\beta).\\mathrm{range}\\,)$$$

Lean4

instance decidableMemRange {α : Type*} {β : α → Type*} [DecidableEq α] [∀ a, DecidableEq (β a)] [Fintype α]
    [∀ a, Fintype (β a)] : DecidablePred (· ∈ (sigmaCongrRightHom β).range) := fun _ => inferInstance

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