English
If a is inserted into a finite set s, the resulting set is finite.
Русский
Если элемент a вставить в конечное множество s, полученное множество тоже конечное.
LaTeX
$$$\\forall a\\in\\alpha,\\forall s\\subseteq \\alpha,\\operatorname{Finite}(s) \\Rightarrow \\operatorname{Finite}(\\operatorname{insert}(a,s)).$$$
Lean4
/-- A `Fintype` instance for inserting an element into a `Set` using the
corresponding `insert` function on `Finset`. This requires `DecidableEq α`.
There is also `Set.fintypeInsert'` when `a ∈ s` is decidable. -/
instance fintypeInsert (a : α) (s : Set α) [DecidableEq α] [Fintype s] : Fintype (insert a s : Set α) :=
Fintype.ofFinset (insert a s.toFinset) <| by simp
