coe_image_univ — Mathlib

English

The set underlying the Finset image of f on the universe equals the range of f: ↑(Finset.image f Finset.univ) = Set.range f.

Русский

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

LaTeX

$$$\uparrow\bigl(\mathrm{image}\,f\,\mathrm{univ}\bigr) = \mathrm{range}\,f$$$

Lean4

theorem coe_image_univ [Fintype α] [DecidableEq β] {f : α → β} : ↑(Finset.image f Finset.univ) = Set.range f := by simp

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