English
Tendsto in WeakBilin B is equivalent to pointwise tendsto of all evaluations: f → x holds in WeakBilin B if and only if for every y ∈ F, B(f(·), y) tends to B(x,y).
Русский
Пределы переходов в WeakBilin B эквивалиентны по точечной схеме оценок: f → x в WeakBilin B тогда и только тогда, когда для каждого y ∈ F функция i ↦ B(f(i), y) стремится к B(x,y).
LaTeX
$$Tendsto f l (nhds x) ↔ ∀ y, Tendsto (fun i => B (f i) y) l (nhds (B x y))$$
Lean4
/-- Addition in `WeakBilin B` is continuous. -/
instance instContinuousAdd [ContinuousAdd 𝕜] : ContinuousAdd (WeakBilin B) :=
by
refine ⟨continuous_induced_rng.2 ?_⟩
refine
cast (congr_arg _ ?_) (((coeFn_continuous B).comp continuous_fst).add ((coeFn_continuous B).comp continuous_snd))
ext
simp only [Function.comp_apply, Pi.add_apply, map_add, LinearMap.add_apply]
