isBigO — Mathlib

English

A bounded bilinear map is continuous as a function on E×F.

Русский

Ограниченное билинейное отображение непрерывно как функция на E×F.

LaTeX

$$$IsBoundedBilinearMap\ 𝕜 f \Rightarrow Continuous f$$$

Lean4

protected theorem isBigO (h : IsBoundedBilinearMap 𝕜 f) : f =O[⊤] fun p : E × F => ‖p.1‖ * ‖p.2‖ :=
  let ⟨C, _, hC⟩ := h.bound
  Asymptotics.IsBigO.of_bound C <| Filter.Eventually.of_forall fun ⟨x, y⟩ => by simpa [mul_assoc] using hC x y

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