toFinset_image — Mathlib

English

The Finset of the image f '' s equals the image of the Finset s under f: h.toFinset = hs.toFinset.image f.

Русский

Образ Finset через отображение f совпадает с образующим Finset: h.toFinset = hs.toFinset.image f.

LaTeX

$$$ h.toFinset = hs.toFinset.image f $$$

Lean4

protected theorem toFinset_image [DecidableEq β] (f : α → β) (hs : s.Finite) (h : (f '' s).Finite) :
    h.toFinset = hs.toFinset.image f := by
  ext
  simp

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