is_empty

Mathlib.Data.Fintype.EquivFin

URI: https://scilib.ai/kg/mathlib#Function.Embedding.is_empty

English

There is no embedding α ↪ β when α is infinite and β is finite.

Русский

Не существует вложения α ↪ β при условии, что α бесконечно, а β конечен.

LaTeX

$$$ \\nexists e:\\alpha \\hookrightarrow \\beta$$$

Lean4

instance is_empty {α β} [Infinite α] [Finite β] : IsEmpty (α ↪ β) :=
  ⟨fun f => not_injective_infinite_finite f f.2⟩

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

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

Разделы

Аффилиация

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