termStronglyMeasurable[_] — Mathlib

English

If f is AEMeasurable and μ is sigma-finite, then f is AEFinStronglyMeasurable.

Русский

Если f измеримо почти всюду относительно μ и μ сигма-конечна, то f является AEFinStronglyMeasurable.

LaTeX

$$$\\text{AEMeasurable}(f,\\mu) \\Rightarrow \\text{AEFinStronglyMeasurable}(f,\\mu)$$$

Lean4

/-- The notation for StronglyMeasurable giving the measurable space instance explicitly. -/
@[scoped term_parser 1000]
public meta def «termStronglyMeasurable[_]» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `MeasureTheory.«termStronglyMeasurable[_]» 1024
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "StronglyMeasurable[") (ParserDescr.cat✝ `term 0))
      (ParserDescr.symbol✝ "]"))

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