injective_of_subsingleton

Mathlib.Logic.Function.Basic

URI: https://scilib.ai/kg/mathlib#Function.injective_of_subsingleton

English

If the domain is a singleton, any function is injective.

Русский

Если область определения содержит ровно один элемент, любая функция инъективна.

LaTeX

$$[Subsingleton\\, α] \\Rightarrow Injective\\,f$$

Lean4

@[nontriviality]
theorem injective_of_subsingleton [Subsingleton α] (f : α → β) : Injective f := fun _ _ _ ↦ Subsingleton.elim _ _

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

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

Разделы

Аффилиация

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