English
If μ is finite and μ(s) ≠ 0, then μ[|s] is a probability measure.
Русский
Если μ конечна и μ(s) ≠ 0, то μ[|s] — вероятностная мера.
LaTeX
$$$IsFiniteMeasure(μ) \\Rightarrow (μ(s) ≠ 0 \\Rightarrow IsProbabilityMeasure(μ[|s]))$$$
Lean4
@[inherit_doc 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.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✝ "]"))
