isEquivalent_zero_iff_isBigO_zero

English

u ~[l] 0 iff u =O[l] 0 (i.e., u is bounded by 0 in the Big-O sense).

Русский

u ~[l] 0 эквивалентно u =O[l] 0 (то есть ограничено по Big-O относительно нуля).

LaTeX

$$$u ~[l] 0 \iff u =O[l] (0 : α \to β)$$$

Lean4

theorem isEquivalent_zero_iff_isBigO_zero : u ~[l] 0 ↔ u =O[l] (0 : α → β) :=
  by
  refine ⟨IsEquivalent.isBigO, fun h ↦ ?_⟩
  rw [isEquivalent_zero_iff_eventually_zero, eventuallyEq_iff_exists_mem]
  exact ⟨{x : α | u x = 0}, isBigO_zero_right_iff.mp h, fun x hx ↦ hx⟩

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