coeFn_continuous

Mathlib.Topology.Algebra.Module.WeakDual

URI: https://scilib.ai/kg/mathlib#WeakDual.coeFn_continuous

English

For every y in E, the evaluation map ev_y: WeakDual 𝕜 E → 𝕜, given by ev_y(φ) = φ(y), is continuous.

Русский

Пусть для каждого y ∈ E отображение оценки ev_y: WeakDual 𝕜 E → 𝕜, ev_y(φ) = φ(y), непрерывно.

LaTeX

$$$ev_y \in C\big(\mathrm{WeakDual}_{\mathbb{k}} E, \mathbb{k}\big)$$$

Lean4

theorem coeFn_continuous : Continuous fun (x : WeakDual 𝕜 E) y => x y :=
  continuous_induced_dom

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

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

Разделы

Аффилиация

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