toFinset_insert — Mathlib

English

Inserting an element a into a set s and then forming its Finset equals inserting a into the Finset of s: (insert a s).toFinset = insert a s.toFinset.

Русский

Добавление элемента a в множество s, а затем построение Finset равно добавлению a в Finset от s: (insert a s).toFinset = insert a s.toFinset.

LaTeX

$$$(insert\ a\ s).toFinset = insert\ a\ s.toFinset$$$

Lean4

@[simp]
theorem toFinset_insert [DecidableEq α] {a : α} {s : Set α} [Fintype (insert a s : Set α)] [Fintype s] :
    (insert a s).toFinset = insert a s.toFinset := by
  ext
  simp

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