phi

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

URI: https://scilib.ai/kg/mathlib#UniformFun.phi

English

The phi map sends ((f,g), x) to (f(x), g(x)) for f,g ∈ α →ᵤ β and x ∈ α.

Русский

Функция φ отправляет ((f,g), x) в (f(x), g(x)) для f,g ∈ α →ᵤ β и x ∈ α.

LaTeX

$$$\\phi( (f,g), x ) = (f(x), g(x))$$$

Lean4

protected def phi (α β : Type*) (uvx : ((α →ᵤ β) × (α →ᵤ β)) × α) : β × β :=
  (uvx.fst.fst uvx.2, uvx.1.2 uvx.2)

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

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

Разделы

Аффилиация

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