continuous_right — Mathlib

English

For a bounded bilinear map h, the map e1 ↦ f(e1, e2) is continuous for each fixed e2.

Русский

Для фиксированного e2 отображение e1 ↦ f(e1, e2) непрерывно.

LaTeX

$$$\forall e_1, \; h.continuous$; (напр. $e_1 \mapsto f(e_1, e_2)$ непрерывно)$$

Lean4

theorem continuous_right (h : IsBoundedBilinearMap 𝕜 f) {e₁ : E} : Continuous fun e₂ => f (e₁, e₂) :=
  h.continuous.comp (continuous_const.prodMk continuous_id)

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