isBigO_const_const_iff — Mathlib

English

Same as previous item, duplication for another context.

Русский

То же самое, повторение для другого контекста.

LaTeX

$$IsBigO l (fun _x => c) (fun _x => c')$$

Lean4

@[simp]
theorem isBigO_const_const_iff {c : E''} {c' : F''} (l : Filter α) [l.NeBot] :
    ((fun _x : α => c) =O[l] fun _x => c') ↔ c' = 0 → c = 0 :=
  by
  rcases eq_or_ne c' 0 with (rfl | hc')
  · simp [EventuallyEq]
  · simp [hc', isBigO_const_const _ hc']

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