instSingleton — Mathlib

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⟩⟩

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