inner — Mathlib

English

For any α and continuous maps f,g : α → Completion(E), the map x ↦ ⟪f(x), g(x)⟫ is continuous.

Русский

Для любых непрерывных отображений f,g: α → Completion(E) отображение x ↦ ⟪f(x), g(x)⟫ непрерывно.

LaTeX

$$$\text{If } f,g: \alpha \to \mathrm{Completion}(E) \text{ are continuous, then } x \mapsto \langle f(x), g(x)\rangle \text{ is continuous.}$$$

Lean4

@[fun_prop]
protected theorem inner {α : Type*} [TopologicalSpace α] {f g : α → Completion E} (hf : Continuous f)
    (hg : Continuous g) : Continuous (fun x : α => ⟪f x, g x⟫) :=
  UniformSpace.Completion.continuous_inner.comp (hf.prodMk hg :)

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