finite_range

Mathlib.Data.Set.Finite.Range

URI: https://scilib.ai/kg/mathlib#Set.finite_range

English

The range of a function has finite cardinality when the domain is finite.

Русский

Образ функции имеет конечную мощность, если область конечна.

LaTeX

$$$ \forall f : \mathrm{Set}(\alpha) \to \mathrm{Set}(\beta), \mathrm{Finite}(\mathrm{domain}(f)) \rightarrow \mathrm{Finite}(\mathrm{range}(f))$$$

Lean4

theorem finite_range (f : ι → α) [Finite ι] : (range f).Finite :=
  toFinite _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru