English
A bounded bilinear map is continuous as a function of two variables; hence the corresponding bilinear operator is continuous.
Русский
Ограниченное билинейное отображение непрерывно как функция от двух переменных; следовательно, связанный билинейный оператор непрерывен.
LaTeX
$$$IsBoundedBilinearMap\ 𝕜 f \Rightarrow Continuous f$$$
Lean4
/-- Useful to use together with `Continuous.comp₂`. -/
theorem continuous (h : IsBoundedBilinearMap 𝕜 f) : Continuous f :=
by
refine continuous_iff_continuousAt.2 fun x ↦ tendsto_sub_nhds_zero_iff.1 ?_
suffices Tendsto (fun y : E × F ↦ f (y.1 - x.1, y.2) + f (x.1, y.2 - x.2)) (𝓝 x) (𝓝 (0 + 0)) by
simpa only [h.map_sub_left, h.map_sub_right, sub_add_sub_cancel, zero_add] using this
apply Tendsto.add
· rw [← isLittleO_one_iff ℝ, ← one_mul 1]
refine h.isBigO_comp.trans_isLittleO ?_
refine (IsLittleO.norm_left ?_).mul_isBigO (IsBigO.norm_left ?_)
· exact (isLittleO_one_iff _).2 (tendsto_sub_nhds_zero_iff.2 (continuous_fst.tendsto _))
· exact (continuous_snd.tendsto _).isBigO_one ℝ
· refine Continuous.tendsto' ?_ _ _ (by rw [h.map_sub_right, sub_self])
exact ((h.toContinuousLinearMap x.1).continuous).comp (continuous_snd.sub continuous_const)
