toFinset_insert — Mathlib

English

If s is finite, then the Finset corresponding to insert a into s equals inserting a into the Finset of s.

Русский

Если s конечно, то соответствующий Finset образа вставки a в s равен вставке a в Finset s.

LaTeX

$$$ (hs : (insert a s).Finite).toFinset = insert a (hs.subset (subset_insert _ _)).toFinset $$$

Lean4

@[simp]
theorem toFinset_insert [DecidableEq α] {s : Set α} {a : α} (hs : (insert a s).Finite) :
    hs.toFinset = insert a (hs.subset <| subset_insert _ _).toFinset :=
  Finset.ext <| by simp

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