Decidability of unique existence on a finite type #
∃! a, p a unfolds to an existential bounded by a universal, both decidable
over a Fintype, so unique existence is decidable. Mathlib has the
list-bounded version (List.decidableBExistsUnique) but no Fintype
instance.
[UPSTREAM] Mathlib.Data.Fintype.Defs, beside Fintype.decidableExistsFintype.
@[instance_reducible]
instance
Fintype.decidableExistsUniqueFintype
{α : Type u_1}
{p : α → Prop}
[DecidablePred p]
[Fintype α]
[DecidableEq α]
:
Decidable (∃! a : α, p a)
Equations
- Fintype.decidableExistsUniqueFintype = decidable_of_iff (∃ (a : α), p a ∧ ∀ (b : α), p b → b = a) ⋯