term_=o[_]_ — Mathlib

English

Equivalent representation: IsLittleO l f g is equivalent to the statement that there exists c>0 with for all x in l, ‖f(x)‖ ≤ c‖g(x)‖.

Русский

Эквивалентное представление: IsLittleO l f g эквивалентно существованию c>0 такого, чтобы для всех x в l выполнялось неравенство.

LaTeX

$$IsLittleO_def'$$

Lean4

@[inherit_doc IsLittleO, 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))

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