of_surjective

Mathlib.Data.Fintype.EquivFin

URI: https://scilib.ai/kg/mathlib#Finite.of_surjective

English

If α is finite and f: α → β is surjective, then β is finite.

Русский

Если α конечен и f: α → β — сюръективна, то β конечен.

LaTeX

$$$\operatorname{Finite}(\alpha) \land \operatorname{Surjective}(f) \Rightarrow \operatorname{Finite}(\beta).$$$

Lean4

theorem of_surjective {α β : Sort*} [Finite α] (f : α → β) (H : Surjective f) : Finite β :=
  Finite.of_injective _ <| injective_surjInv H

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

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

Разделы

Аффилиация

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