English
The conditional measure μ[|s] is either the zero measure or a probability measure.
Русский
Условная мера μ[|s] либо нулевая, либо вероятностная мера.
LaTeX
$$$IsZeroOrProbabilityMeasure(μ[|s])$$$
Lean4
/-- The conditional probability measure of measure `μ` on `{ω | X ω ∈ s}`.
It is `μ` restricted to `{ω | X ω ∈ s}` and scaled by the inverse of `μ {ω | X ω ∈ s}`
(to make it a probability measure): `(μ {ω | X ω ∈ s})⁻¹ • μ.restrict {ω | X ω ∈ s}`. -/
@[scoped term_parser 1000]
public meta def «term__[|_In_]» : Lean.TrailingParserDescr✝ :=
ParserDescr.trailingNode✝ `ProbabilityTheory.«term__[|_In_]» 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✝ " in "))
(ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ "]"))
