instInsert — Mathlib

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

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