toUniformOnFun_toFun

Mathlib.Topology.UniformSpace.CompactConvergence

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

English

The canonical map from C(α,β) to UniformOnFun is the identity on the underlying functions.

Русский

Единый отображение из C(α,β) в UniformOnFun является тождественным на базовых функциях.

LaTeX

$$$$ UniformOnFun.toFun _ f.toUniformOnFunIsCompact = f. $$$$

Lean4

@[simp]
theorem toUniformOnFun_toFun (f : C(α, β)) : UniformOnFun.toFun _ f.toUniformOnFunIsCompact = f :=
  rfl

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

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

Разделы

Аффилиация

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