English
The operation insert a into a Finite set s yields the Finset consisting of a and the elements of s.
Русский
Операция вставки a в конечное множество s даёт конечный набор, содержащий a и элементы s.
LaTeX
$$$\text{insert}: Finset\,\alpha \times Finset\,\alpha \to Finset\,\alpha$ satisfies $insert\,a\,s = \{a\} \cup s$ (i.e., the resulting multiset is $\{a\} \cup s$).$$
Lean4
/-- `insert a s` is the set `{a} ∪ s` containing `a` and the elements of `s`. -/
instance : Insert α (Finset α) :=
⟨fun a s => ⟨_, s.2.ndinsert a⟩⟩