of_surjOn

Mathlib.Data.Set.Finite.Basic

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

English

If f maps s onto t and s is finite, then t is finite.

Русский

Если отображение f проецирует s на t и s конечно, то t конечно.

LaTeX

$$$\operatorname{SurjOn}(f,s,t) \land s \text{ finite} \Rightarrow t \text{ finite}$$$

Lean4

theorem of_surjOn {s : Set α} {t : Set β} (f : α → β) (hf : SurjOn f s t) (hs : s.Finite) : t.Finite :=
  (hs.image _).subset hf

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

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

Разделы

Аффилиация

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