not_injective_infinite_finite

Mathlib.Data.Fintype.EquivFin

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

English

There is no injective function from an infinite α to a finite β.

Русский

Нет инъективной функции из бесконечного α в конечное β.

LaTeX

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

Lean4

theorem not_injective_infinite_finite {α β} [Infinite α] [Finite β] (f : α → β) : ¬Injective f := fun hf =>
  (Finite.of_injective f hf).false

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

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

Разделы

Аффилиация

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