coeFn_continuous

Mathlib.Topology.Algebra.Module.WeakBilin

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

← MathLib Explorer

English

The map x ↦ (y ↦ B(x,y)) from WeakBilin B into F → 𝕜 is continuous.

Русский

Отображение x ↦ (y ↦ B(x,y)) из WeakBilin B в F → 𝕜 непрерывно.

LaTeX

$$Continuous fun (x : WeakBilin B) y => B(x,y)$$

Lean4

/-- The coercion `(fun x y => B x y) : E → (F → 𝕜)` is continuous. -/
theorem coeFn_continuous : Continuous fun (x : WeakBilin B) y => B x y :=
  continuous_induced_dom

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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