term∫_,_ — Mathlib

English

If the (scalar) integral of f is nonzero, then f is integrable in the Bochner sense.

Русский

Если скалярный интеграл функции не равен нулю, то функция интегрируема в смысле Бо́хнера.

LaTeX

$$$\\int f \\neq 0 \\Rightarrow f \\text{ integrable (Bochner)}$$$

Lean4

@[inherit_doc MeasureTheory.integral, term_parser 1000]
public meta def «term∫_,_» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `MeasureTheory.«term∫_,_» 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "∫") Batteries.ExtendedBinder.extBinders)
        (ParserDescr.symbol✝ ", "))
      (ParserDescr.cat✝ `term 60))

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