term__[|_] — Mathlib

English

If μ is finite on s and μ(s) ≠ 0, then the conditional measure μ[|s] is a probability measure.

Русский

Если μ ограничена на s и μ(s) ≠ 0, то условная мера μ[|s] является вероятностной мерой.

LaTeX

$$$[IsFiniteMeasure\\; μ] \\wedge μ(s) ≠ 0 \\Rightarrow IsProbabilityMeasure(μ[|s])$$$

Lean4

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

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