fintypeImage — Mathlib

English

If s is finite and f is a function, then the image f''s is finite.

Русский

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

LaTeX

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

Lean4

instance fintypeImage [DecidableEq β] (s : Set α) (f : α → β) [Fintype s] : Fintype (f '' s) :=
  Fintype.ofFinset (s.toFinset.image f) <| by simp

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