isLittleO_const_const_iff — Mathlib

English

Another equivalent characterization: u = o[l] v is equivalent to existence of φ with Tendsto φ to 0 and u = φ v up to l-equivalence.

Русский

Еще одна эквивалентная характеристика: u = o[l] v эквивалентно существованию φ с Tendsto φ→0 и u = φ v почти по l.

LaTeX

$$$ u =o[l] v \\iff \\exists \\phi : α \\to 𝕜, Tendsto \\phi l (\\mathcal{N} 0) ∧ u =ᶠ[l] \\phi \\cdot v $$$

Lean4

@[simp high] -- Increase priority so that this triggers before `isLittleO_const_left`

theorem isLittleO_const_const_iff [NeBot l] {d : E''} {c : F''} : ((fun _x => d) =o[l] fun _x => c) ↔ d = 0 :=
  by
  have : ¬Tendsto (Function.const α ‖c‖) l atTop := not_tendsto_atTop_of_tendsto_nhds tendsto_const_nhds
  simp only [isLittleO_const_left, or_iff_left_iff_imp]
  exact fun h => (this h).elim

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