toFinset_append — Mathlib

English

The Finset corresponding to the concatenation of two lists equals the union of the Finsets corresponding to each list.

Русский

Финсет, соответствующий конкатенации двух списков, равен объединению финсет-образов каждого списка.

LaTeX

$$toFinset (l ++ l') = l.toFinset ∪ l'.toFinset$$

Lean4

@[simp]
theorem toFinset_append : toFinset (l ++ l') = l.toFinset ∪ l'.toFinset := by
  induction l with
  | nil => simp
  | cons hd tl hl => simp [hl]

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