toFinset_image — Mathlib

English

The Finset of the image of a set under a function f equals the image of the Finset of the set: (f '' s).toFinset = s.toFinset.image f.

Русский

Образ множества s под действием функции f в виде Finset равен изображению Finset от самого множества: (f '' s).toFinset = s.toFinset.image f.

LaTeX

$$$\bigl(f '' s\bigr).toFinset = s.toFinset.image f$$

Lean4

@[simp]
theorem toFinset_image [DecidableEq β] (f : α → β) (s : Set α) [Fintype s] [Fintype (f '' s)] :
    (f '' s).toFinset = s.toFinset.image f :=
  Finset.coe_injective <| by simp

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