inner_

Mathlib.Analysis.InnerProductSpace.OfNorm

URI: https://scilib.ai/kg/mathlib#Continuous.inner_

← MathLib Explorer

English

If f,g: ℝ → E are continuous, then x ↦ ⟨f(x), g(x)⟩ is continuous.

Русский

Если f,g: ℝ → E непрерывны, то ⟨f(x),g(x)⟩ по x непрерывно.

LaTeX

$$$\text{Continuous}_{x}( \langle f(x), g(x)\rangle )$$$

Lean4

theorem _root_.Continuous.inner_ {f g : ℝ → E} (hf : Continuous f) (hg : Continuous g) :
    Continuous fun x => inner_ 𝕜 (f x) (g x) := by
  unfold _root_.inner_
  fun_prop

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

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

Разделы

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

Аффилиация

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