isLittleO_const_iff_isLittleO_one

English

A simplification showing constant bound equivalence to 1-bound in Big-OWith.

Русский

Упрощение эквивалентности ограничений константы 1 в Big-OWith.

LaTeX

$$IsBigOWith c l f g ↔ (something with 1-bound)$$

Lean4

theorem isLittleO_const_iff_isLittleO_one {c : F''} (hc : c ≠ 0) : (f =o[l] fun _x => c) ↔ f =o[l] fun _x => (1 : F) :=
  ⟨fun h => h.trans_isBigOWith (isBigOWith_const_one _ _ _) (norm_pos_iff.2 hc), fun h =>
    h.trans_isBigO <| isBigO_const_const _ hc _⟩

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