finite_image

Mathlib.Data.Set.Finite.Basic

URI: https://scilib.ai/kg/mathlib#Finite.Set.finite_image

English

The image of a finite set under any function is finite.

Русский

Образ конечного множества под любой функцией также конечен.

LaTeX

$$$\forall {\alpha : Type u} {\beta : Type v} (s : Set\alpha) (f : \alpha \to \beta), Finite s \to Finite (f '' s)$$$

Lean4

instance finite_image (s : Set α) (f : α → β) [Finite s] : Finite (f '' s) :=
  by
  cases nonempty_fintype s
  classical infer_instance

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

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

Разделы

Аффилиация

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