English
For any nonempty α, the map b ↦ (const α b) from β to α → β is injective.
Русский
Если α непусто, отображение b ↦ (константная функция на α, значащая β) из β в α → β инъективно.
LaTeX
$$$$\\\\forall{b_1,b_2:\\\\beta},\\\\ (\\\\mathrm{const}_{\\\\alpha}(b_1) = \\\\mathrm{const}_{\\\\alpha}(b_2)) \\\\Rightarrow b_1 = b_2. $$$$
Lean4
/-- This invokes the two `Decidable` arguments $O(n)$ times. -/
instance decidableBExistsUnique {α : Type*} [DecidableEq α] (p : α → Prop) [DecidablePred p] :
(l : List α) → Decidable (∃! x, x ∈ l ∧ p x)
| [] => .isFalse <| by simp
| x :: xs =>
if hx : p x then
decidable_of_iff (∀ y ∈ xs, p y → x = y)
(⟨fun h ↦ ⟨x, by grind⟩, fun ⟨z, h⟩ y hy hp ↦ (h.2 x ⟨mem_cons_self, hx⟩).trans (by grind)⟩)
else
have := List.decidableBExistsUnique p xs
decidable_of_iff (∃! x, x ∈ xs ∧ p x) (by grind)
