instNonemptyUniformFun

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

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

English

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

Русский

Если β ненулево, то α →ᵤ[𝔖] β непусто.

LaTeX

$$$\\text{Nonempty}(α \\to^ᵤ[𝔖] β)$, если $\\text{Nonempty}(β)$$$

Lean4

instance [Nonempty β] : Nonempty (α →ᵤ β) :=
  Pi.instNonempty

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

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

Разделы

Аффилиация

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