English
For each w in W, the map v ↦ e(L(v,w)) defines a bounded continuous function from V to ℂ. In other words, for every w ∈ W, the function v ↦ e(L(v,w)) lies in the bounded continuous function space on V with values in ℂ.
Русский
Пусть w ∈ W. Отображение v ↦ e(L(v,w)) является ограниченной непрерывной функцией от V в ℂ. То есть для каждого w ∈ W функция v ↦ e(L(v,w)) принадлежит пространству ограниченных непрерывных функций на V с значениям в ℂ.
LaTeX
$$$\\forall w \\in W,\\quad (v \\mapsto e(L(v,w))) \\in C_b(V, \\mathbb{C}).$$$
Lean4
/-- The bounded continuous mapping `fun v ↦ e (L v w)` from `V` to `ℂ`. -/
noncomputable def char (he : Continuous e) (hL : Continuous fun p : V × W ↦ L p.1 p.2) (w : W) : V →ᵇ ℂ
where
toFun := fun v ↦ e (L v w)
continuous_toFun := continuous_induced_dom.comp (he.comp (hL.comp (Continuous.prodMk_left w)))
map_bounded' := by
refine ⟨2, fun x y ↦ ?_⟩
calc
dist _ _ ≤ (‖_‖ : ℝ) + ‖_‖ := dist_le_norm_add_norm _ _
_ ≤ 1 + 1 := (add_le_add (by simp) (by simp))
_ = 2 := by ring
