ofFun_toFun

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

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

English

ofFun and its inverse compose to identity on UniformFun.

Русский

ofFun и его обратная композиция дают тождественный отображение на UniformFun.

LaTeX

$$$\\text{ofFun}(\\text{toFun}(f)) = f$ for all $f : \\mathrm{UniformFun}(\\alpha,\\beta)$$$

Lean4

@[simp]
theorem ofFun_toFun (f : α →ᵤ β) : ofFun (toFun f) = f :=
  rfl

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

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

Разделы

Аффилиация

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