instSubsingletonUniformFun

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

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

English

If β is a subsingleton, then α →ᵤ[𝔖] β is a subsingleton.

Русский

Если β — частное, то α →ᵤ[𝔖] β — частное.

LaTeX

$$$\\text{Subsingleton}(β) \\Rightarrow \\text{Subsingleton}(α \\to^ᵤ[𝔖] β)$$$

Lean4

instance [Subsingleton β] : Subsingleton (α →ᵤ β) :=
  inferInstanceAs <| Subsingleton <| α → β

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

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

Разделы

Аффилиация

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