eval_continuous

Mathlib.Topology.Algebra.Module.WeakDual

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

English

For a fixed y ∈ E, the evaluation ev_y: WeakDual 𝕜 E → 𝕜 is continuous.

Русский

Для фиксированного y ∈ E отображение ev_y: WeakDual 𝕜 E → 𝕜 непрерывно.

LaTeX

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

Lean4

theorem eval_continuous (y : E) : Continuous fun x : WeakDual 𝕜 E => x y :=
  continuous_pi_iff.mp coeFn_continuous y

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

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

Разделы

Аффилиация

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