termAEStronglyMeasurable[_]

Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

URI: https://scilib.ai/kg/mathlib#MeasureTheory.termAEStronglyMeasurable[_]

Lean4

/-- A function is `m`-`AEStronglyMeasurable` with respect to a measure `μ` if it is almost
everywhere equal to the limit of a sequence of `m`-simple functions. -/
@[scoped term_parser 1000]
public meta def «termAEStronglyMeasurable[_]» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `MeasureTheory.«termAEStronglyMeasurable[_]» 1024
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "AEStronglyMeasurable[") (ParserDescr.cat✝ `term 0))
      (ParserDescr.symbol✝ "]"))

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru