toFinset_range — Mathlib

English

If range f is finite, then the Finset of its range equals the image of Finset.univ under f.

Русский

Если множество значений функции f (range f) конечно, то Finset диапазона равен образу Finset.univ под действием f.

LaTeX

$$$ h.toFinset = \mathrm{Finset.univ}.image f $$$

Lean4

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

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