not_surjective_finite_infinite

Mathlib.Data.Fintype.EquivFin

URI: https://scilib.ai/kg/mathlib#not_surjective_finite_infinite

← MathLib Explorer

English

There is no surjective function from a finite α onto an infinite β.

Русский

Не существует сюръекции от конечного α на бесконечный β.

LaTeX

$$$ \\forall f:\\alpha \\to \\beta, \\operatorname{Surjective}(f) \\Rightarrow \\bot$$$

Lean4

theorem not_surjective_finite_infinite {α β} [Finite α] [Infinite β] (f : α → β) : ¬Surjective f := fun hf =>
  (Infinite.of_surjective f hf).not_finite ‹_›

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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