English
There is a singleton Finset constructor: for every a in α, {a} is a Finset α.
Русский
Существfет конструктор одиночного финсета: для каждого a ∈ α множество {a} — это Finset α.
LaTeX
$$∀ a, \\{a\\} ∈ Finset(α) and |\\{a\\}| = 1$$
Lean4
/-- `{a} : Finset a` is the set `{a}` containing `a` and nothing else.
This differs from `insert a ∅` in that it does not require a `DecidableEq` instance for `α`.
-/
instance : Singleton α (Finset α) :=
⟨fun a => ⟨{ a }, nodup_singleton a⟩⟩