instSubsingletonOfIsEmpty

Mathlib.Topology.ContinuousMap.Defs

URI: https://scilib.ai/kg/mathlib#ContinuousMap.instSubsingletonOfIsEmpty

English

If X is empty, then any two maps X → Y are equal; hence C(X,Y) is Subsingleton.

Русский

Если X пусто, то любые две функции X → Y совпадают; следовательно, C(X,Y) — подмножество с одним элементом.

LaTeX

$$$ [\\text{IsEmpty } X] \\Rightarrow \\text{Subsingleton } C(X,Y) $$$

Lean4

instance [IsEmpty X] : Subsingleton C(X, Y) :=
  DFunLike.subsingleton_dom

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

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

Разделы

Аффилиация

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