toFinset_range — Mathlib

English

The Finset of the range of a function f equals the image of the universal Finset under f: (Set.range f).toFinset = Finset.univ.image f.

Русский

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

LaTeX

$$$\mathrm{range}(f)\toFinset = \mathrm{univ}.image\,f$$

Lean4

@[simp]
theorem toFinset_range [DecidableEq α] [Fintype β] (f : β → α) [Fintype (Set.range f)] :
    (Set.range f).toFinset = Finset.univ.image f := by
  ext
  simp

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