finite_replacement

Mathlib.Data.Set.Finite.Range

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

English

The set {f x | x ∈ α} is finite if α is finite.

Русский

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

LaTeX

$$$ \forall f : \alpha \to \beta, \text{Finite}(\alpha) \rightarrow \mathrm{Finite}(\{ f(x) : x \in \alpha \})$$$

Lean4

instance finite_replacement [Finite α] (f : α → β) : Finite {f x | x : α} :=
  Finite.Set.finite_range f

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

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

Разделы

Аффилиация

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