term_=O[_]_ — Mathlib

English

If IsBigOWith c l f g holds, then the same bound holds after applying a norm to the left function: IsBigOWith c l ||f|| g.

Русский

Если IsBigOWith имеет место при f и g, то та же граница действует после взятия нормы: IsBigOWith c l ||f|| g.

LaTeX

$$IsBigOWith c l f g → IsBigOWith c l (fun x => ‖f(x)‖) g$$

Lean4

@[inherit_doc IsBigO, term_parser 1000]
public meta def «term_=O[_]_» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `Asymptotics.«term_=O[_]_» 100 0
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " =O[") (ParserDescr.cat✝ `term 0))
        (ParserDescr.symbol✝ "] "))
      (ParserDescr.cat✝ `term 100))

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