uniqueOfSurjectiveConst

Mathlib.Logic.Unique

URI: https://scilib.ai/kg/mathlib#Function.Surjective.uniqueOfSurjectiveConst

Lean4

/-- If a constant function is surjective, then the codomain is a singleton. -/
def uniqueOfSurjectiveConst (α : Type*) {β : Type*} (b : β) (h : Function.Surjective (Function.const α b)) : Unique β :=
  @uniqueOfSubsingleton _ (subsingleton_of_forall_eq b <| h.forall.mpr fun _ ↦ rfl) b

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

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

Разделы

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

Аффилиация

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