uniqueOfSurjectiveOne

Mathlib.Algebra.Group.Pi.Basic

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

Lean4

/-- If the one function is surjective, the codomain is trivial. -/
@[to_additive /-- If the zero function is surjective, the codomain is trivial. -/
    ]
def uniqueOfSurjectiveOne (α : Type*) {β : Type*} [One β] (h : Function.Surjective (1 : α → β)) : Unique β :=
  h.uniqueOfSurjectiveConst α (1 : β)

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

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

Разделы

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

Аффилиация

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