isBoundedUnder_le — Mathlib

English

For any l, f: α → E, and c ≠ 0, f = O_l (λ x, c) iff IsBoundedUnder (≤) l (‖f‖).

Русский

Для любого l, f: α → E и c ≠ 0: f = O_l (λ x, c) эквивалентно IsBoundedUnder (≤) l (‖f‖).

LaTeX

$$$ (f =O[l](\lambda x. c)) \iff (c \neq 0) \, \rightarrow\ IsBoundedUnder (\le) l (\|f\|). $$$

Lean4

theorem isBoundedUnder_le {c : F} (h : f =O[l] fun _x => c) : IsBoundedUnder (· ≤ ·) l (norm ∘ f) :=
  let ⟨c', hc'⟩ := h.bound
  ⟨c' * ‖c‖, eventually_map.2 hc'⟩

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