fintypeMap

Mathlib.Data.Set.Finite.Basic

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

English

If s is finite, the image f''s is finite (alias of image finiteness).

Русский

Если s конечно, то образ f(s) конечно (аналог образа).

LaTeX

$$$\\forall s\\subseteq \\alpha,\\; \\operatorname{Finite}(s) \\Rightarrow \\operatorname{Finite}(f''s).$$$

Lean4

instance fintypeMap {α β} [DecidableEq β] : ∀ (s : Set α) (f : α → β) [Fintype s], Fintype (f <$> s) :=
  Set.fintypeImage

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

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

Разделы

Аффилиация

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