isLittleO_pi — Mathlib

English

For finite index set, a bound for a function into a product is equivalent to a family of bounds bound for each coordinate.

Русский

Для конечного множества индексов равносильно существование границ по каждой координате.

LaTeX

$$$\\displaystyle \\text{If } f : α \\to ∀ i, E_i, \\; f = O_l g \\iff ∀ i, f_i = O_l g.$$$

Lean4

@[simp]
theorem isLittleO_pi {ι : Type*} [Fintype ι] {E' : ι → Type*} [∀ i, NormedAddCommGroup (E' i)] {f : α → ∀ i, E' i} :
    f =o[l] g' ↔ ∀ i, (fun x => f x i) =o[l] g' :=
  by
  simp +contextual only [IsLittleO_def, isBigOWith_pi, le_of_lt]
  exact ⟨fun h i c hc => h hc i, fun h c hc i => h i hc⟩

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