continuous_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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