fold_union_empty_singleton — Mathlib

English

Let s be a finite set of elements in α. The union of the singleton sets {a} over all a in s equals s; i.e. the singletons over s form s when joined by union.

Русский

Пусть s — конечное множество элементов α. Объединение одноэлементных множеств {a} по всем a ∈ s даёт s; то есть ⋃_{a∈s} {a} = s.

LaTeX

$$$$ \\bigcup_{a \\in s} \\{a\\} = s. $$$$

Lean4

@[simp]
theorem fold_union_empty_singleton [DecidableEq α] (s : Finset α) : Finset.fold (· ∪ ·) ∅ singleton s = s := by
  induction s using Finset.induction_on with
  | empty => simp only [fold_empty]
  | insert a s has ih => rw [fold_insert has, ih, insert_eq]

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