map

Mathlib.Data.Set.Finite.Basic

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

English

A finite set remains finite after applying a function.

Русский

Прообраз изображение сохраняет конечность.

LaTeX

$$$\forall f:\\alpha \to \beta, \mathrm{Finite}(s) \Rightarrow \mathrm{Finite}(f''s)$$$

Lean4

theorem map {α β} {s : Set α} : ∀ f : α → β, s.Finite → (f <$> s).Finite :=
  Finite.image

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

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

Разделы

Аффилиация

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