subsingleton_dom

Mathlib.Data.FunLike.Basic

URI: https://scilib.ai/kg/mathlib#DFunLike.subsingleton_dom

← MathLib Explorer

English

If the domain α is empty, then F is Subsingleton.

Русский

Если множество аргументов пусто, то F имеет одноэлементную структуру.

LaTeX

$$$[IsEmpty \alpha] \Rightarrow \operatorname{Subsingleton}(F).$$$

Lean4

/-- This is not an instance to avoid slowing down every single `Subsingleton` typeclass search. -/
theorem subsingleton_dom [IsEmpty α] : Subsingleton F :=
  coe_injective.subsingleton

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

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

Разделы

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

Аффилиация

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