term__[_|_] — Mathlib

English

The set {f ∈ Lp F p μ | AEStronglyMeasurable[m] f μ} is closed.

Русский

Множество {f ∈ Lp F p μ | AEStronglyMeasurable[m] f μ} замкнуто.

LaTeX

$$$\text{IsClosed}\{f:\ Lp F p μ \mid AEStronglyMeasurable[m] f μ\}$$$

Lean4

@[inherit_doc MeasureTheory.condExp, scoped term_parser 1000]
public meta def «term__[_|_]» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `MeasureTheory.«term__[_|_]» 1024 0
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.unary✝ `group (ParserDescr.const✝ `noWs))
              (ParserDescr.symbol✝ "["))
            (ParserDescr.cat✝ `term 0))
          (ParserDescr.symbol✝ "|"))
        (ParserDescr.cat✝ `term 0))
      (ParserDescr.symbol✝ "]"))

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