map_coe

Mathlib.Topology.UniformSpace.Completion

URI: https://scilib.ai/kg/mathlib#UniformSpace.Completion.map_coe

English

For a ∈ α, the map applied to the embedded element equals f a: (Completion.map f)(â) = f(a).

Русский

Для a ∈ α отображение, применяемое к встроенному элементу, равно f(a): (Completion.map f)(â) = f(a).

LaTeX

$$$\\forall a:\\alpha, (\\mathrm{Completion.map} f)(\\hat a) = f(a)$$$

Lean4

theorem map_coe (hf : UniformContinuous f) (a : α) : (Completion.map f) a = f a :=
  cPkg.map_coe cPkg hf a

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

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

Разделы

Аффилиация

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