term∮_InC(_,_),_ — Mathlib

English

The circle integral can be computed by integrating over θ in the closed interval Icc[0, 2π] using the same integrand deriv(circleMap c R) θ • f(circleMap c R θ).

Русский

Круговой интеграл можно вычислять, интегрируя по θ на отрезке Icc[0,2π] той же интеграндной функции deriv(circleMap c R) θ • f(circleMap c R θ).

LaTeX

$$$\\oint z\\in C(c,R) f(z)\\;dz = \\int_{\\theta\\in Icc\\;0\\;2\\pi} deriv(circleMap\\; c\\; R)\\;\\theta \\;\\cdot f(circleMap\\; c\\; R\\; \\theta) \\, d\\theta$$$

Lean4

/-- `∮ z in C(c, R), f z` is the circle integral $\oint_{|z-c|=R} f(z)\,dz$. -/
@[term_parser 1000]
public meta def «term∮_InC(_,_),_» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `«term∮_InC(_,_),_» 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen
              (ParserDescr.binary✝ `andthen
                (ParserDescr.binary✝ `andthen
                  (ParserDescr.binary✝ `andthen
                    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "∮") Batteries.ExtendedBinder.extBinders)
                    (ParserDescr.symbol✝ " in "))
                  (ParserDescr.symbol✝ "C("))
                (ParserDescr.cat✝ `term 0))
              (ParserDescr.symbol✝ ", "))
            (ParserDescr.cat✝ `term 0))
          (ParserDescr.symbol✝ ")"))
        (ParserDescr.symbol✝ ", "))
      (ParserDescr.cat✝ `term 0))

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