_,_∂_ — Mathlib

English

The norm of the interval integral equals the integral of the norm over the restricted interval.

Русский

Норма интервального интеграла равна интегралу нормы по ограниченному интервалу.

LaTeX

$$$\\|\\int x \\in a..b f(x) \\partial\\mu\\| = \\|\\int x \\in Ι a b f(x) \\partial\\mu\\|$$$

Lean4

@[inherit_doc intervalIntegral, term_parser 1000]
public meta def «term∫_In_.._,_∂_» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `«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.binary✝ `andthen
                    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "∫") Batteries.ExtendedBinder.extBinders)
                    (ParserDescr.symbol✝ " in "))
                  (ParserDescr.cat✝ `term 0))
                (ParserDescr.symbol✝ ".."))
              (ParserDescr.cat✝ `term 0))
            (ParserDescr.symbol✝ ", "))
          (ParserDescr.cat✝ `term 60))
        (ParserDescr.symbol✝ " ∂"))
      (ParserDescr.cat✝ `term 70))

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