term∫⁻_In_,_∂_ — Mathlib

Lean4
@[inherit_doc MeasureTheory.lintegral, term_parser 1000]
public meta def «term∫⁻_In_,_∂_» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `MeasureTheory.«term∫⁻_In_,_∂_» 1022
    (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.cat✝ `term 0))
            (ParserDescr.symbol✝ ", "))
          (ParserDescr.cat✝ `term 60))
        (ParserDescr.symbol✝ " ∂"))
      (ParserDescr.cat✝ `term 70))
Похожие утверждения