inner — Mathlib

English

If f and g are continuous within a set s at x, then the map t ↦ ⟪f t, g t⟫ is continuous within s at x.

Русский

Если функции f и g непрерывны внутри множества s в точке x, тогда отображение t ↦ ⟪f t, g t⟫ непрерывно внутри s в x.

LaTeX

$$$\\text{ContinuousWithinAt}_{s}^{x}\\left( t \\mapsto \\langle f(t), g(t)\\rangle \\right)$$$

Lean4

@[continuity, fun_prop]
theorem inner (hf : Continuous f) (hg : Continuous g) : Continuous fun t => ⟪f t, g t⟫ :=
  continuous_iff_continuousAt.2 fun _x => by fun_prop

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