coe_union — Mathlib

English

The embedding from Finset to Set preserves unions: the image of the union equals the union of images.

Русский

Ембединение из Finset в Set сохраняет объединение: образ объединения равен объединению образов.

LaTeX

$$$ \uparrow (s_{1} \cup s_{2}) = (s_{1} \cup s_{2}) \; :\; Set\,\alpha $$$

Lean4

@[simp, norm_cast]
theorem coe_union (s₁ s₂ : Finset α) : ↑(s₁ ∪ s₂) = (s₁ ∪ s₂ : Set α) :=
  Set.ext fun _ => mem_union

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